Nameless, painless
Abstract
De Bruijn indices are a well known technique for programming with names and binders. They provide a representation that is both simple and canonical.
Related papers
- Painless Panes for Smalltalk Windows OOPSLA 1987
- Generic Reasoning of the Locally Nameless Representation APLAS 2024
- Painless programming combining reduction and search: design principles for embedding decision procedures in high-level languages ICFP 2012
- Locally Nameless Sets POPL 2023
- D-Painless: A Framework for Distributed Portfolio SAT Solving TACAS 2025
- An anti-locally-nameless approach to formalizing quantifiers CPP 2021
- Modular and Efficient Divide-and-Conquer SAT Solver on Top of the Painless Framework TACAS 2019
- Intrinsically typed compilation with nameless labels POPL 2021