Intersection types for explicit substitutions

DOI10.1016/j.ic.2003.09.004zbMath1082.68014OpenAlexW1993809637MaRDI QIDQ1887145

Dan Dougherty, Stéphane Lengrand, Steffen van Bakel, Pierre Lescanne, Mariangiola Dezani-Ciancaglini

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

zbMATH Keywords

Strong normalizationIntersection typesCalculi of explicit substitutions

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Related Items (6)

Nominal essential intersection types ⋮ A resource aware semantics for a focused intuitionistic calculus ⋮ Resource operators for \(\lambda\)-calculus ⋮ Characterising Strongly Normalising Intuitionistic Sequent Terms ⋮ Computation with classical sequents ⋮ Calculi, types and applications: essays in honour of M. Coppo, M. Dezani-Ciancaglini and S. Ronchi della Rocca

Uses Software

• Automath

Cites Work

• 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
• 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

This page was built for publication: Intersection types for explicit substitutions