Jeremy-y: Created page with "'''Thinning-stable metaprogramming''' ''András Kovács'' In this talk I give an overview of various notions of stability in metaprogramming and propose stability under thinning as a setup which shows some promise and which has not yet been explored. When we have "f : Code a -> Code b" in some staged language, we expect "f" to work on object expressions in arbitrary scopes. So, semantically we'd like to have "∀ Γ. Code Γ a → Code Γ b". However, functions of suc..."

2026-10-07T08:07:44Z

Created page with "'''Thinning-stable metaprogramming''' ''András Kovács'' In this talk I give an overview of various notions of stability in metaprogramming and propose stability under thinning as a setup which shows some promise and which has not yet been explored. When we have "f : Code a -> Code b" in some staged language, we expect "f" to work on object expressions in arbitrary scopes. So, semantically we'd like to have "∀ Γ. Code Γ a → Code Γ b". However, functions of suc..."

New page

'''Thinning-stable metaprogramming'''

''András Kovács''

In this talk I give an overview of various notions of stability in metaprogramming and propose stability under thinning as a setup which shows some promise and which has not yet been explored. When we have "f : Code a -> Code b" in some staged language, we expect "f" to work on object expressions in arbitrary scopes. So, semantically we'd like to have "∀ Γ. Code Γ a → Code Γ b". However, functions of such type can inspect Γ in arbitrary unhygienic ways. So we'd like to restrict ourselves to metaprograms that are stable under certain morphisms between object-level scopes. Previous works have explored stability under a) substitution b) variable renaming c) injective variable renaming, in various logical frameworks and nominal and staged calculi. I investigate stability under thinning (also known as order-preserving embedding).

WG211/M26Kovacs - Revision history