1. Bindings as Bounded Natural Functors
- Author
-
Jasmin Christian Blanchette, Lorenzo Gheri, Dmitriy Traytel, Andrei Popescu, Theoretical Computer Science, Network Institute, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Vrije Universiteit Amsterdam [Amsterdam] (VU), Middlesex University [London], Eidgenössische Technische Hochschule - Swiss Federal Institute of Technology [Zürich] (ETH Zürich), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft
- Subjects
Computer science ,HOL ,0102 computer and information sciences ,02 engineering and technology ,01 natural sciences ,Higher-order logic ,0202 electrical engineering, electronic engineering, information engineering ,Safety, Risk, Reliability and Quality ,Type struc-tures ,Functor ,Higher order logic ,business.industry ,Proof assistant ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,020207 software engineering ,Modular design ,16. Peace & justice ,Syntax ,Theory of computation → Logic and verification ,Algebra ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,010201 computation theory & mathematics ,Bounded function ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,Free variables and bound variables ,business ,Software - Abstract
International audience; 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.
- Published
- 2019
- Full Text
- View/download PDF