Sciweavers

WOLLIC
2010
Springer
13 years 10 months ago
Intersection Type Systems and Explicit Substitutions Calculi
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...
Daniel Lima Ventura, Mauricio Ayala-Rincón,...
CORR
2002
Springer
99views Education» more  CORR 2002»
14 years 2 days ago
Intersection Types and Lambda Theories
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...
Mariangiola Dezani-Ciancaglini, Stefania Lusin
ENTCS
2002
90views more  ENTCS 2002»
14 years 3 days ago
Simple Easy Terms
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...
Fabio Alessi, Stefania Lusin
TCS
2008
14 years 6 days ago
A typed lambda calculus with intersection types
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...
Viviana Bono, Betti Venneri, Lorenzo Bettini
FSTTCS
1993
Springer
14 years 4 months ago
Essential Intersection Type Assignment
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...
Steffen van Bakel
ICFP
1997
ACM
14 years 4 months ago
A Modular, Polyvariant, and Type-Based Closure Analysis
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...
Anindya Banerjee
ICFP
1999
ACM
14 years 4 months ago
Relating Typability and Expressiveness in Finite-Rank Intersection Type Systems (Extended Abstract)
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...
Assaf J. Kfoury, Harry G. Mairson, Franklyn A. Tur...
LICS
2000
IEEE
14 years 4 months ago
A Model for Impredicative Type Systems, Universes, Intersection Types and Subtyping
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...
Alexandre Miquel
RTA
2007
Springer
14 years 6 months ago
Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi
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...
Kentaro Kikuchi