WOLLIC
2010
Springer
13 years 9 months ago
2010
Springer
Abstract. The λ-calculus with de Bruijn indices, called λdB, assembles each α-class of λ-terms into a unique term, using indices instead of variable names. Intersection types p...
CORR
2002
Springer
13 years 11 months ago
2002
Springer
We illustrate the use of intersection types as a semantic tool for showing properties of the lattice of -theories. Relying on the notion of easy intersection type theory we succes...
ENTCS
2002
13 years 11 months ago
2002
We illustrate the use of intersection types as a semantic tool for proving easiness result on -terms. We single out the notion of simple easiness for -terms as a useful semantic p...
TCS
2008
13 years 11 months ago
2008
Intersection types are well-known to type theorists mainly for two reasons. Firstly, they type all and only the strongly normalizable lambda terms. Secondly, the intersection type...
FSTTCS
1993
Springer
14 years 3 months ago
1993
Springer
This paper will show the usefulness and elegance of strict intersection types for the Lambda Calculus; these are strict in the sense that they are the representatives of equivalen...
ICFP
1997
ACM
14 years 3 months ago
1997
ACM
We observe that the principal typing property of a type system is the enabling technology for modularity and separate compilation [10]. We use this technology to formulate a modul...
ICFP
1999
ACM
14 years 3 months ago
1999
ACM
d Abstract) Assaf J. Kfoury∗ Boston University http://www.cs.bu.edu/˜kfoury Harry G. Mairson† Brandeis University http://www.cs.brandeis.edu/˜mairson Franklyn A. Turbak‡ We...
LICS
2000
IEEE
14 years 3 months ago
2000
IEEE
We introduce a new model based on coherence spaces for interpreting large impredicative type systems such as the Extended Calculus of Constructions (ECC). Moreover, we show that t...
RTA
2007
Springer
14 years 5 months ago
2007
Springer
We present a method of lifting to explicit substitution calculi some characterizations of the strongly normalizing terms of λ-calculus by means of intersection type systems. The m...