By abstracting over well-known properties of De Bruijn’s representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi’s approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.
Variable binding and substitution for (nameless) dummies / Hirschowitz A.; Hirschowitz T.; Lafont A.; Maggesi M.. - ELETTRONICO. - 13242:(2022), pp. 389-408. (Intervento presentato al convegno 25th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2022, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022 tenutosi a Munich, Germany nel 2022) [10.1007/978-3-030-99253-8_20].
Variable binding and substitution for (nameless) dummies
Maggesi M.
2022
Abstract
By abstracting over well-known properties of De Bruijn’s representation with nameless dummies, we design a new theory of syntax with variable binding and capture-avoiding substitution. We propose it as a simpler alternative to Fiore, Plotkin, and Turi’s approach, with which we establish a strong formal link. We also show that our theory easily incorporates simple types and equations between terms.File | Dimensione | Formato | |
---|---|---|---|
978-3-030-99253-8_20.pdf
accesso aperto
Tipologia:
Pdf editoriale (Version of record)
Licenza:
Open Access
Dimensione
453.47 kB
Formato
Adobe PDF
|
453.47 kB | Adobe PDF |
I documenti in FLORE sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.