gmane.comp.science.types

[TYPES] Future of TLCA

Paweł Urzyczyn — 2013-05-01T12:02:37

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]


This message is addressed to everyone interested in the future
of the conference TLCA (Typed Lambda Calculi and Applications).
The bi-annual conference started in 1993 and will have its 11th
edition this June in Eindhoven as part of RDP. After 20 years
it seems reasonable to ask some questions about the future.
In particular there is an emerging discussion on whether TLCA
should merge with RTA or perhaps develop into a new conference
of a broader scope. In order to gain opinions from as large part
of TLCA community as possible, we have created a Google Group:

     https://groups.google.com/forum/#!forum/tlca-list

We invite everybody who feels part of TLCA community to contribute
to the discussion with their opinions and suggestions.

Samson Abramsky, Pierre-Louis Curien,
Mariangiola Dezani-Ciancaglini,
Masahito Hasegawa, Luke Ong,
Simona Ronchi Della Rocca,
Paweł Urzyczyn

[TYPES] John Reynolds

Uday S Reddy — 2013-04-29T19:39:48

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear friends and colleagues,

I am sorry to bring the sad news that John Reynolds, whose work and insights
I have mentioned and recounted in my recent exchanges, has passed away on
Sunday in Pittsburgh.

John has not only done seminal work on a wide range of programming language
topics, but he was also a guiding spirit and a great friend to many of us.
We will dearly miss him.

At this juncture, we might take a moment to reflect on his life time of
accomplishment:

  http://www.cs.cmu.edu/~jcr/

Uday

[TYPES] The type/object distinction and possible synthesis of OOP and imperative programming languages

Mark Janssen — 2013-04-15T03:48:05

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello,

I'm new to the list and hoping this might be the right place to
introduce something that has provoked a bit of an argument in my
programming community.

