skip to content

Department of Computer Science and Technology

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 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.