Abstracting models of strong normalization for classical calculi
DOI10.1016/j.jlamp.2019.100512zbMath1494.68055OpenAlexW2995413974WikidataQ126532454 ScholiaQ126532454MaRDI QIDQ2291828
Paul Downen, Philip Johnson-Freyd, Zena M. Ariola
Publication date: 31 January 2020
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://www.osti.gov/biblio/1595425
Functional programming and lambda calculus (68N18) Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Combinatory logic and lambda calculus (03B40)
Related Items (2)
Cites Work
- Unnamed Item
- Unnamed Item
- Linear logic
- The parametric lambda calculus. A metamodel for computation.
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- A syntactic approach to type soundness
- Realizability interpretation and normalization of typed call-by-need \(\lambda\)-calculus with control
- A call-by-name lambda-calculus machine
- Classical \(F_{\omega}\), orthogonality and symmetric candidates
- Why the usual candidates of reducibility do not work for the symmetric $\lambda\mu$-calculus
- The duality of computation
- Structures for structural recursion
- Classical Call-by-Need and Duality
- The Duality of Computation under Focus
- An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
- Focalisation and Classical Realisability
- Parametric polymorphism and operational equivalence
- Call-by-value is dual to call-by-name
- The Duality of Construction
- Intensional interpretations of functionals of finite type I
- Uniform strong normalization for multi-discipline calculi
This page was built for publication: Abstracting models of strong normalization for classical calculi