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
Times are displayed in time zone: Greenwich Mean Time : Belfast change

13:45 - 14:51: CategoriesResearch Papers at Sala II
Chair(s): Nicolas TabareauInria
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