A Case for First-Class Environments
summary
Argues that a small-step environment-based semantics replaces substitution and yields λE, a call-by-value, statically typed calculus using de Bruijn indices that exposes first-class environments as language values. Formalization and proofs are mechanized in Coq, an abstract machine is derived with an easy correctness proof, references and a simple first-class module encoding are added, and λE is shown to be a conservative extension of STLC with simpler progress/preservation proofs and reproducible artifacts.
AI-written summary · about
chapters (11)
- 0:00Substitution model drawbacks
- 1:05Alternatives to substitution
- 2:30First-class environments defined
- 3:16Small-step semantics
- 4:40First-class environment ops
- 5:45First-class modules with caps
- 8:00Core calculus with envs
- 10:13Operational correspondence
- 12:19Type safety proof
- 13:46Formalization & comparisons
- 14:31Q&A
related talks
15mStable Relations and Abstract Interpretation of Higher-Order Programs
14mType-Sensitive Algebraic Macros
24mScoped and Typed Staging by Evaluation
19mExtensible Metatheory Mechanization via Family Polymorphism
31mPyrosome: A Framework for Modular, Extensible, Equivalence-Preserving Compilati...
24mAn Intrinsically-typed Probabilistic Programming Language in Coq (Extended Abstr...
29mExplicit Refinement Types
20mCoq a la Carte: A Practical Approach to Modular Syntax With Binders