Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
From MaRDI portal
Publication:930871
DOI10.1016/j.tcs.2008.01.022zbMath1146.68028MaRDI QIDQ930871
Silvia Ghilezan, Pierre Lescanne, 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
68N18: Functional programming and lambda calculus
03F05: Cut-elimination and normal-form theorems
03B40: Combinatory logic and lambda calculus
Related Items
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
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