Program

10:00	José Espírito Santo, Ralph Matthes and Luís Pinto Faithful interpretations of LJT and LJQ into polarized logic (abstract) PRESENTER: Luís Pinto
10:20	Reynald Affeldt, Alessandro Bruni, Pierre Roux and Takafumi Saikawa Yet another formal theory of probabilities (with an application to random sampling) (abstract)

10:40-11:10Coffee Break

11:10-12:30 Session 4: Constructive Mathematics

Chair:

Benno van den Berg

Location: Aud 0

11:10	Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot and Matthieu Piquerez A zoo of continuity properties in constructive type theory (abstract)
11:30	Dominik Kirst and Haoyi Zeng The Blurred Drinker Paradox and Blurred Choice Axioms for the Downward Löwenheim-Skolem Theorem (abstract)
11:50	Bruno da Rocha Paiva, Liron Cohen, Yannick Forster, Dominik Kirst and Vincent Rahli Limited Principles of Omniscience in Constructive Type Theory (abstract)
12:10	Haoyi Zeng, Yannick Forster and Dominik Kirst Post’s Problem and the Priority Method in CIC (abstract)

12:30-14:00Lunch Break

14:00-15:20 Session 5: Proof Assistant Implementation

Chair:

Pierre-Marie Pédrot

Location: Aud 0

14:00	Kanstantsin Nisht and Andreas Abel Type-Based Termination Checking in Agda (abstract)
14:20	Hugo Herbelin Size-preserving dependent elimination (abstract)
14:40	Hugo Herbelin How much do System T recursors lift to dependent types? (abstract)
15:00	Kayleigh Lieverse, Lucas Escot and Jesper Cockx A generic translation from case trees to eliminators (abstract) PRESENTER: Kayleigh Lieverse

15:20-15:50Coffee Break

15:50-16:50 Session 6: Blockchain and Smart Contracts

Chair:

Patrick Bahr

Location: Aud 0

15:50	Orestis Melkonian, Mauro Jaskelioff, James Chapman and Jon Rossie Mechanizing BFT consensus protocols in Agda (abstract)
16:10	Fahad Alhabardi and Anton Setzer Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness (abstract)
16:30	Nikolaj Sidorenco, Laura Brædder, Lasse Letager Hansen, Eske Hoy Nielsen and Bas Spitters A formal security analysis of Blockchain voting (abstract)

16:50-17:50 Session 7: Business Meeting

Chair:

Rasmus Ejlers Møgelberg

Location: Aud 0

Tuesday, June 11th

View this program: with abstracts session overview talk overview

09:00-10:00 Session 8: Invited Talk

Chair:

Bas Spitters

Location: Aud 0

09:00

Talia Ringer

Bridging Neural and Symbolic Proof Automation (abstract)

10:00-10:40 Session 9: Parametricity

Chair:

Paige Randall North

Location: Aud 0

10:00	Thorsten Altenkirch, Ambrus Kaposi, Michael Shulman and Elif Üsküplü Internal relational parametricity, without an interval (abstract)
10:20	Jacob Neumann Updates on Paranatural Category Theory (abstract)

10:40-11:10Coffee Break

11:10-12:30 Session 10: Models of Type Theory

Chair:

Daniel Gratzer

Location: Aud 0

11:10	Benno van den Berg Recent progress in the theory of effective Kan fibrations in simplicial sets (abstract)
11:30	Viktor Bense, Ambrus Kaposi and Szumi Xie Strict syntax of type theory via alpha-normalisation (abstract)
11:50	Thorsten Altenkirch and Ambrus Kaposi Coherent Categories with Families (abstract)
12:10	Ambrus Kaposi and Szumi Xie Type theory in type theory using single substitutions (abstract)

12:30-14:00Lunch Break

14:00-15:20 Session 11: New Type Theories

Chair:

András Kovács

Location: Aud 0

14:00	Henning Basold and Herman Geuvers Harmony in Duality (abstract)
14:20	Daniel Gratzer and Lars Birkedal A modal deconstruction of Loeb induction (abstract)
14:40	Thierry Coquand and Jonas Höfer Poset Type Theory (abstract)
15:00	Yulong Huang and Jeremy Yallop Towards Quantitative Inductive Families (abstract)

15:20-15:50Coffee Break

15:50-16:50 Session 12: Formalisations and Probability Theory

Chair:

Mauro Jaskelioff

Location: Aud 0

15:50	Dominique Larchey-Wendling Quasi Morphisms for Almost Full Relations (abstract)
16:10	Joachim Kristensen, Tobias Reinhard and Michael Kirkedal Thomsen Looking Back: A Probabilistic Inverse Perspective on Test Generation (abstract)
16:30	András Kovács Polarized Lambda-Calculus at Runtime, Dependent Types at Compile Time (abstract)

18:30-20:00 Welcome Reception

The welcome reception will be hosted in Festsalen at Copenhagen City Hall. Details on how to get there.

Wednesday, June 12th

View this program: with abstracts session overview talk overview

09:00-10:00 Session 13: Algebraic Geometry and Topology

Chair:

Ulrik Buchholtz

Location: Aud 0

09:00	Max Zeuner and Matthias Hutzler Grothendieck’s Functor of Points Approach to Schemes in Type Theory – Constructivity and Size Issues (abstract)
09:20	Axel Ljungström and Loïc Pujet A Constructive Cellular Approximation Theorem in HoTT (abstract)
09:40	Axel Ljungström and David Wärn Revisiting the Steenrod Squares in HoTT (abstract)

10:00-10:40 Session 14: Logic

Chair:

Henning Basold

