An abstract framework for environment machines

DOI10.1016/0304-3975(91)90230-YzbMath0727.68033MaRDI QIDQ804281

Pierre-Louis Curien

Publication date: 1991

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

zbMATH Keywords

\(\lambda \) -calculusenvironment machines

Mathematics Subject Classification ID

Related Items (21)

Inductive families ⋮ Unnamed Item ⋮ Simply typed lambda calculus with first-class environments ⋮ Categorical abstract machines for higher-order typed \(\lambda\)-calculi ⋮ Explicit substitutions and higher-order syntax ⋮ On explicit substitution with names ⋮ On explicit substitutions and names (extended abstract) ⋮ A syntactic correspondence between context-sensitive calculi and abstract machines ⋮ Computational Complexity Via Finite Types ⋮ Abstract machines, optimal reduction, and streams ⋮ Inter-deriving Semantic Artifacts for Object-Oriented Programming ⋮ Full abstraction for non-deterministic and probabilistic extensions of PCF. I: The angelic cases ⋮ Explaining the lazy Krivine machine using explicit substitution and addresses ⋮ The next 700 Krivine machines ⋮ State-transition machines, revisited ⋮ On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion ⋮ New Developments in Environment Machines ⋮ Inter-deriving semantic artifacts for object-oriented programming ⋮ The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus ⋮ From Reduction-Based to Reduction-Free Normalization ⋮ λν, a calculus of explicit substitutions which preserves strong normalisation

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
• Combinators and functional programming languages. Thirteenth Spring School of the LITP, Val d'Ajol, France, May 6-10, 1985. Proceedings
• The categorical abstract machine
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Full abstraction in the lazy lambda calculus
• A Rewriting System for Categorical Combinators with Multiple Arguments
• Explicit substitutions
• The Mechanical Evaluation of Expressions

This page was built for publication: An abstract framework for environment machines