Post #2777173
2026-05-21 15:26 UTC
does anyone know why Fiore-Plotkin-Turi in 'Abstract Syntax and Variable Binding' (https://doi.org/10.1109/LICS.1999.782615) & subsequent works study algebraic structures on *sets* of types rather than *categories*?
Replies (3)
-
@mc@mathstodon.xyz 2026-05-21 15:38
to be precise, their 'substitution algebras' are for F-sets, where F is finite sets = free cocartesian category on a single generator.
-
@olynch@mathstodon.xyz 2026-05-21 15:33
@mc@mathstodon.xyz It's actually important to have a *set* of types in order to model definitional equality.
-
@mathemagical@mathstodon.xyz 2026-05-21 18:39
@mc@mathstodon.xyz is there a follow-up paper that you recommend that talks about multiple variable binding and nested binding contexts? (e.g. local variable shadowing/aliasing whether in an imperative or functional language)