An abstract framework for environment machines
From MaRDI portal
This paper developes a calculus of classes, i.e. a formalism to handle \(\lambda\)-terms with substitutions. It is shown that machines with environment (Krivine's machine and the CAM) essentially corresponds to different strategies for normalizing closures (call by name, call by value). Simple typed closures are also considered and a categorical point of view is sketched.
Recommendations
Cites work
- A Rewriting System for Categorical Combinators with Multiple Arguments
- Call-by-name, call-by-value and the \(\lambda\)-calculus
- Combinators and functional programming languages. Thirteenth Spring School of the LITP, Val d'Ajol, France, May 6-10, 1985. Proceedings
- Confluence results for the pure strong categorical logic CCL. \(\lambda\)- calculi as subsystems of CCL
- Explicit substitutions
- Full abstraction in the lazy lambda calculus
- scientific article; zbMATH DE number 3811536 (Why is no real title available?)
- scientific article; zbMATH DE number 3959364 (Why is no real title available?)
- scientific article; zbMATH DE number 4048997 (Why is no real title available?)
- scientific article; zbMATH DE number 130889 (Why is no real title available?)
- scientific article; zbMATH DE number 4122189 (Why is no real title available?)
- scientific article; zbMATH DE number 3316072 (Why is no real title available?)
- scientific article; zbMATH DE number 3400430 (Why is no real title available?)
- The categorical abstract machine
- The Mechanical Evaluation of Expressions
Cited in
(28)- Inductive families
- Categorical abstract machines for higher-order typed -calculi
- Simply typed lambda calculus with first-class environments
- On explicit substitution with names
- Explaining the lazy Krivine machine using explicit substitution and addresses
- The next 700 Krivine machines
- State-transition machines, revisited
- CINNI -- a generic calculus of explicit substitutions and its application to -, - and -calculi
- Computational Complexity Via Finite Types
- λν, a calculus of explicit substitutions which preserves strong normalisation
- Inter-deriving Semantic Artifacts for Object-Oriented Programming
- From reduction-based to reduction-free normalization
- scientific article; zbMATH DE number 1342289 (Why is no real title available?)
- On explicit substitutions and names (extended abstract)
- A categorical understanding of environment machines
- Full abstraction for non-deterministic and probabilistic extensions of PCF. I: The angelic cases
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
- Abstract machines, optimal reduction, and streams
- New developments in environment machines
- A concrete framework for environment machines
- A Logical Foundation for Environment Classifiers
- A Logical Foundation for Environment Classifiers
- Optimizing a non-deterministic abstract machine with environments
- Equivalence of eval-readback and eval-apply big-step evaluators by structuring the lambda-calculus's strategy space
- Explicit substitutions and higher-order syntax
- A syntactic correspondence between context-sensitive calculi and abstract machines
- On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion
- Inter-deriving semantic artifacts for object-oriented programming
This page was built for publication: An abstract framework for environment machines
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q804281)
