Talks

Upcoming Talks

• May 28: Rasmus Møgelberg: Induction and Recursion Principles in a Higher-Order Quantitative Logic
• June 25: Lyes Saadi

Spring 2025

• May 14: Matteo Acclavio (Sussex): Formulas as Processes in Linear Logic Programming
• April 9: Grant application discussions
• April 8: Joris Ceulemans (KU Leuven): Multimode Type Theory as a Library in Type Theory
• April 7: Philipp Haselwarter (Aarhus): Security Proofs via Approximate Relational Reasoning for Higher-Order Probabilistic Programs
• April 2: Grant application discussions
• Mar 26: Sergei Stepanenko (Aarhus): Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It
• Feb 21: Nobuko Yoshida (Oxford): Separation and Encodability in Mixed Choice Multiparty Sessions

Autumn 2024

• Dec 11: Simon Gay (Glasgow): Trains, Pictures and Types
• Dec 9: Marino Miculan (Udine): A Bigraph-based Formal Model and Verification Framework for Container-Based Systems
• Nov 26: Eric Giovannini (University of Michigan): Denotational Semantics of Gradual Typing using Synthetic Guarded Domain Theory
• Nov 22: PLS research day (all day)
• Nov 19: Maaike Zwart: Self-Distributing Monads
• Sept 10: Patrick Bahr: Calculating Graph-Based Compilers
• Aug 27: Rasmus Møgelberg: An introduction to synthetic guarded domain theory with applications to probabilistic programming languages.

Spring 2024

• June 25: Pawel Sobocinski (TalTech)
• 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