A call-by-name lambda-calculus machine

DOI10.1007/s10990-007-9018-9zbMath1130.68057OpenAlexW2040871029MaRDI QIDQ2464723

Jean-Louis Krivine

Publication date: 17 December 2007

Published in: Higher-Order and Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10990-007-9018-9

zbMATH Keywords

Curry-Howard correspondenceControl instructionLambda-calculus machine

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Combinatory logic and lambda calculus (03B40)

Related Items (27)

Systematic abstraction of abstract machines ⋮ Unnamed Item ⋮ An introduction to differential linear logic: proof-nets, models and antiderivatives ⋮ Execution time of λ-terms via denotational semantics and intersection types ⋮ Automating the functional correspondence between higher-order evaluators and abstract machines ⋮ Classical (co)recursion: Mechanics ⋮ Classical realizability and arithmetical formulæ ⋮ Simply typed fixpoint calculus and collapsible pushdown automata ⋮ Call-by-name extensionality and confluence ⋮ Unnamed Item ⋮ Linear dependent types in a call-by-value scenario ⋮ Krivine machines and higher-order schemes ⋮ Geometry of resource interaction and Taylor–Ehrhard–Regnier expansion: a minimalist approach ⋮ Uniformity and the Taylor expansion of ordinary lambda-terms ⋮ Classical realizability in the CPS target language ⋮ Proving correctness of a compiler using step-indexed logical relations ⋮ Krivine Machines and Higher-Order Schemes ⋮ On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion ⋮ A verified framework for higher-order uncurrying optimizations ⋮ Evaluating lambda terms with traversals ⋮ ASMs and Operational Algorithmic Completeness of Lambda Calculus ⋮ A Classical Realizability Model for a Semantical Value Restriction ⋮ Classical By-Need ⋮ Abstracting models of strong normalization for classical calculi ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ Quantitative classical realizability ⋮ Soft Linear Logic and Polynomial Complexity Classes

Cites Work

• A syntactic correspondence between context-sensitive calculi and abstract machines
• Dependent choice, `quote' and the clock
• The Mechanical Evaluation of Expressions
• Typed lambda-calculus in classical Zermelo-Fraenkel set theory
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A call-by-name lambda-calculus machine