Fall 2020

- Sept 8: Severin Mejak: Topos models of set-theoretic principles (Severin)
- Sept 22: Coquand, Mannaa and Ruch: Stack semantics of type theory (Magnus)
- Sept 29: Coquand, Ruch and Sattler: Constructive sheaf models of type theory (Magnus)
- Oct 6: Licata and Weaver: A Constructive Model of Directed Univalence in Bicubical Sets?
- Oct 20: Hofmann: Semantical Analysis of Higher-Order Abstract Syntax (Andrea)
- Oct 27: Pientka et al: Cocon: Computation in Contextual Type Theory (Carsten)
- Nov 3: Pientka and Schöpp: Semantical Analysis of Contextual Types (Andrea)
- Nov 10: Plotkin and Power: Notions of Computation Determine Monads (Rasmus)
- Nov 17: Bauer and Pretnar: Programming with Algebraic Effects and Handlers (Patrick)
- Nov 24: Ahman, Ghani and Plotkin. Dependent Types and Fibred Computational Effects (Rasmus)
- Dec 1: Fu, Kishida and Selinger: Linear Dependent Type Theory for Quantum Programming Languages (?)

Fall 2019

- Sep 11, 13-15 (2A18): Orton and Pitts: Axioms for Modelling Cubical Type Theory in a Topos (Magnus)
- Sep 18, 13-15 (2A18): Sterling and Spitters: Normalisation by gluing for free lambda-theories (Andrea)
- Sep 25, 13-15 (2A18): Gratzer, Sterling and Birkedal: Implementing a modal dependent type theory (Patrick)
- Oct 1, 10-12 (3A18): Coquand, Huber and Sattler: Homotopy canonicity for cubical type theory (Rasmus)
- Oct 31, 14-16 (4A54): A judgmental reconstruction of modal logic and Contextual Modal Type Theory (Carsten)
- Nov 7, 14-16 (4A54): Modal Dependent Type Theory and Dependent Right Adjoints (Rasmus)
- Nov 14, 14-16 (4A54): Propositional lax logic (Carsten)
- Nov 21, 14-16 (2A20): Quantitative program reasoning with graded modal types (Patrick)
- Nov 28, 14-16 (4A54): The Syntax and Semantics of Quantitative Type Theory
- Dec 5, 14-16 (2A20): Christian Sattler: Higher categorical structure in HoTT
- Dec 12, 13-15 (2A20): Towards a constructive simplicial model of Univalent Foundations (Magnus)

Spring 2019

This semester we meet Wednesdays 10-12 at various locations at ITU

- March 20: Type-driven Development of Concurrent Communicating Systems (Patrick, 2A08)
- March 27: Cancelled (3A20)
- April 10: Interactive Programming in Agda – Objects and Graphical User Interfaces (Christian, 2A20)
- April 24: Wellfounded Recursion with Copatterns and Sized Types (Andrea, 2A20)
- May 1: Modalities, Cohesion, and Information Flow (Rasmus, 2A20)
- May 8: Brouwer’s fixed-point theorem in real-cohesive homotopy type theory (Magnus, 2A20)
- May 15: Same as above, continued (3A20)
- May 22: Modalities in homotopy type theory (3A08)
- May 29: Continued (3A20)
- June 5: Continued (3A20)

Fall 2018

- Sep 17, 24 and Oct 1: Iris from the ground up (Jonas)
- Oct 29 and Nov 5: RustBelt: Securing the Foundations of the Rust Programming Language (Jesper)

Spring 2018

- Feb 23: Guarded Cubical Type Theory (Rasmus) in 4A20
- Mar 2 and 9: The clocks they are adjunctions (Bassel) in 4A54
- Mar 16: HoTT book chapter 6 (Christian)
- Mar 23: Coquand, Huber and Mortberg: On higher inductive types in cubical type theory (Niccolo)
- Apr 13: Frumin, Geuvers, Gondelman and van der Weide: Finite Sets in Homotopy Type Theory (Niccolo)
- Apr 20: Kristina Sojakova: Higher inductive types as homotopy initial algebras (Patrick)
- May 4: Licata, Orton, Pitts and Spitters: Internal Universes in Models of Homotopy Type Theory (Bassel)
- May 25: Sterling and Harper: Guarded Computational Type Theory (Rasmus)

Fall 2017

- Sept 21, 28 and Oct 5: Huber thesis chapter 2 and 3 (Bassel)
- Oct 12, Nov 9, 16 and 23: Huber thesis chapter 6 (Niccolo)
- Nov 30: Huber thesis chapter 7 (Christian)
- Dec 7: Guarded cubical type theory (Bassel).

Spring 2017

- Feb 9. The topos of trees and guarded recursion. First 17 slides of these slides. (Rasmus)
- Feb 15. Seely: Locally cartesian closed categories and type theory and Awodey, Category Theory, chapter 8.7 and 9.7. (Rasmus)
- Feb 22. Simon Huber: Cubical interpretation of type theory (PhD thesis) chapter 1. Alternative source: Martin Hofmann: Syntax and semantics of dependent types (Marie)
- Mar 1.Huber chapter 1 continued (Marie) and a bit of universes in locally cartesian closed categories (Rasmus)
- Mar 8. Robert Atkey and Conor McBride: Productive coprogramming with guarded recursion (Christian)
- Mar 15. Bizjak et al: Guarded dependent type theory with coinductive types (Patrick)
- Mar 22 and 29. Ales Bizjak and Rasmus Møgelberg: Paper in progress (Rasmus)
- Apr 5. Martin Hofmann and Thomas Streicher: The groupoid interpretation of type theory (Bassel)
- Apr 19. Awodey and Warren: Homotopy theoretic models of identity types (Bassel)
- April 26 and May 3. HoTT book Chp 2 (Marie)
- May 10. HoTT book Chp 3 (Christian)
- May 24. HoTT book Chp 4 (Danil)
- Some day in the future. Marc Bezem, Thierry Coquand and Simon Huber: A model of type theory in cubical sets
- …