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 lang

[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'

[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.

[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
ab

[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.  I

[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 grat

[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 po

[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.