Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Wed 16 Jan 2019 14:07 - 14:29 at Sala II - Categories Chair(s): Nicolas Tabareau

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

13:45 - 14:51: Research Papers - Categories at Sala II
Chair(s): Nicolas TabareauInria
POPL-2019-Research-Papers13:45 - 14:07
Tom HirschowitzUniv. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry
Link to publication DOI File Attached
POPL-2019-Research-Papers14:07 - 14:29
Jasmin Christian BlanchetteVrije Universiteit Amsterdam, Lorenzo GheriMiddlesex University London, Andrei PopescuMiddlesex University, London, Dmitriy TraytelETH Zurich
Link to publication DOI File Attached
POPL-2019-Research-Papers14:29 - 14:51
Paul-André MelliesCNRS and University Paris Diderot
Link to publication DOI File Attached