Type theory seminar

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 and Oct 6: Coquand, Ruch and Sattler: Constructive sheaf models of type theory (Magnus)
• Oct 20: Pientka et al: Cocon: Computation in Contextual Type Theory (Carsten)
• Oct 27: Hofmann: Semantical Analysis of Higher-Order Abstract Syntax (Andrea)
• 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
• …