I'm from the Python programming community.  Python is an "interpreted"
language.  Since 2001, Python's has migrated towards a "pure" Object
model (ref: http://www.python.org/download/releases/2.2/descrintro/).
Prior to then, it had both types and classes and these types were
anchored to the underlying C code and the machine/hardware
architecture itself.  After the 2001 "type/class unification" , it
went towards Alan Kay's ideal of "everything is an object".  From
then, every user-defined class inherited from the abstract Object,
rooted in nothing but a pure abstract ideal.  The parser, lexer, and
such spin these abstrations into something that can be run on the
actual hardware.

As a contrast, this is very distinct from C++, where everything is
concretely rooted in the language's type model which in *itself* is
rooted (from it's long history) in the CPU architecture.   The STL,
for example, has many Container types, but each of them requires using
a single concrete type for homogenous containers or uses machine
pointers to hold arbitrary items in heterogeneous containers (caveat:
I haven't programmed in C++ for a long time, so it's possible this
might not be correct anymore).

My question is:  Is there something in the Computer Science literature
that has noticed this distinction/development in programming language
design and history?

It's very significant to me, because as languages went higher and
higher to this pure OOP model, the programmer+data ecosystem tended
towards very personal object hierarchies because now the hardware no
longer formed a common basis of interaction (note also, OOPs promise
of re-usable code never materialized).

It's not unlike LISP, where the power of its general language
architecture tended towards hyperpersonal mini macro languages --
making it hardly used, in practice, though it was and is so powerful,
in theory.

That all being said, the thrust of this whole effort is to possibly
advance Computer Science and language design, because in-between the
purely concrete "object" architecture of the imperative programming
languages and the purely abstract object architecture of
object-oriented programming languages is a possible middle ground that
could unite them all.

Thank you for your time.

Mark Janssen
Tacoma, Washington

[TYPES] Decidability of type reconstruction in predicative System-F?

Christian Skalka — 2013-01-28T22:38:24

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I am wondering if there are formal results related to the (un?)decidability
of type reconstruction in predicative System-F. As I understand it, Joe
Wells' well-known undecidability result only applies to impredicative
System-F.

Pointers/citations appreciated.

Thanks,

-chris

[TYPES] Strong normalization of overlapping rewrite rules

Andreas Abel — 2012-12-11T00:34:53

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

The typical normalization proof for a typed lambda calculus with rewrite 
rules requires the rules to be left-linear and non-overlapping.  What is 
known about left-linear but /overlapping/ rewriting?  [References 
appreciated.]

Best,
Andreas

[TYPES] a counterexample to Plotkin and Abadi's characterization of equivalence at existential type?

Derek Dreyer — 2012-12-05T13:42:50

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I have what appears to be a counterexample to the characterization of
equivalence at existential type in Plotkin and Abadi's logic for
parametric polymorphism, and I'm wondering what's going on.  Here is a
link to their TLCA'93 paper from Gordon's web page:

http://homepages.inf.ed.ac.uk/gdp/publications/Par_Poly.pdf

In short, Theorem 7 in their paper says that two terms of existential
type are equal *if and only if* there exists a "simulation relation"
between their internal representations of the abstract type such that
the operations are logically related at the appropriate type
(interpreting the abstract type using the chosen simulation relation).
 The "if" direction is fine: that's just the well-known principle of
"representation independence".  It's the "only if" direction that I'm
confused about.

In particular, it seems to me that, using the "only if" direction of
Theorem 7, I can derive a contradiction in the logic, so I'm trying to
figure out where/if I screwed up.

The issue is the following: There is an example given in Pitts'
chapter in Pierce's ATTAPL book, namely Sumii's variation on Example
7.7.4 discussed in Remark 7.7.7.  (I will reproduce it below.)  The
entire point of the example, which in Sumii's variation applies to
pure System F, is that it shows a case where two existential packages
are contextually equivalent despite the fact that there is no
simulation relation between their type representations that would make
a simulation argument (i.e. representation independence proof) go
through.  Pitts proves that there is no simulation proof, and he also
sketches the proof of contextual equivalence of the packages through
brute-force means.

Now, by itself, Pitts' result is not in contradiction to Theorem 7
from the Plotkin-Abadi logic (PAL) paper, since PAL does not talk
about contextual equivalence: it talks about its own primitive notion
of equality.  So one might write off this example as a quirk of
contextual equivalence which is not relevant to the better-behaved PAL
equality.

However, in March 2008, I worked out (and privately circulated) a
*much* simpler proof of the contextual equivalence in question, which
is not brute force: rather, it relies on a simple transitive
combination of two simulation subproofs (see below).  Now it seems to
me that there should be no problem expressing my simulation proofs in
PAL, and therefore constructing a proof of equivalence of the
existential packages in the example (by transitivity of PAL's
equality), despite the fact that there is provably no direct
simulation argument that shows them equivalent.  So, unless I'm
confused (which I probably am), this would seem to contradict the
"only if" direction of Theorem 7.

One basic problem I have is that I do not understand the proof of the
"only if" direction of Theorem 7 in PAL -- it is not presented in the
paper (which merely suggests that it follows from the "parametricity
schema"), and I have not yet found a worked-out proof of it in any
follow-on paper either.  If someone can point me to such a proof, that
would be most helpful.  If not, how would one prove it?
Alternatively, have I gone wrong somewhere in my argument that it is
false?

The details of the "counterexample" are given below.

Thanks and best regards,
Derek

-------

First, here are the details of Pitts' example (the Sumii variation):

Q = Exists X. (X -> Bool) -> Bool
Void = Forall X. X
H1 = \f:Void->Bool. False
P1 = pack [Void,H1] as Q
H2 = \f:Bool->Bool. (f True) and not (f False)
P2 = pack [Bool,H2] as Q

We want to prove that P1 is equivalent to P2.  Intuitively, they are
equivalent because the only possible function that could be passed in
as the instantiation of f is the constant function returning True or
False.  In either case, both H1(f) and H2(f) will return False.

A direct simulation proof does not exist.  To see this, suppose one
did exist: it would involve a simulation relation between Void and
Bool, together with a proof that H1 and H2 are related at "(E -> Bool)
-> Bool".

1. Void is an empty type, so the only possible simulation relation
between Void and Bool is the empty relation E.

2. Given E as the necessary choice of simulation relation, we can
choose f1 to be any function of type Void -> Bool and we can choose f2
to be the identity function at Bool -> Bool.  Since E is empty, it is
trivial to show that f1 and f2 are logically related at "E -> Bool".
However, H1(f1) returns False, while H2(f2) returns True, in which
case they are not logically related at Bool.  So H1 and H2 are *not*
logically related at "(E -> Bool) -> Bool".  Contradiction.

OK, now I will prove that P1 and P2 are in fact equivalent by giving a
*pair* of simulation proofs demonstrating that each of them is
equivalent to P3, defined as follows:

H3 = \f:Bool->Bool. (f True) and not (f True)
P3 = pack [Bool,H3] as Q

To prove P1 equivalent to P3 by simulation argument:

1. We choose the simulation relation to be the empty relation E
between Void and Bool (that's all we can choose).

2. Let f1 and f3 be functions of type Void -> Bool and Bool -> Bool
related at "E -> Bool".  We must show H1(f1) and H3(f3) are related at
Bool.  Clearly, H1(f1) = False, so we must show H3(f3) = False.  We
know that (f3 True) has type Bool, so it either equals True or False
(the logical relations lemma tells us that, if nothing else).  In
either case, H3(f3) = False, so we are done.

To prove P3 equivalent to P2 by simulation argument:

1. We choose the simulation relation to be the full relation R between
Bool and Bool.  Choosing R = {(True,True),(True,False)} would also
work.

2. Let f3 and f2 be functions, both of type Bool -> Bool, related at
"R -> Bool".  We must show H3(f3) and H2(f2) related at Bool, i.e.
that H3(f3) = H2(f2).  Since (True,True) and (True,False) are both in
R, we have from the relatedness of f3 and f2 that (f3 True) = (f2
True) and (f3 True) = (f2 False).  Hence, (f2 True) = (f3 True) = (f2
False), and so H3(f3) = H2(f2) = False.

Thus, P1 = P3 = P2, which implies P1 = P2 by transitivity, but there
is no direct simulation proof of P1 = P2, which seems to contradict
the "only if" direction of Theorem 7.

[TYPES] Please give me a link. Is alpha-conversion easy or not?

George Cherevichenko — 2012-11-04T20:43:49

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi
Where can I find a precise description how to interpret typed lambda
calculi with named variables in cartesian closed categories? Or how to
interpret lambda calculi with named variables in lambda calculi with De
Brujn indices? I know how to do that, but I need a link. I need proofs of
the following facts:
1) Alpha-equal terms correspond to the same term with De Brujn indices (or
the same arrow in CCC).
2) Substitutions with named variables correspond to substitutions with De
Brujn indices.
I read Altenkirch "Alpha-conversion is easy", should I only refer to this
article?
Please, no nominal logic.
George

[TYPES] Free theorems for maps of higher rank and polarized systems?

Ahn, Ki Yung — 2012-10-16T23:38:55

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

I have some questions on free theorems for maps, which most people may 
believe, but having difficulty to cite where actual proof is written 
down, or an instance of a more general theorem, or whether it has ever 
been actually proved. I'd greatly appreciate pointers to related papers.


Question 1. Proper citation for free theorems for fmap
   (fmap is Haskell-ish term for generic maps) for rank 1
   (* -> *) and rank 2 (such as (* -> *) -> (* -> *))?

Wadler's "Theorems for free!" papers discusses map for lists.

But everyone seem to believe it holds for arbitrary structure of rank 1, 
that is, F : * -> *. We can formalize this idea in Fw as follows:

If there exists
   fmap : forall (f:*->*)(a:*)(b:*). (a -> b) -> f a -> f b
then (1) any such fmap satisfy the expected property of fmap, i.e.,
   fmap id = id
   fmap f . fmap f = fmap g
and  (2) also such fmap is unique.

Similar statement could be made for rank 2 version of this.
These generic maps of also called as monotonicity witness.

Papers on monotonicity that I've seen doesn't exactly proves (1) but 
since they use monotonicity witness to encode iterations or folds, I 
think it may be considered as indirect proof of the properties in (1). 
But it would be nice to know if you have seen proofs of statements in 
the form above as (1), and also for uniqeness (2), I'd appreciate the 
pointers to such literature.

Matthes' CSL'98 paper discusses that monotonicity witness for rank 2 has 
not been proved yet and it is an open question. Has this been proved 
afterwards for rank 2 or higher?



Question 2. Are fully(?) positively polarized type constructors monotone 
in general?

We can track polarities of the use of type constructor variables in Fw 
and label and have extra annotation +,-, or 0 (means it can be used in 
both + and - positions) at kinds (e.g., +* -> *, -* -> *, 0* -> *). 
Systems like Fixw in CSL 04 paper by Abel and others is an example of a 
polarized system. Then, in such systems, I conjecture that type 
constructors of kinds +* -> *, +(+* -> *) -> (+* ->*) that have + 
polarities everywhere must always have monotonicity witness.

This is a slightly more general version of strictly positivity because 
it considers negative of negative position to be positive. If you have 
seen anyone proved this, again, I would very much appreciate pointers to 
those materials.

Thanks in advance.

Ki Yung

[TYPES] [REMINDER] Agda Intensive Meeting 16th (AIM XVI) inCopenhagen

Nicolas Pouillard — 2012-08-23T15:46:22

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

[We apologize for multiple copies]

Hello,

This is a reminder that the next instance of AIM approaches.

It will be held at ITU in Copenhagen from October 3 to October 9.

Registration is still open and it is now a good time propose talks
and code sprint ideas.

Everyone with a genuine interest in Agda is invited
to attend. The meeting will be similar to previous ones:

 * Presentations concerning theory, implementation, and use cases
   of Agda.

 * Discussions around issues of the Agda language.

 * Plenty of time to work on or in Agda, in collaboration with the
   other participants.

A few details can be found on the wiki page of the event:

  http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXVI

including pointers to recommended accommodations.

Registration
------------

Although no  official registration is needed,  we want to know  how many
will attend. If you want to give a  talk please send us the title and an
abstract.

To register, please reply to us (our email is aim16 at ƛ.net — or if you
are not an unicode aficionado aim16 at xn--dia.net), filling out the
following form:

---------------8<----------------------------------------
Name:
Affiliation:
email:

Program:
* I'd like to give a talk or lead a discussion (yes/no):
Title:
Abstract: (optional)

* Suggestion for code-sprint (optional):
---------------8<----------------------------------------

See you in København,

[TYPES] decidability/confluence of beta-eta convertibility inChurch-style STLC

Derek Dreyer — 2012-08-10T11:34:49

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hi, all.  I'm having a hard time finding a (canonical) source for what
I thought would be a very simple question.

Consider the simply-typed lambda calculus (STLC), Church-style (with
type annotations on variable binders), and beta-eta reduction.
Beta-eta convertibility, which I'll write as M ~ N, means that M is
convertible to N by some sequence of beta/eta reductions/expansions,
which may very well go through ill-typed intermediate terms even if M
and N are themselves well-typed.

I want to show the following:

If G |- M : A and G |- N : A, and M ~ N, then M and N have the same
beta-eta (short) normal form.

It is well known that well-typed terms in STLC are strongly
normalizing wrt beta-eta reduction.  But to prove the above, one also
needs confluence.  The problem is that the intermediate terms in the
beta-eta conversion of M and N may be ill-typed, and
beta-eta-reduction is not confluent in this setting for ill-typed
terms.  In particular,

(\x:A.(\y:B.y)x)

can eta-convert to

\y:B.y

or beta-convert to

\x:A.x

which are only equal if A = B.

One strategy would be to prove that beta-eta-convertibility --
*between terms of the same type* -- going through ill-typed terms is
equivalent to beta-eta convertibility restricted to going only through
well-typed terms.  Intuitively, this seems like it should be true, but
it is not at all clear to me how to show it.  In particular, the
*between terms of the same type* part seems critical in order to
outlaw the confluence counterexample given above.

I found some discussion of some related questions in a thread on the
Types list from 1989:

http://article.gmane.org/gmane.comp.science.types/266  (and subsequent posts)

But it doesn't seem to contain a direct answer to my question.

Thanks!
Derek

[TYPES] question (cont.)

Vladimir Voevodsky — 2012-07-19T14:44:47

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Sorry, I forgot to mention that there is also induction. V.

[TYPES] a question

Vladimir Voevodsky — 2012-07-19T14:43:10

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello,

does any one know if the system of natural arithmetic with equality, addition, multiplication, exponentiation (or without exponentiation), "forall" quantifier, implication and conjunction is decidable? There is no existential quantifier and no negation.

Thanks!
Vladimir.

[TYPES] strict unit type

Vladimir Voevodsky — 2012-04-29T14:10:47

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello,

let Pt be the unit type ("one point"). In Coq-like systems it is introduced through an eliminator and the associated iota-reduction rule. This is in practice sufficient for proving all its expected properties modulo propositional equality (or identity types) but does not create a terminal object in the category of contexts. 

I wonder if any one has considered type theories where Pt is introduced as having a distinguished object tt together with reduction rules of the following form (in the absence of dependent sums, otherwise one needs more):

1. any object of Pt other than tt reduces to tt,

2. Prod x : T , Pt reduces to Pt,

3. Prod x : Pt , T reduces to T.

Thanks,
Vladimir.

[TYPES] Explicit renaming of bound variables

George Cherevichenko — 2012-04-27T20:31:42

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

 Hello.
I think I have  found "the right definition" of substitution and
alpha-conversion. Three main ideas are:
1) Contexts with multiplicity (i.e., repetitions of variables are
permitted);
2) A new form of explicit substitutions;
3) A new definition of free variables.
Renaming of bound variables when performing substitutions is done using
special reductions and may be delayed.
So far told two people: Lev Beklemishev and Mati Pentus (both like).
George.

