Variable binding and substitution for (nameless) dummies

Autor: André Hirschowitz, Tom Hirschowitz, Ambroise Lafont, Marco Maggesi
Jazyk: angličtina
Rok vydání: 2024
Předmět:
Zdroj: Logical Methods in Computer Science, Vol Volume 20, Issue 1 (2024)
Druh dokumentu: article
ISSN: 1860-5974
DOI: 10.46298/lmcs-20(1:18)2024
Popis: 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.
Databáze: Directory of Open Access Journals