ProgLog /
StockholmGoteborgMeeting181212
Stockholm–Göteborg meeting on Wednesday, 12 December 2018 in Göteborg
Program
| Time | Speaker | Title |
|---|---|---|
| 11:30–12:15 | Erik Palmgren | A setoid model of extensional Martin-Löf type theory in Agda |
| lunch | ||
| 13:15–13:45 | Thierry Coquand | A remark on sheaf models of type theory |
| 13:45–14:15 | Andreas Abel | Lessons learnt from implementing a runnable well-typed interpreter for C-- in Agda |
| 14:15–15:00 | Menno de Boer | The gluing construction for path categories |
| fika | ||
| 15:30–15:50 | Peter LeFanu Lumsdaine | A Coq formalisation of the initiality conjecture |
| 15:50–16:30 | Guillaume Brunerie | An Agda formalization of the initiality conjecture |
| 16:30–17:15 | Hugo Moeneclaey | Finitary higher inductive types in the groupoid model |
| 18:00 | dinner |