TY - JOUR
T1 - Bindings as bounded natural functors
AU - Blanchette, Jasmin Christian
AU - Gheri, Lorenzo
AU - Popescu, Andrei
AU - Traytel, Dmitriy
PY - 2019/1
Y1 - 2019/1
N2 - We present a general framework for specifying and reasoning about syntax with bindings. Abstract binder types are modeled using a universe of functors on sets, subject to a number of operations that can be used to construct complex binding patterns and binding-aware datatypes, including non-well-founded and infinitely branching types, in a modular fashion. Despite not committing to any syntactic format, the framework is "concrete" enough to provide definitions of the fundamental operators on terms (free variables, alpha-equivalence, and capture-avoiding substitution) and reasoning and definition principles. This work is compatible with classical higher-order logic and has been formalized in the proof assistant Isabelle/HOL.
AB - We present a general framework for specifying and reasoning about syntax with bindings. Abstract binder types are modeled using a universe of functors on sets, subject to a number of operations that can be used to construct complex binding patterns and binding-aware datatypes, including non-well-founded and infinitely branching types, in a modular fashion. Despite not committing to any syntactic format, the framework is "concrete" enough to provide definitions of the fundamental operators on terms (free variables, alpha-equivalence, and capture-avoiding substitution) and reasoning and definition principles. This work is compatible with classical higher-order logic and has been formalized in the proof assistant Isabelle/HOL.
UR - https://dl.acm.org/toc/pacmpl/2019/3/POPL
U2 - 10.1145/3290335
DO - 10.1145/3290335
M3 - Article
SN - 2475-1421
VL - 3
SP - 1
EP - 34
JO - Proceedings of the ACM on Programming Languages
JF - Proceedings of the ACM on Programming Languages
IS - POPL
M1 - 22
ER -