**Upcoming Talks**

- June 25: Pawel Sobocinski (TalTech)

**Past Talks**

- May 30: Markus Krabbe Larsen: Mechanizing state separation for modular cryptographic proofs
- May 6: Giorgio Bacci (Aalborg): Two Propositional Logics for the Lawvere Quantale. In 4A05
- Apr 9: Alessandro Bruni: Exploration of properties of differentiable logics through mechanisation. In 3A07.
- Mar 14: Daniel Gratzer (Aarhus): A modal deconstruction of Loeb induction
- Mar 12: Markus Krabbe Larsen: Adjoint Affine Interpretation
- Mar 8: Marco Carbone: A Probabilistic Choreography Language for PRISM
- Feb 27: Dmitriy Traytel (DIKU): Binding-aware datatypes and inductive predicates in Isabelle/HOL
- Feb 13: Maaike Zwart: What monads can and cannot do with a bit of extra time.

**Autumn 2023**

- Nov 14: Lean Course
- Nov 21: Lean Course
- Nov 28: Lean Course
- Monday Dec 4 (in Aud4):
**Brigitte Pientka**.*Mechanizing Session-Types: Enforcing linearity without linearity* - Oct 3:
**Emil Ørup Kristensen**.*Secure Choreographies in PSPSP/Isabelle* - Sept 5:
**Mahsa Varshosaz**.*Formal Specification and Testing for Reinforcement Learning* - Aug 22:
**Patrick Bahr**.*Modal FRP For All.*

Spring 2023. We meet Tuesdays 12-13

- Jan 25: Dawit Tirore: Sound and complete projection of multi-party protocols
- Feb 7: No talk, just meetings
- March 7: Carsten Schürmann (postponed)
- March 21: Reynald Affeldt (AIST) and Takafumi Saikawa (Nagoya)
- March 31: Raul Pardo Jimenez (Joint PLS/Square): Formal Verification of Privacy Policies for Social Networks
- April 11: Jimmy Koppen (MIT): Meta-metaprogramming
- May 2: Carsten Schürmann: Tick Unify
- May 16: Ichiro Hasuo (National Institute of Informatics, Japan): Proving Safety of Automated Driving Vehicles. Online talk.
- May 22: Natalia Slusarz (Heriot-Watt): Logic of Differentiable Logics: Towards a Uniform Semantics of DL
- May 24: Ekaterina Komendantskaya (Heriot-Watt): Integrated Neural Network Verification with Vehicle

Autumn 2022. We meet Tuesdays 12-13

- Sept 5: Frederik Haagensen: Incentive Alignment through Secure
- Oct 4: Yannick Zakowski (Inria): Monadic Definitional Interpreters as Formal Semantic Models of Computations in Coq
- Nov 1: Adele Veschetti (University of Bologna): A formal analysis of blockchain consensus protocols
- Nov 8: Jon Sterling (Aarhus University)
- Dec 13: Rasmus Møgelberg

Spring 2022. We meet Tuesdays 12-13

- Feb 11: Rasmus Lerchedahl Petersen (GitHub): Static analysis at GitHub Scale
- Feb 15: Jonas Kastberg Hinrichsen (Aarhus) (cancelled)
- March 15: Carsten Schürmann
- March 29: Mikkel Kragh Mathiesen (DIKU)
- April 7: Alejandro Aguirre (Aarhus)
- April 26: Tarmo Uustalu (Reykjavik) (over Zoom)
- May 18: Tim Steenvoorden (Open University the Netherlands)
- May 25: Christoph Matheja (DTU). Joint PLS/Square talk.
- June 7: Philip Munksgaard (DIKU)
- June 17: Sebastian Mödersheim (DTU). Joint PLS/CISAT talk

Autumn 2021. We meet Tuesdays 12-13.

- Sept 10: Patrick Bahr
- Sept 24: Jesper Bengtson
- Oct 5: Antoine van Muylder (Vrije Universiteit Brussel)
- Nov 16: Dawit Tiore
- Nov 30: Rasmus Lerchedahl Petersen (GitHub)(Cancelled)
- Dec 7 (at 13): Niccolò Veltri (Tallinn)
- Dec 14: Patricia Johann (Appalachian State University)

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: Christian Uldal Graulund PhD defence at 13.
- March 19: Willard Rafnsson
- March 26: Alceste Scalas: Effpi: Verified Message-Passing Programs in Scala 3
- April 9: Maaike Zwart
- April 16: Alex Kavvos (Bristol)
- April 23: Rasmus Møgelberg
- May 28: Louis Parlant
- June 4: Maja Hanne Kirkeby (RUC)

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