http://arxiv.org/abs/1111.3171

[TYPES] Is naive freshness adequate to avoid capture?

Philip Wadler — 2012-04-27T11:14:07

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Say that a lambda term is 'fresh' if each lambda abstraction binds a
distinct variable.  For instance, (\x.(\y.\z.y)x) is fresh, but
(\x.(\y.\x.y)x) is not.

Consider lambda terms without the alpha rule, where capture avoiding
substitution is a partial function.  For instance, [x/y](\z.y) is
defined, but [x/y](\x.y) is undefined, because the substitution would
result in capture.

Consider a sequence of beta reductions where no alpha reduction is
allowed.  In our first example, this terminates in a normal form:

  (\x.(\y.\z.y)x) -->  \x.\z.x

In our second example, we get stuck.

  (\x.(\y.\x.y)x) -/->

Attempting to beta reduce the redex would result in capture.

Starting with a fresh term and performing beta reductions but no alpha
reductions, are there reduction sequences which get stuck?  I suspect
the answer is yes, but I am having difficulty locating a
counter-example in the literature or creating one on my own.

Answers gratefully received.  Yours,  -- P

[TYPES] A question about unification terminology

Giuseppe Castagna — 2012-03-28T13:13:52

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Typers,

   the problem of finding a substitution σ such that tσ=sσ is called unification;

   the problem of finding a substitution σ such that tσ=s is called 
