Talks
Autumn 2023. We meet Tuesdays 1213.
Upcoming Talks
 Sept 19
 Oct 3
 Oct 17 (No talk, Autumn break)
 Oct 31
 Nov 14
 Nov 28
 Dec 12
Past Talks

Sept 5:: Mahsa Varshosaz. Formal Specification and Testing for Reinforcement Learning
The development process for reinforcement learning applications is still exploratory rather than systematic. This exploratory nature reduces reuse of specifications between applications and increases the chances of introducing programming errors. This paper takes a step towards systematizing the development of reinforcement learning applications. We introduce a formal specification of reinforcement learning problems and algorithms, with a particular focus on temporal difference methods and their definitions in backup diagrams. We further develop a test harness for a large class of reinforcement learning applications based on temporal difference learning, including SARSA and Qlearning. The entire development is rooted in functional programming methods; starting with pure specifications and denotational semantics, ending with propertybased testing and using compositional interpreters for a domainspecific term language as a test oracle for concrete implementations. We demonstrate the usefulness of this testing method on a number of examples, and evaluate with mutation testing. We show that our test suite is effective in killing mutants (90% mutants killed for 75% of subject agents). More importantly, almost half of all mutants are killed by generic writeonceuseeverywhere tests that apply to any reinforcement learning problem modeled using our library, without any additional effort from the programmer.

Aug 22: Patrick Bahr. Modal FRP For All.
Functional reactive programming (FRP) provides a highlevel interface for implementing reactive systems in a declarative manner. However, this highlevel interface has to be carefully reigned in to ensure that programs can in fact be executed in practice. Specifically, one must ensure that FRP programs are productive, causal, and can be implemented without introducing space leaks. In recent years, modal types have been demonstrated to be an effective tool to ensure these operational properties.
In this paper, we present Rattus, a modal FRP language that extends and simplifies previous modal FRP calculi while still maintaining the operational guarantees for productivity, causality, and space leaks. The simplified type system makes Rattus a practical programming language that can be integrated with existing functional programming languages. To demonstrate this, we have implemented a shallow embedding of Rattus in Haskell that allows the programmer to write Rattus code in familiar Haskell syntax and seamlessly integrate it with regular Haskell code. Thus Rattus combines the benefits enjoyed by FRP libraries such as Yampa, namely access to a rich library ecosystem (e.g. for graphics programming), with the strong operational guarantees offered by a bespoke type system.
To establish the productivity, causality, and memory properties of the language, we prove type soundness using a logical relations argument fully mechanised in the Coq proof assistant.
Spring 2023. We meet Tuesdays 1213
 Jan 25: Dawit Tirore: Sound and complete projection of multiparty 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): Metametaprogramming
 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 (HeriotWatt): Logic of Differentiable
Logics: Towards a Uniform Semantics of DL
 May 24: Ekaterina Komendantskaya (HeriotWatt): Integrated Neural Network Verification with Vehicle
Autumn 2022. We meet Tuesdays 1213
 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 1213
 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 1213.
 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 1213. 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 (1213). No talk, catchup meeting
 Feb 26 (1213). Magnus Baunsgaard Kristensen
 March 12: Christian Uldal Graulund PhD defence at 13.
 March 19: Willard Rafnsson
 March 26: Alceste Scalas: Effpi: Verified MessagePassing 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, 12301330): Marco Carbone: A Characterisation of Coherence as Linear Logic Proofs
 Oct 20 (Zoom, 1314): Jonas Kastberg Hinrichsen: Mechanising Type Systems using Semantic Typing
 Nov 5 (3A08, 1213): Christian Uldal Graulund
 Nov 17, 12301330: Willard Rafnsson
Spring 2020. This semester we meet Tuesdays 1213 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 1213 in 4A05 unless otherwise noted.
 Aug 1, 1314 (4A54): Guillaume MunchMaccagnoni: From systems programming to linear logic, and back
 Sep 3: No talk, just discussions
 Sep 17: Talk cancelled
 Sep 23, 1011 (3A18): Andreas Nuyts: Dependent type theory with modalities and modes
 Oct 1: Alessandro Bruni
 Oct 24 (Thursday), 1213 (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, 1415 (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 1213 in 3A07
 Jan 29: No talk just discussions
 Feb 21 (3A08, 1415): Willard Rafnsson: Types for InformationFlow 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: Welltyped 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
1213
 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
1213
 Feb 27: No talk, just discussions
 March 8 (1011 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 1213 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 twolevel type theory
 Oct 31: Cancelled
 Nov 13: Danel Ahman: A fibrational view on computational effects.
1314 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 1213 in 3A08.
 February 2: No talk, just discussions
 February 16: Rosario Giustolisi
 March 16: Christian Uldal Graulund
 March 24, 1415 in 4A05: Bas Spitters (Aarhus): Colimits in homotopy
type theory.
 March 30: Agata Murawska: Lincx: A Linear Logical Framework with
Firstclass 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 1213 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: Noninterleaving opperational semantics for
late and early Picalculus
 Nov 24. Bassel Mannaa.
Talks from Spring 2016:
 February 4. Alessandro Bruni: AIFω: Setbased 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, 1313:30, 3A08. Patrick Bahr: Certified Symbolic
Management of Financial Multiparty Contracts
 September 3, 1213, 3A08. Peter Brottveit Bock: A linear contextual
logical Framework.
 September 17, 1213, 3A08. Marco Carbone: Multiparty Session Types
as Coherence Proofs
 September 18, 1213, 3A08. Thomas Bolander (DTU): Building Planning
Agents with HigherOrder Reasoning Capabilities
 September 21, 1011, 3A08. Paul Blain Levy (Birmingham): Transition
systems over games
 October 1, 1213, 3A18. Cinzia Di Giusto (Nice, Sophia Antipolis): A
Multyparty Session Type discipline for EventBased Runtime
Adaptation
 October 19, 1213, 2A08. Marco Paviotti: Formally verifying
exceptions for lowlevel code with Separation Logic
 October 29, 1213. TBD.
 November 11, 1011, 4A09. Robbert Krebbers (Aarhus): Formalizing C
in Coq
 November 12, 1213. Agata Anna Murawska: Towards an happy
marriage: Linear Logic and Beluga
 November 26, 1213. Marie Kerjean (PPS Paris): The computational
content of derivation
 December 10, 1213. Marco Paviotti. Synthetic Guarded Domain Theory:
Recursion in Guarded Recursion.
 December 17, 1213. Lorena Ronquillo