Variable binding and substitution for (nameless) dummies

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...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2024-02
Main Authors: Hirschowitz, André, Hirschowitz, Tom, Lafont, Ambroise, Maggesi, Marco
Format: Article
Language:English
Subjects:
Binding
Dummies
Substitutes
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422
DOI:10.48550/arxiv.2209.02614