semi-unification;

   but how is it called the problem of finding a substitution σ such that tσ≤sσ 
where ≤ denotes a generic subtyping relation?

I found in the literature the generic name of "subtype constraint resolution" 
(e.g., Pottier) but I was wondering whether there exists a more specific name.

Thanks in advance for your answers and pointers to related work.


Beppe

[TYPES] passing away of N.G. de Bruijn

Vrijer, R.C. de — 2012-03-14T14:44:17

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Sad to announce the passing away of

N. G. (Dick) de Bruijn                July 9, 1918 - February 17, 2012

We are grateful to this remarkable and inspiring man.
Next to putting his everlasting mark on diverse areas in pure and applied
mathematics, he introduced, in 1967, the pioneering language AUTOMATH
and the idea of automated verification of mathematical proofs after formalization.
This application of type theory and rewriting is both fundamental and high-tech.
The resulting field of formal verification has developed into a major industrial
contribution of mathematics.

Henk Barendregt
Jan Willem Klop
Roel de Vrijer

[TYPES] Representing inductive types with W-types

Kristina Sojakova — 2011-11-17T22:50:43

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Dear Russell,

I do not necessarily see anything ad-hoc about the particular encoding 
of tress as

Tree A ~ W (a,n):A*nat. Fin n

On the other hand, I find it very natural. After all, a tree is 
determined by
1) a term a : A, which is the value at the root
2) a term n : nat, which is the number of children
3) n subtrees
Each pair (a,n) will determine a separate constructor, thus the type of 
constructors will be A x nat. Since the arity of the constructor (a,n) 
is n, we need a dependent type
(a,n) : A x nat |- B(a,n) type
such that B(a,n) is inhabited by exactly n terms. As we see the value of 
a does not matter for this requirement, thus we need a type
n : nat |- B(n) type
which is inhabited by precisely n terms, which is the specification of 
Fin(n).

