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.68028OpenAlexW1980174718MaRDI 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
Functional programming and lambda calculus (68N18) Cut-elimination and normal-form theorems (03F05) Combinatory logic and lambda calculus (03B40)
Related Items (6)
Unnamed Item ⋮ Characterising Strongly Normalising Intuitionistic Sequent Terms ⋮ Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) ⋮ A Filter Model for the λμ-Calculus ⋮ Unnamed Item ⋮ Intersection Types for the Resource Control Lambda Calculi
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- 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
This page was built for publication: Characterizing strong normalization in the Curien-Herbelin symmetric lambda calculus: extending the Coppo-Dezani heritage