Location: Aud 0

10:00	Felix Bradley and Zhaohui Luo Representing Temporal Operators with Dependent Event Types (abstract)
10:20	Herman Geuvers and Tonny Hurkens Normalization of Natural Deduction for Classical Predicate Logic (abstract)

10:40-11:10Coffee Break

11:10-12:30 Session 15: Equality and Evaluation

Chair:

Andreas Abel

Location: Aud 0

11:10	Pablo Barenbaum, Delia Kesner and Mariana Milicich Useful Evaluation, Quantitatively (abstract)
11:30	Kenji Maillard Splitting Booleans with Normalization-by-Evaluation (abstract)
11:50	Matthew Sirman, Meven Lennon-Bertrand and Neel Krishnaswami Implementing Observational Equality with Normalisation by Evaluation (abstract)
12:10	Bruno Barras, Thiago Felicissimo and Théo Winterhalter Towards a logical framework modulo rewriting and equational theories (abstract)

12:30-14:00Lunch Break

14:00-15:00 Session 16: Computability

Chair:

Dominik Kirst

Location: Aud 0

14:00	Danel Ahman and Andrej Bauer Comodule Representations of Second-Order Functionals (abstract)
14:20	Andrew Swan Oracle modalities (abstract)
14:40	Pierre-Marie Pédrot “Proofs are programs” in MLTT (abstract)

15:00-15:30Coffee Break

16:50-18:00 Social Event: Canal Tour

A boat will take us through the canals of Copenhagen starting at Christianshavns Torv, right next to Lagkagehuset. Details on how to get there.

Thursday, June 13th

View this program: with abstracts session overview talk overview

09:00-10:00 Session 17: Invited Talk

Chair:

Thierry Coquand

Location: Aud 0

09:00

Egbert Rijke

Concrete Univalent Mathematics (abstract)

10:00-10:40 Session 18: Proofs

Chair:

Marco Carbone

Location: Aud 0

10:00	Joachim Tilsted Kristensen, Ján Perháč, Lars Tveito, Lars-Bo Husted Vadgaard, Michael Kirkedal Thomsen, Oleks Shturmov, Samuel Novotný, Sergej Chodarev and William Steingartner OnlineProver: A proof assistant for online teaching of formal logic and semantics (abstract)
10:20	Mikkel Kragh Mathiesen and Ken Friis Larsen Proof and Consequences: Separating Construction and Checking of eBPF Loops (abstract)

10:40-11:10Coffee Break

11:10-12:30 Session 19: HoTT and Sets

Chair:

Benedikt Ahrens

Location: Aud 0

11:10	Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu Constructive Ordinal Exponentiation in Homotopy Type Theory (abstract)
11:30	Clemens Kupke, Fredrik Nordvall Forsberg and Sean Watters Extensional Finite Sets and Multisets in Type Theory (abstract)
11:50	Philipp Joram and Niccolò Veltri Comparing Quotient- and Symmetric Containers (abstract)
12:10	Håkon Robbestad Gylterud and Elisabeth Stenholm Univalent Material Set Theory: Hierarchies of n-types (abstract)

12:30-14:00Lunch Break

14:00-15:20 Session 20: Category Theory

Chair:

Nicolai Kraus

Location: Aud 0

14:00	Nima Rasekh, Niels van der Weide, Benedikt Ahrens and Paige Randall North The Univalence Maxim and Univalent Double Categories (abstract) PRESENTER: Niels van der Weide
14:20	Felix Cherubini, Thierry Coquand, Freek Geerligs and Hugo Moeneclaey Synthetic Stone duality (abstract)
14:40	Kobe Wullaert A formal study of the Rezk completion (abstract)
15:00	Niels van der Weide The Internal Language of Univalent Categories (abstract)

15:20-15:50Coffee Break

15:50-17:10 Session 21: Universes

Chair:

Andrew Swan

Location: Aud 0

15:50	Ulrik Buchholtz, Daniel Gratzer and Jonathan Weinberger Universes in simplicial type theory (abstract)
16:10	Yuta Takahashi Large Universe Construction by Indexed Induction-Recursion in Agda (abstract)
16:30	Yoan Géran A Canonical Form for Universe Levels in Impredicative Type Theory (abstract)
16:50	Peter Dybjer and Anton Setzer Predicativity of the Mahlo Universe in Type Theory (abstract)

19:00-22:00 Conference Dinner

The conference dinner will be hosted at Spiseloppen. Details on how to get there.

Friday, June 14th

View this program: with abstracts session overview talk overview

09:15-10:30 Session 22: Special Session for Peter Aczel

Chair:

Peter Dybjer

Location: Aud 0

09:15	Peter Dybjer Special Session in Memory of Peter Aczel
09:30	Michael Rathjen On Relating Type Theories and Set Theories (abstract)

10:30-11:00Coffee Break

11:00-12:00 Session 23: Special Session for Peter Aczel

Chair:

Peter Dybjer

Location: Aud 0

11:00

Nicola Gambino

Logic in Dependent Type Theory (abstract)

12:00-13:30Lunch Break

13:30-14:50 Session 24: Models of Type Theory

Chair:

Ambrus Kaposi

Location: Aud 0

13:30	Daniël Otten and Matteo Spadetto Semantics of Axiomatic Type Theory (abstract)
13:50	Sori Lee Identity types in predicate logic (abstract)
14:10	Sam Speight Partial Combinatory Algebras for Intensional Type Theory (abstract)
14:30	Fernando Chu, Éléonore Mangel and Paige Randall North A directed homotopy type theory for 1-categories (abstract)

14:50-15:20Coffee Break