An Operational Account of Call-by-Value Minimal and Classical λ-Calculus in “Natural Deduction” Form
From MaRDI portal
Publication:3637192
DOI10.1007/978-3-642-02273-9_12zbMath1246.03030OpenAlexW1839102226MaRDI QIDQ3637192
Hugo Herbelin, Stéphane Zimmermann
Publication date: 7 July 2009
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-02273-9_12
Related Items
Open Call-by-Value ⋮ Proof nets and the call-by-value \(\lambda\)-calculus ⋮ Head reduction and normalization in a call-by-value lambda-calculus ⋮ Classical Call-by-Need and Duality ⋮ Abstracting models of strong normalization for classical calculi ⋮ A Fresh Look at the λ-Calculus ⋮ On reduction and normalization in the computational core
Cites Work
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- An equivalence between lambda- terms
- λμ-calculus and Böhm's theorem
- A reflection on call-by-value
- The duality of computation
- Control reduction theories: the benefit of structural substitution
- Sound and complete axiomatisations of call-by-value control operators
- From Böhm's Theorem to Observational Equivalences
- Unnamed Item
- Unnamed Item