On September 20, 2024, we are organizing a small workshop on Theoretical Computer Science. The workshop will precede the PhD defense of Joseph Paulus.
Location
The workshop will take place in the Academy Building, in the city center (Google maps).
Talks will take place at the Senaatskamer (first floor)
Coffee break and Lunch will take place at the Bruinzaal.
Workshop Program
(Last updated: September 12, 2024)
8:50 - 9:00: Welcome (Senaatskamer)
9:00 - 9:40: Talk 1: Simon Gay (Glasgow): Trains, Pictures and Types
Abstract:
We present an embedded domain-specific language (EDSL) for drawing diagrams of model railway layouts, and see how a dependent type system can check that layouts join up smoothly without self-intersection. We implement this EDSL in Idris with the Open2GL library. The result is a novel and visually appealing introduction to some of the key principles of dependently typed programming.
9:40 - 10:10: Talk 2: Juan C. Jaramillo (Groningen): Around Classical and Intuitionistic Linear Processes
Abstract:
Curry-Howard correspondences between Linear Logic (LL) and session types provide a firm foundation for concurrent processes. As the correspondences hold for intuitionistic and classical versions of LL (ILL and CLL), we obtain two different families of type systems for concurrency. An open question remains: how do these two families exactly relate to each other? Based upon a translation from CLL to ILL due to Laurent, we provide two complementary answers, in the form of full abstraction results based on a typed observational equivalence due to Atkey. Our results elucidate hitherto missing formal links between seemingly related yet different type systems for concurrency.
(based on joint work with Dan Frumin and Jorge Pérez, presented at CONCUR'24)
10:10 - 10:20: Coffee Break (Bruinzaal)
10:20 - 11:00: Talk 3: Herman Geuvers (Nijmegen): Initial algebras and terminal coalgebras as inductive and coinductive types
Abstract:
Joint work with Steven Bronsveld and Niels van der Weide
In type theory, inductive types are meant to model initial algebras and coinductive types are meant to model terminal coalgebras, for some chosen functor F. By choosing F appropriately we can thereby interpret (inductive) data types like natural numbers, lists, trees and (coinductive) data-types like streams. For the inductive types
one expects to get a "function definition principle" (to define functions by well-founded recursion) and a "induction proof principle". Similarly, for coinductive types one expects a "guarded recursion principle" (to define infinitary objects by guarded recursion) and a "coinduction proof principle" (saying that equality of infinite objects coincides with bisimilarity).
In the talk we first discuss how exactly these expectations become manifest in type theory in case the inductive types really behave as initial algebras (and the coinductive types as terminal coalgebras). This seems to be folklore: how to get the induction principle from initiality (and the dual), but we haven't found a
reference. Then we look at polymorphic type theory (Girard's system F), where inductive (and coinductive) types are definable, but it is well-known that they are to weak: they are only "weakly initial algebras" which makes that, e.g. the induction principle for natural numbers is not derivable. Recently it has been shown by Awodey, Frey and Speight (LiCS 2018) that if one adds a few principles (that arise naturally in Homotopy Type Theory), initial algebras can be defined in polymorphic type theory. In the talk we will discuss the approach of Awodey et al and how it generalises to terminal coalgebras.
11:00 - 11:30: Talk 4: Anton Chernev (Groningen): A Categorical Representation of Thin Trees
Abstract:
Infinite trees with countably many branches, called thin trees, have been studied via methods from automata theory and algebra. We take a categorical approach to thin trees using the framework of coalgebra. We show that the collection of thin trees can be seen as an initial algebra satisfying a certain axiom. We prove this by defining an algebra of thin tree representatives and showing that each thin tree has a canonical representative.