You are right that the types nat and Fin do not occur in the Coq 
definition of Tree A explicitly and have to be inferred at the 
meta-level. So if you are asking whether it is possible to derive a 
completely generic way to encode suitable data types (as in, a precise 
algorithm) then the answer is probably not. There has been some work 
done by Gambino&Hyland
in their paper "Wellfounded trees and Dependent Polynomial Functors":
http://www.math.unipa.it/~ngambino/Research/Papers/gambino-hyland.pdf
They show that certain class of inductive types corresponding to the 
dependent polynomial functors can be represented by W-types (which 
correspond to non-dependent polynomial functors). I am not sure if this 
is what you were looking for though.

Best,

Kristina

[TYPES] Representing inductive types with W-types

2011-11-17T20:57:36

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Does anyone have a reference on how to encode (non-mutually recursive) 
inductive data type declarations of a language similar to CiC using 
W-Types?

I was playing around with this by hand, and I can make ad-hoc encodings 
for the types I've tried; but I haven't quite figured out what the 
systematic translation is.  For example, I find

Inductive Tree (A:Type) : Type :=
node : A -> list (Tree A) -> Tree A

quite difficult to translate.  I can only manage because I happen to know 
that list X ~ Sigma n:nat. Fin n -> X

where Fin

Fin 0 = Void
Fin (S n) = Unit + Fin n

