Overview
The event has passed
- Date:Starts 1 October 2025, 08:30Ends 1 October 2025, 17:00
- Location:
- Language:English
- Last sign up date:28 August 2025
Prof. Peter Dybjer is a leading researcher in type theory and constructive logic. He is widely recognised among other things for his influential work on inductive families, induction-recursion, and normalisation by evaluation.
After more than 40 years at Chalmers, Peter has now retired and been appointed Professor Emeritus.
To celebrate his lasting contributions we are organising a workshop on October 1st 2025 at Chalmerska huset.
Program
Time | Speaker | Title |
|---|---|---|
| 8:30-9:00 | Coffee | |
| 9:00 | Start of the day program at Poppelmanska room | |
| 9:00-9:15 | Ana and Thierry | Welcome |
| 9:15-10:00 | Xavier Leroy | Sharing is caring: Laziness and concurrency in normalization and convertibility checking |
| 10:00-10:15 | Andras Kovacs | Canonicity for inductive-recursive types |
| 10:15-10:30 | Hugo Moeneclaey | Finitary higher inductive types in the groupoid model |
| 10:30-11:00 | Coffee break | |
| 11:00-11:45 | Pierre Clairambault | The troublesome games model of dependent types |
| 11:45-12:00 | Aarne Ranta | Hikes with Peter |
| 12:00-13:15 | Lunch | |
| 13:15-14:00 | Martín Escardó | An inductive-recursive universe of well-ordered searchable types |
| 14:00-14:15 | Christian Sattler | Categories with families: A short tour |
| 14:15-14:30 | Peter LeFanu Lumsdaine | Categories with families: Thirty years since Skövde |
| 14:30-14:45 | Andreas Abel | The Godfather |
| 14:45-15:30 | Coffee break | |
| 15:30-16:15 | Anton Setzer | Exploration of the predicativity of the Mahlo universe |
| 16:15-17:00 | Marc Bezem | A poem, a carpet, and a tricycle |
| 17:00-17:10 | Andrés Sicard | Greetings from another country |
| 17:10 | End of day program | |
| 17:30 | Start of the evening program at the bank vault | |
| Jan Smith | 44 years ago Peter arrived at Chalmers. What has happened since then? | |
| 18:30-21:00 | Dinner at Marmorsalongen | |
