Intersection types for explicit substitutions
From MaRDI portal
Publication:1887145
DOI10.1016/j.ic.2003.09.004zbMath1082.68014MaRDI QIDQ1887145
Steffen van Bakel, Mariangiola Dezani-Ciancaglini, Pierre Lescanne, Stéphane Lengrand, Dan Dougherty
Publication date: 23 November 2004
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2003.09.004
68N18: Functional programming and lambda calculus
Related Items
Resource operators for \(\lambda\)-calculus, Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca, Characterising Strongly Normalising Intuitionistic Sequent Terms, Computation with classical sequents
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- The lambda calculus. Its syntax and semantics. Rev. ed.
- An extension of basic functionality theory for \(\lambda\)-calculus
- Complete restrictions of the intersection type discipline
- Explicit substitution. On the edge of strong normalization
- Typing untyped \(\lambda\)-terms, or reducibility strikes again!
- Intersection type assignment systems
- Typing and computational properties of lambda expressions
- Strong normalization and typability with intersection types
- Explicit Substitutions and Reducibility
- λν, a calculus of explicit substitutions which preserves strong normalisation
- A new type assignment for λ-terms
- Proving termination with multiset orderings
- Extending a λ-calculus with explicit substitution which preserves strong normalisation into a confluent calculus on open terms
- Reductions, intersection types, and explicit substitutions
- Explicit substitutions
- Intensional interpretations of functionals of finite type I