By my ad hoc method I get

nat ~ W : Bool. if b then Void else Unit
list A ~ W x : Unit + A. [const Void | const Unit] x
Tree A ~ W (a,n):A*nat. Fin n

But of course nat and Fin do not directly appear in the Inductive 
definition of Tree, so I'm not entirely sure how to deduce them (or 
something isomorphic) systematically.

[TYPES] Strong Normalization for Coq (CiC)

Jean-Philippe Bernardy — 2011-11-08T13:02:48

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

Hello,

I should point out that in [1], we have given a notion of logical relation
which is uniformly defined for terms, types and sorts. Although we
stay away from
the problem of normalization, the definition follows a similar pattern as yours.

You might also be interested in glancing at [2] or even [3].

Cheers,
JP.

[1] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=118913
[2] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=127466
[3] http://publications.lib.chalmers.se/cpl/record/index.xsql?pubid=147257

[TYPES] Strong Normalization for Coq (CiC)

Eddy Westbrook — 2011-11-03T16:15:09

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

All,

I have a new generalization of logical relations that can prove SN for  
CiC (the core theory of Coq), including the full universe hierarchy  
and inductive types. AFAIK, this has been an open problem for a while,  
and I thought my solution would be of interest to people on this list.

The basic idea is uniformity, where, instead of defining an  
interpretation (aka a logical relation) for only types, or defining  
one for types and one for terms, in my approach the interpretation is  
defined uniformly on all terms M. When M happens to be a type, the  
interpretation is similar to the standard logical relations for types.

The current draft can be found here:
http://www.cs.rice.edu/~emw4/uniform-lr.pdf

Thanks in advance for any input!
-Eddy

P.S. Thanks again to everyone who has helped me out with this paper,  
including prior anonymous reviewers.