Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage

DOI10.1016/j.tcs.2008.01.022zbMath1146.68028MaRDI QIDQ930871

Pierre Lescanne, Silvia Ghilezan, Daniel J. Dougherty

Publication date: 24 June 2008

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2008.01.022

zbMATH Keywords

sequent calculus; classical logic; intersection-types

Mathematics Subject Classification ID

68N18: Functional programming and lambda calculus

03F05: Cut-elimination and normal-form theorems

03B40: Combinatory logic and lambda calculus

Related Items

Unnamed Item, Unnamed Item, Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\), A Filter Model for the λμ-Calculus, Intersection Types for the Resource Control Lambda Calculi, Characterising Strongly Normalising Intuitionistic Sequent Terms

Uses Software

• Forsythe

Cites Work

• Coppo-Dezani types do not correspond to propositional logic
• The lambda calculus. Its syntax and semantics. Rev. ed.
• An extension of basic functionality theory for \(\lambda\)-calculus
• The ``relevance of intersection and union types
• Normalization without reducibility
• Intersection and union types: Syntax and semantics
• A symmetric lambda calculus for classical program extraction
• A lattice-theoretical fixpoint theorem and its applications
• From Polyvariant flow information to intersection and union types
• Why the usual candidates of reducibility do not work for the symmetric $\lambda\mu$-calculus
• A new type assignment for λ-terms
• A filter lambda model and the completeness of type assignment
• Tridirectional typechecking
• Normalization as a homomorphic image of cut-elimination
• Principal Type Schemes for the Strict Type Assignment System
• A calculus with polymorphic and polyvariant flow types
• Symmetry and Interactivity in Programming
• Hyperformulae, Parallel Deductions and Intersection Types
• Lambda terms for natural deduction, sequent calculus and cut elimination
• Call-by-value is dual to call-by-name
• Foundations of Software Science and Computation Structures
• Strong Normalization of the Dual Classical Sequent Calculus
• Term Rewriting and Applications
• Typed Lambda Calculi and Applications
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item