Variable binding and substitution for (nameless) dummies
Logic in Computer Science
2024-08-07 v6
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.
Cite
@article{arxiv.2209.02614,
title = {Variable binding and substitution for (nameless) dummies},
author = {André Hirschowitz and Tom Hirschowitz and Ambroise Lafont and Marco Maggesi},
journal= {arXiv preprint arXiv:2209.02614},
year = {2024}
}