Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order

We derive by program transformation Pierre Crégut's full-reducing Krivine machine KN from the structural operational semantics of the normal order reduction strategy in a closure-converted pure lambda calculus. We thus establish the correspondence between the strategy and the machine, and showcase our technique for deriving full-reducing abstract machines. Actually, the machine we obtain is a slightly optimised version that can work with open terms and may be used in implementations of proof assistants.

• Publication year

  2013

• Venue

  ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming

• Publication date

  2013-09-16

• Fields of study

  Mathematics, Computer Science

• Identifiers
  DOI 10.1145/2505879.2505887
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• On the syntactic and functional correspondence between hybrid (or layered) normalisers and abstract machines

  2014cited by this paper
• A syntactic and functional correspondence between full-reducing normalisers and full-reducing abstract machines

  2013cited by this paper
• A syntactic and functional correspondence between reduction semantics and reduction-free full normalisers

  2013cited by this paper
• Interpretations of the gradually-typed lambda calculus

  2012cited by this paper
• Under consideration for publication in Math. Struct. in Comp. Science Towards Böhm trees for lambda-value: the

  2012cited by this paper
• From Mathematics to Abstract Machine: A formal derivation of an executable Krivine machine

  2012cited by this paper
• A walk in the semantic park

  2011cited by this paper
• The Lambda Calculus

  2009cited by this paper
• Strongly reducing variants of the Krivine abstract machine

  2007cited by this paper
• The Theory of Calculi with Explicit Substitutions Revisited

  2007cited by this paper
• Lightweight fusion by fixed point promotion

  2007cited by this paper
• A concrete framework for environment machines

  2005cited by this paper
• An Operational Foundation for Delimited Continuations in the CPS Hierarchy

  2005cited by this paper
• From Reduction-based to Reduction-free Normalization

  2004cited by this paper
• A structural approach to operational semantics

  2004cited by this paper
• A functional correspondence between evaluators and abstract machines

  2003cited by this paper
• A compiled implementation of strong reduction

  2002cited by this paper
• The essence of computation: complexity, analysis, transformation

  2002cited by this paper
• Demonstrating Lambda Calculus Reduction

  2001cited by this paper
• ML for the working programmer (2. ed.)

  1996cited by this paper
• A Combinatory Logic

  1995cited by this paper
• BOOK REVIEW: ML for the Working Programmer by Laurence C. Paulson: (Cambridge University Press, 429 pp., 1991)

  1992cited by this paper
• An Abstract Framework for Environment Machines

  1991cited by this paper
• An abstract machine for Lambda-terms normalization

  1990cited by this paper
• Explicit substitutions

  1989cited by this paper
• Natural Semantics

  1987cited by this paper
• The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages

  1987cited by this paper
• Categorical Combinators

  1986influential reference
• The Lambda Calculus: Its Syntax and Semantics

  1985cited by this paper
• Call-by-Name, Call-by-Value and the lambda-Calculus

  1975cited by this paper
• The Mechanical Evaluation of Expressions

  1964cited by this paper
• Íòòòö Óò××××öøøóò Óö Ôùùðð Blockinøøóò Ò Ååøøº Ëøöù Blockinøº Ò Óñôº Ë Blockin Blockin Blockinò Çôööøøóòòð ×ô Blockinø× Óó Íòøýô Aeóöññððþþøøóò Ý Úðùùøøóò

  year unknowncited by this paper

• A Diamond Machine For Strong Evaluation

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

  2019influential citation
• Crumbling Abstract Machines

  2019cites this paper
• Abstract machines for Open Call-by-Value

  2019cites this paper
• Pattern Matching and Fixed Points: Resource Types and Strong Call-By-Need: Extended Abstract

  2018cites this paper
• The Maximal MAM, a Reasonable Implementation of the Maximal Strategy

  2017cites this paper
• Implementing Open Call-by-Value (Extended Version)

  2017cites this paper
• Implementing Open Call-by-Value

  2017cites this paper
• Foundations of strong call by need

  2017cites this paper
• The Useful MAM, a Reasonable Implementation of the Strong λ-Calculus

  2016cites this paper
• A Strong Distillery

  2015cites this paper
• PhD Abstracts

  2015cites this paper
• Operational Aspects of Full Reduction in Lambda Calculi

  2014influential citation
• On the syntactic and functional correspondence between hybrid (or layered) normalisers and abstract machines

  2014cites this paper
• Deriving interpretations of the gradually-typed lambda calculus

  2014influential citation
• Optimizing a Non-Deterministic Abstract Machine with Environments

  year unknowncites this paper