The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus

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

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Related Items (1)

Deriving Efficient Sequential and Parallel Generators for Closed Simply-Typed Lambda Terms and Normal Forms

Uses Software

• ML
• PoplMark

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