Bindings as Bounded Natural Functors

Jasmin Christian Blanchette (1, 2, 3, 4) , Lorenzo Gheri (5) , Andrei Popescu (5) , Dmitriy Traytel (6)

1 MPII - Max-Planck-Institut für Informatik
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
3 LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
4 VU - Vrije Universiteit Amsterdam [Amsterdam]
5 Middlesex University [London]
6 ETH Zürich - Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich]

the Romanian Academy, Romania DMITRIY TRAYTEL, ETH Zürich, Switzerland 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.

Mots clés: Theory of computation → Logic and verification; Higher order logic; Type struc-tures

Domaines: Logique en informatique [cs.LO]

Jasmin Christian Blanchette, Lorenzo Gheri, Andrei Popescu, Dmitriy Traytel. Bindings as Bounded Natural Functors. Proceedings of the ACM on Programming Languages, 2019, 3 (POPL), pp.1-34. ⟨10.1145/3290335⟩. ⟨hal-01989726⟩