Locally Nameless Sets
summary
Presents a concrete claim and proofs: equational axiomatization of opening and closing (nine axioms, effectively five independent axioms) lets freshness and local closedness be defined algebraically rather than by structural recursion. Builds a shift functor on a category of these sets, shows finitary functors with sums/products have initial algebras that recover standard locally nameless syntax, constructs initial locally nameless sets for each Plotkin binding signature, and proves the category is isomorphic to the topos of finitely supported T_Omega-sets, unifying several prior renaming models.
AI-written summary · about
chapters (7)
- 0:00Start
- 1:50Named, Nameless and Locally Nameless
- 7:27Locally nameless infrastructure
- 11:59A new syntax-independent theory
- 13:31Locally nameless sets
- 18:33The category Lns
- 23:02Summary
related talks
21mSyntax with Shifted Names
26m2-Functoriality of Initial Semantics, and Applications
53mIntroduction to Intuitionistic Type Theory
14mAdequacy for Algebraic Effects Revisited
27mFunctorial Semantics for Partial Theories
11mLocal algebraic effect theories
02h 24mCategory Theory Track
30mDisplayed Monoidal Categories for the Semantics of Linear Logic