Syntax with Shifted Names
summary
Claims a new representation called shifted names that tags free names with numeric indices so freshness side-conditions disappear. Defines four concrete operations open/close/weak/bind with equations (open then close = id, weaken then bind = id) and shows renaming, substitution, weakening and equivariance lemmas become direct. Formal development is formalized in Coq and used to prove a CPS conversion preservation lemma without freshness side-conditions; prototype works but naive eager shifting would be slow in a compiler.
AI-written summary · about
chapters (10)
- 0:00Avoiding capture
- 1:21Some good ideas
- 3:53open and close
- 5:42Shifted Names
- 7:31wk and bind
- 8:57Four basic operations
- 9:51Derived operations
- 12:00Parallel operations
- 12:34Equivariance lemma
- 13:46Substitution lemma
related talks
25mLocally Nameless Sets
29mA Typed and Unified Reflection for Shift and Shift0
25mIntrinsically Typed Compilation with Nameless Labels
12mOn the power of syntactic methods: It is all syntax after all…
14mAdequacy for Algebraic Effects Revisited
28mTowards Light-Weight Operational Reasoning for Languages with Binders, Categorically
18mA Simple and Efficient Implementation of Strong Call by Need by an Abstract Ma…
28mFirst-class Names for Effect Handlers