The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus
From MaRDI portal
Publication:4972064
DOI10.1017/S0956796819000017zbMath1493.68085OpenAlexW2943029224WikidataQ127959945 ScholiaQ127959945MaRDI QIDQ4972064
Álvaro García-Pérez, Pablo Nogueira
Publication date: 22 November 2019
Published in: Journal of Functional Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1017/s0956796819000017
Related Items (1)
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Combinatory logic. With two sections by William Craig.
- The lambda calculus. Its syntax and semantics. Rev. ed.
- An abstract framework for environment machines
- Needed reduction and spine strategies for the lambda calculus
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- \(\lambda\) to SKI, semantically -- declarative pearl
- Parametric parameter passing \(\lambda\)-calculus
- The locally nameless representation
- Strongly reducing variants of the Krivine abstract machine
- A call-by-name lambda-calculus machine
- Full Reduction in the Face of Absurdity
- The Useful MAM, a Reasonable Implementation of the Strong $$\lambda $$ -Calculus
- Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus
- The duality of computation
- A compiled implementation of strong reduction
- Engineering formal metatheory
- A Theory of Explicit Substitutions with Safe and Full Composition
- A Strong Distillery
- The Theory of Calculi with Explicit Substitutions Revisited
- From Reduction-Based to Reduction-Free Normalization
- Formal verification of parallel programs
- Confluence properties of weak and strong calculi of explicit substitutions
- Explicit substitutions
- Explicit substitutions with de bruijn's levels
- A concrete framework for environment machines
- Theorem Proving in Higher Order Logics
This page was built for publication: The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus