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

DOI10.1017/S0956796819000017zbMATH Open1493.68085OpenAlexW2943029224WikidataQ127959945 ScholiaQ127959945MaRDI QIDQ4972064FDOQ4972064

Á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

Recommendations

• Strongly reducing variants of the Krivine abstract machine
• An abstract machine for strong call by value
• The next 700 Krivine machines
• A concrete framework for environment machines
• Abstract λ-Calculus Machines

Mathematics Subject Classification ID

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

Cites Work

• Theorem Proving in Higher Order Logics
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Combinatory logic. With two sections by William Craig.
• The lambda calculus. Its syntax and semantics. Rev. ed.
• Formal verification of parallel programs
• Title not available (Why is that?)
• Types and programing languages
• The duality of computation
• Title not available (Why is that?)
• Engineering formal metatheory
• From reduction-based to reduction-free normalization
• Explicit substitutions with de bruijn's levels
• Title not available (Why is that?)
• A call-by-name lambda-calculus machine
• An abstract framework for environment machines
• Title not available (Why is that?)
• Title not available (Why is that?)
• Parametric parameter passing \(\lambda\)-calculus
• The locally nameless representation
• Explicit substitutions
• Needed reduction and spine strategies for the lambda calculus
• Title not available (Why is that?)
• The Theory of Calculi with Explicit Substitutions Revisited
• Title not available (Why is that?)
• A concrete framework for environment machines
• Title not available (Why is that?)
• Strongly reducing variants of the Krivine abstract machine
• A compiled implementation of strong reduction
• Confluence properties of weak and strong calculi of explicit substitutions
• \(\lambda\) to SKI, semantically -- declarative pearl
• Preservation of strong normalisation modulo permutations for the structural \(\lambda\)-calculus
• A Theory of Explicit Substitutions with Safe and Full Composition
• A Strong Distillery
• The Useful MAM, a Reasonable Implementation of the Strong $$\lambda $$ -Calculus
• Full Reduction in the Face of Absurdity
• Title not available (Why is that?)

Cited In (3)

• Deriving Efficient Sequential and Parallel Generators for Closed Simply-Typed Lambda Terms and Normal Forms
• Formal small-step verification of a call-by-value lambda calculus machine
• Strongly reducing variants of the Krivine abstract machine

Uses Software

• ML
• PoplMark

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4972064)