Spring 2021. We meet Fridays 12-13. For the time being meetings are virtual. Invitation will appear in calendars. If you would like to attend or give a talk, email Rasmus.

- Feb 12 (12-13). No talk, catch-up meeting
- Feb 26 (12-13). Magnus Baunsgaard Kristensen
- March 12: Reserved
- March 26: Alceste Scalas

Autumn 2020.

- Oct 6 (Zoom, 1230-1330): Marco Carbone: A Characterisation of Coherence as Linear Logic Proofs
- Oct 20 (Zoom, 13-14): Jonas Kastberg Hinrichsen: Mechanising Type Systems using Semantic Typing
- Nov 5 (3A08, 12-13): Christian Uldal Graulund
- Nov 17, 1230-1330: Willard Rafnsson

Spring 2020. This semester we meet Tuesdays 12-13 in 3A08 unless otherwise noted.

- Feb 4, (5A09): Marco Carbone: Towards a Logic of Forwarders
- Apr 17 (On zoom): Søren Debois
- May 18 (On zoom): Daniel Gratzer (Aarhus)

Autumn 2019. This semester we meet Tuesdays 12-13 in 4A05 unless otherwise noted.

- Aug 1, 13-14 (4A54): Guillaume Munch-Maccagnoni: From systems programming to linear logic, and back
- Sep 3: No talk, just discussions
- Sep 17: Talk cancelled
- Sep 23, 10-11 (3A18): Andreas Nuyts: Dependent type theory with modalities and modes
- Oct 1: Alessandro Bruni
- Oct 24 (Thursday), 12-13 (3A07): Jesper Bengtson.
- Nov 12: Patrick Bahr: Calculating Correct Compilers – How to Implement Compilers by Proving Their Correctness First
- Dec 4 (3A07): Andrea Vezzosi: Formalizing π-calculus in Guarded Cubical Agda
- Dec 5, 14-15 (2A20): Christian Sattler: Higher categorical structure in HoTT
- Dec 10 (4A05): Hugo Andres Lopez

In the Spring of 2019 PLS lunch talk are usually every other Wednesday 12-13 in 3A07

- Jan 29: No talk just discussions
- Feb 21 (3A08, 14-15): Willard Rafnsson: Types for Information-Flow Control in Functional Programming Languages
- March 13: Jonas Kastberg Hinrichsen: Formal Verification of Distributed Systems in Iris
- March 27: Andrea Vezzosi: Higher Inductive Types in Cubical Agda
- April 10: Dima Szamozvancev: Well-typed music does not sound wrong
- May 8: Carsten Schürmann: Intro to LF
- May 14: Adrien Guatto (IRIF, Paris): A Basis for Synchronous Functional Programming (at 12 in 3A01)
- May 15: Carsten Schürmann: Intro to LF continued
- May 29: Sonia Marin: Justification logic for modal logics on an intuitionistic base

In the Autumn of 2018 PLS lunch talk are usually every other Tuesday 12-13

- Sept 4 (2A08): No talk, just discussions
- Sept 18 (2A08): Patrick Bahr: Strict Ideal Completions of the Lambda Calculus
- Oct 2 (4A05): Niccolo Veltri: Bisimulation as path type for guarded recursive types
- Nov 20 (3A08): No talk
- Dec 4 (3A08): Marco Carbone: An Introduction to Multiparty Session Types and their Logical Interpretation
- Dec 18 (3A08): Rasmus Møgelberg: An invitation to presheaf semantics of type theory.

In the Spring of 2018 PLS lunch talk are usually every other Tuesday 12-13

- Feb 27: No talk, just discussions
- March 8 (10-11 in 3A18): Eva Graversen and Nobuko Yoshida
- March 13: Christian Uldal Graulund
- April 24: Jonas Kastberg Hinrichsen
- May 8: Jesper Bengtson
- May 28: Willard Rafnsson
- June 14: Rasmus Møgelberg and Bassel Mannaa (two talks)

In the Fall of 2017 PLS lunch talks usually take place on every other Tuesday 12-13 in 2A08.

- Sept 6: Oscar Toro: The Bitcoin Backbone Protocol
- Sept 19: Jonas Kastberg Hinrichsen: Specification of object oriented languages in practice
- Oct 3: Niccolo Veltri: Finiteness and rational sequences, constructively
- Oct 5: Formalisations using two-level type theory
- Oct 31: Cancelled
- Nov 13: Danel Ahman: A fibrational view on computational effects. 13-14 in 3A08.
- Nov 14: Hugo A. Lopez
- Nov 28: Anupam Das (U. Copenhagen)
- Dec 12: Sonia Marin

In the Spring of 2017 PLS lunch talks usually take place on every other Thursday 12-13 in 3A08.

- February 2: No talk, just discussions
- February 16: Rosario Giustolisi
- March 16: Christian Uldal Graulund
- March 24, 14-15 in 4A05: Bas Spitters (Aarhus): Colimits in homotopy type theory.
- March 30: Agata Murawska: Lincx: A Linear Logical Framework with First-class Context
- May 23: Patrick Bahr: The clocks are ticking: No more delays! and Rasmus Møgelberg: Presheaf semantics for Guarded Dependent Type Theory
- June 8: Bassel Mannaa: Stack Semantics of Type Theory

In the Fall of 2016 PLS lunch talks usually take place on every other Thursday 12-13 in 3A08.

- September 1. Marco Carbone: Coherence Generalises Duality: a logical explanation of multiparty session types
- September 29. Peter Brottveit Bock.
- October 13. Meeting cancelled.
- Nov 10. Håkon Normann: Non-interleaving opperational semantics for late and early Pi-calculus
- Nov 24. Bassel Mannaa.

Talks from Spring 2016:

- February 4. Alessandro Bruni: AIF-ω: Set-based Protocol Abstraction with Countable Families.
- February 18. Robin Kaarsgaard (U. Copenhagen)
- March 17. Hans Bugge Grathwohl (Aarhus).
- March 31. Alec Faithful: Coqoon: an IDE for interactive proof development in Coq
- April 28. Søren Debois.
- June 10. Michael Denzel (U. Birmingham).

Talks from Fall 2015:

- August 27, 13-13:30, 3A08. Patrick Bahr: Certified Symbolic Management of Financial Multi-party Contracts
- September 3, 12-13, 3A08. Peter Brottveit Bock: A linear contextual logical Framework.
- September 17, 12-13, 3A08. Marco Carbone: Multiparty Session Types as Coherence Proofs
- September 18, 12-13, 3A08. Thomas Bolander (DTU): Building Planning Agents with Higher-Order Reasoning Capabilities
- September 21, 10-11, 3A08. Paul Blain Levy (Birmingham): Transition systems over games
- October 1, 12-13, 3A18. Cinzia Di Giusto (Nice, Sophia Antipolis): A Multyparty Session Type discipline for Event-Based Runtime Adaptation
- October 19, 12-13, 2A08. Marco Paviotti: Formally verifying exceptions for low-level code with Separation Logic
- October 29, 12-13. TBD.
- November 11, 10-11, 4A09. Robbert Krebbers (Aarhus): Formalizing C in Coq
- November 12, 12-13. Agata Anna Murawska: Towards an happy marriage: Linear Logic and Beluga
- November 26, 12-13. Marie Kerjean (PPS Paris): The computational content of derivation
- December 10, 12-13. Marco Paviotti. Synthetic Guarded Domain Theory: Recursion in Guarded Recursion.
- December 17, 12-13. Lorena Ronquillo