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.
Bindings as Bounded Natural Functors -- slides from the POPL presentation (slides_BindingsAsBNFs.pdf) | 950KiB |
Wed 16 Jan Times are displayed in time zone: Greenwich Mean Time : Belfast change
Wed 16 Jan
Times are displayed in time zone: Greenwich Mean Time : Belfast change
13:45 - 14:07 Talk | Familial Monads and Structural Operational Semantics Research Papers Tom HirschowitzUniv. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry Link to publication DOI Media Attached File Attached | ||
14:07 - 14:29 Talk | Bindings as Bounded Natural Functors Research Papers Jasmin BlanchetteVrije Universiteit Amsterdam, Lorenzo GheriMiddlesex University London, Andrei PopescuMiddlesex University, London, Dmitriy TraytelETH Zurich Link to publication DOI Media Attached File Attached | ||
14:29 - 14:51 Talk | Categorical Combinatorics of Scheduling and Synchronization in Game Semantics Research Papers Paul-André MelliesCNRS and University Paris Diderot Link to publication DOI Media Attached File Attached |