Intersection Types for the Resource Control Lambda Calculi

DOI10.1007/978-3-642-23283-1_10zbMath1351.03008MaRDI QIDQ3105748

Silvia Ghilezan, Pierre Lescanne, Silvia Likavec, Jelena Ivetić

Publication date: 6 January 2012

Published in: Theoretical Aspects of Computing – ICTAC 2011 (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/2318/135234

Mathematics Subject Classification ID

03B40: Combinatory logic and lambda calculus

Uses Software

• Automath
• CRSX

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Computational interpretations of linear logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Resource operators for \(\lambda\)-calculus
• Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
• An extension of basic functionality theory for \(\lambda\)-calculus
• Complete restrictions of the intersection type discipline
• Typing untyped \(\lambda\)-terms, or reducibility strikes again!
• An equivalence between lambda- terms
• Behavioural inverse limit \(\lambda\)-models
• A symmetric lambda calculus for classical program extraction
• Strong normalization and typability with intersection types
• The duality of computation
• Intuitionistic Sequent-Style Calculus with Explicit Structural Rules
• The Prismoid of Resources
• A new type assignment for λ-terms
• A filter lambda model and the completeness of type assignment
• Solvability in Resource Lambda-Calculus
• Completing Herbelin’s Programme
• Term Rewriting and All That
• Characterising Strongly Normalising Intuitionistic Terms
• Simple Proofs of Characterizing Strong Normalization for Explicit Substitution Calculi
• Intensional interpretations of functionals of finite type I
• THEORETICAL PEARLS: A bargain for intersection types: a simple strong normalization proof