All times are in Boston Local Time, (UTC-4).
| Time | Event |
|---|---|
| 08:15 - 09:00 | Light breakfast |
| 09:20 - 09:25 | Opening remarks |
| 09:25 - 10:10 | Invited talk: Howard Straubing - The Algebra of Finite Categories |
| 10:10 - 10:30 | Lingyuan Ye - Categorical Structure in Theory of Arithmetic (slides) |
| 10:30 - 11:00 | Coffee break |
| 11:00 - 11:20 | Benjamin Merlin Bumpus - Compositional Algorithms on Compositional Data: Deciding Sheaves on Presheaves |
| 11:20 - 11:40 | Rémi Morvan - Algebras for Automatic Relations (slides) |
| 11:40 - 12:00 | Pierre Cagne - GADTs Are Not (Even Lax) Functors (slides) |
| 12:00 - 12:20 | Amin Karamlou - Capturing Quantum Isomorphism in the Kleisli Category of the Quantum Monad (slides) |
| 12:20 - 14:00 | Lunch |
| 14:00 - 14:45 | Invited talk: Alexandra Silva - Guarded KATs – efficient reasoning for algebraic program verification (slides) |
| 14:45 - 15:05 | Mikołaj Bojańczyk - The Category of MSO Transductions |
| 15:05 - 15:25 | Glynn Winskel - Concurrent Games over Relational Structures (slides) |
| 15:25 - 16:00 | Coffee break |
| 16:00 - 16:20 | Ugo Dal Lago - Enumerating Error Bounded Polytime Algorithms Through Arithmetical Theories (slides) |
| 16:20 - 16:40 | Diana Kessler - Higher-Dimensional Subdiagram Matching (slides) |
| 16:40 - 17:00 | Colin Riba - Finitely Accessibly Arboreal Adjunctions and Hintikka Formulae (slides) |
| 17:00 - 17:20 | Vincent Moreau - Profinite λ-terms and Parametricity (slides) |
| 17:20 - 17:40 | Peter Hines - On Conway’s Proof of Undecidability in Elementary Arithmetic (slides) |
Abstracts
Abstracts of the contributed talks can be found in the book of abstracts.
Alexandra Silva - Guarded KATs – efficient reasoning for algebraic program verification
Abstract: Kleene Algebra with Tests (KAT) has been developed over the last three decades as an algebraic framework to reason about program equivalence, refinement, and verification. In this talk, we will provide an overview of recent results characterizing a fragment of KAT in which equivalence can be decided more efficiently. We will then show how this fragment can be extended in different ways to perform domain-specific verification tasks. Based on joint work with Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, Wojtek Rozowski, Todd Schmid, and Steffen Smolka.
Howard Straubing - The Algebra of Finite Categories
Abstract: The algebraic structure of finite semigroups and monoids is among the most useful mathematical tools for determining the expressive power of logics describing the behavior of automata over words. Treating finite categories as algebraic objects emerged in the 1980's as an important method for settling some of the more challenging problems in this domain. In this talk, I will survey the fundamentals of this theory and some of its many applications (both the old ones and much more recent ones). I will also briefly discuss efforts to extend this framework to the study of automata over trees.
