Variable binding and substitution for (nameless) dummies

TL;DR

This paper introduces a simplified theory of syntax with variable binding and capture-avoiding substitution using De Bruijn's nameless dummies, providing a formal link to existing approaches and accommodating simple types and equations.

Contribution

It presents a new, simpler framework for variable binding and substitution that connects to established theories and extends to include simple types and equations.

Findings

Establishes a formal link to Fiore, Plotkin, and Turi's approach

Easily incorporates simple types and equations

Provides a simpler alternative to existing theories

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.