Reversible, irreversible and optimal -machines

DOI10.1016/S0304-3975(99)00049-3MaRDI QIDQ1575873zbMATH OpenFDO

Authors Vincent Danos, Laurent Regnier

Publication date 23 August 2000

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0304-3975(99)00049-3

zbMATH Keywords

call/return symmetrygeometry of interactioninteraction abstract machineKrivine's abstract machinelambda-calculuslinear head reductionlinear logicreversible computations

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Functional programming and lambda calculus (68N18)

Recommendations

• scientific article; zbMATH DE number 1231514
• Strongly reducing variants of the Krivine abstract machine
• New developments in environment machines
• The next 700 Krivine machines
• Abstract λ-Calculus Machines

Cited in

(34)

• Evaluating lambda terms with traversals
• The graphical Krivine machine
• Explaining the lazy Krivine machine using explicit substitution and addresses
• The next 700 Krivine machines
• A call-by-name lambda-calculus machine
• A structural approach to reversible computation
• Reversibility in the higher-order \(\pi\)-calculus
• A fully labelled lambda calculus: towards closed reduction in the geometry of interaction machine
• Semantics of higher-order quantum computation via geometry of interaction
• A strong distillery
• Abstract λ-Calculus Machines
• scientific article; zbMATH DE number 1231514 (Why is no real title available?)
• On the dynamics of sharing graphs
• An introduction to differential linear logic: proof-nets, models and antiderivatives
• A correspondence between maximal abelian sub-algebras and linear logic fragments
• Lambda and pi calculi, CAM and SECD machines
• The dynamic geometry of interaction machine: a token-guided graph rewriter
• Krivine machine and Taylor expansion in a non-uniform setting
• δο!∈=1 Optimizing optimal λ-calculus implementations
• A Fresh Look at the λ-Calculus
• scientific article; zbMATH DE number 7561616 (Why is no real title available?)
• On the expressivity of linear recursion schemes
• Addressing machines as models of \(\lambda\)-calculus
• Abstract machines, optimal reduction, and streams
• Causal-consistent rollback in a tuple-based language
• New developments in environment machines
• The involutions-as-principal types/application-as-unification analogy
• Musings around the geometry of interaction, and coherence
• Light logics and optimal reduction: completeness and complexity
• (Definitely not) boring interaction abstract machines
• Slightly nonlinear higher-order tree transducers
• Proof nets and the call-by-value \(\lambda\)-calculus
• A syntactic congruence for languages of birooted trees
• Uniformity and the Taylor expansion of ordinary lambda-terms

This page was built for publication: Reversible, irreversible and optimal \(\lambda\)-machines

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