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

DOI10.1017/S0956796819000017MaRDI QIDQ4972064zbMATH OpenOpenAlexWikidataFDO

Authors Á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)

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

Cites work

• scientific article; zbMATH DE number 2185670 (Why is no real title available?)
• scientific article; zbMATH DE number 4035108 (Why is no real title available?)
• scientific article; zbMATH DE number 4048997 (Why is no real title available?)
• scientific article; zbMATH DE number 1142317 (Why is no real title available?)
• scientific article; zbMATH DE number 1953288 (Why is no real title available?)
• scientific article; zbMATH DE number 1521621 (Why is no real title available?)
• scientific article; zbMATH DE number 194911 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• scientific article; zbMATH DE number 958048 (Why is no real title available?)
• A Theory of Explicit Substitutions with Safe and Full Composition
• A call-by-name lambda-calculus machine
• A compiled implementation of strong reduction
• A concrete framework for environment machines
• A strong distillery
• An abstract framework for environment machines
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Combinatory logic. With two sections by William Craig.
• Confluence properties of weak and strong calculi of explicit substitutions
• Engineering formal metatheory
• Explicit substitutions
• Explicit substitutions with de bruijn's levels
• Formal verification of parallel programs
• From reduction-based to reduction-free normalization
• Full Reduction in the Face of Absurdity
• Needed reduction and spine strategies for the lambda calculus
• Parametric parameter passing \(\lambda\)-calculus
• Preservation of strong normalisation modulo permutations for the structural -calculus
• Strongly reducing variants of the Krivine abstract machine
• The Theory of Calculi with Explicit Substitutions Revisited
• The duality of computation
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The locally nameless representation
• The useful MAM, a reasonable implementation of the strong -calculus
• Theorem Proving in Higher Order Logics
• Types and programing languages
• \(\lambda\) to SKI, semantically -- declarative pearl

Cited in

(5)

• Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
• Deriving efficient sequential and parallel generators for closed simply-typed lambda terms and normal forms
• Optimizing a non-deterministic abstract machine with environments
• Strongly reducing variants of the Krivine abstract machine
• Formal small-step verification of a call-by-value lambda calculus machine

Describes a project that uses

Uses Software

• PoplMark
• ML

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)