Programme

Talks will take place in room TL325 in the Learning and Teaching Building on the University of Strathclyde campus, with coffee breaks and lunches in the adjacent room TL328 (TL324 on Friday). Invited talks (with yellow background below) are 45 minutes long, and contributed talks are either 15 minutes (light gray background below) or 20 minutes long. The talks that are part of the Women in EPN event on Tuesday afternoon have different timings.

The programme is also available in PDF format and as an ICS file which you can import into your calendar (or look at online).

Time (BST) Monday 9 June Tuesday 10 June Wednesday 11 June Thursday 12 June Friday 13 June
8:30–09:00 Registration and coffee Coffee Coffee Coffee Coffee
09:00–10:35 Chair: Fredrik Nordvall Forsberg Chair: Robert Atkey Chair: Andreas Abel Chair: Herman Geuvers Chair: Andrew Swan
Towards topological type theory for decrypting transfinite methods in classical mathematics [s]
Ingo Blechschmidt		 Algebraic Universes and Variances For All [s]
Matthieu Sozeau, Marc Bezem		 Intuitionistic modalities through proof theory [s]
Sonia Marin		 A Guided Tour of Polarity and Focusing [s]
Chris Martens		 A constructive higher groupoid model of homotopy type theory [s]
Christian Sattler
Internalized Parametricity via Lifting Universals [s]
Aaron David Stump
Accessible Sets in Martin-Löf Type Theory with Function Extensionality [s]
Yuta Takahashi		 Extending Sort Polymorphism with Elimination Constraints [s]
Tomás Díaz, Johann Rosain, Matthieu Sozeau, Nicolas Tabareau, Théo Winterhalter		 Higher-Order Focusing on Linearity and Effects [s]
Siva Somayyajula		 Compositional memory management in the λ-calculus [s]
Sky Wilshaw, Graham Hutton		 A Ghost Sort for Proof-Relevant yet Erased Data in Rocq and MetaRocq [s]
Johann Rosain, Matthieu Sozeau, Théo Winterhalter
In Cantor Space, No One Can Hear You Stream [s]
Martin Baillon, Assia Mahboubi, Pierre-Marie Pédrot		 The Case for Impredicative Universe Polymorphism [s]
Stefan Monnier		 Monadic Equational Reasoning for while loop in Rocq [s]
Ryuji Kawakami, Jacques Garrigue, Takafumi Saikawa, Reynald Affeldt		 Choice principles and a cotopological modality in HoTT [s]
Owen Milner		 A Fully Dependent Assembly Language [s]
Yulong Huang, Jeremy Yallop
Examples and counter-examples of injective types in univalent mathematics [s]
Tom de Jong, Martin Escardo		 From parametricity to identity types [s]
Thorsten Altenkirch, Ambrus Kaposi, Michael Shulman, Elif Üsküplü		 Commuting Rules for the Later Modality and Quantifiers in Step-Indexed Logics [s]
Bálint Kocsis, Robbert Krebbers		 Towards Modular Composition of Inductive Types Using Lean Meta-programming [s]
Ramy Shahin		 Efficient Program Extraction in Elementary Number Theory using the Proof Assistant Minlog [s]
Franziskus Wiesnet
10:35–11:00 Coffee break Coffee break Coffee break Coffee break Coffee break
11:00–12:30 Chair: Guillaume Allais Chair: Tom de Jong Chair: András Kovács Chair: Liang-Ting Chen Chair: Kenji Maillard
A Coq Formalization of Lagois Connections for Secure Information Flow [s]
Casper Ståhl, Léon Gondelman, René Rydhof Hansen, Danny Bøgsted Poulsen		 About the construction of simplicial and cubical sets in indexed form: the case of degeneracies [s]
Hugo Herbelin, Ramkumar Ramachandra		 How (not) to prove typed type conversion transitive [s]
Yann Leray		 Type-safe Bidirectional Channels in Idris 2 [s]
Guillaume Allais		 Linear Types inside Dependent Type Theory [s]
Maximilian Doré
Coq proof of the fifth Busy Beaver value [s]
Tristan Stérin, the bbchallenge Collaboration		 Predicative Stone Duality in Univalent Foundations [s]
Ayberk Tosun, Martin Escardo		 Arrow algebras [s]
Benno van den Berg, Marcus Briët, Umberto Tarantino		 Code Generation via Meta-programming in Dependently Typed Proof Assistants (Experience Report) [s]
Mathis Bouverot-Dupuis, Yannick Forster		 Impredicative Encodings of Inductive and Coinductive Types [s]
Herman Geuvers, Niels van der Weide, Steven Bronsveld
Mechanizing logical relations [s]
Josselin Poiret		 Cocompleteness in simplicial homotopy type theory [s]
Daniel Gratzer, Jonathan Weinberger, Ulrik Buchholtz		 Weak Equality Reflection in MLTT with Propositional Truncation [s]
Felix Bradley, Zhaohui Luo		 Towards Being Positively Negative about Dependent Types [s]
Jan de Muijnck-Hughes		 NbE for LNL via Adjoint Meta-modalities [s]
James Wood
Geometric Reasoning in Lean: from Algebraic Structures to Presheaves [s]
Kenji Maillard, Yiming Xu		 Yet another homotopy group, yet another Brunerie number [s]
Tom Jack, Axel Ljungström		 Towards Quotient Inductive Types in Observational Type Theory [s]
Thiago Felicissimo, Nicolas Tabareau		 Implementing a Typechecker for an Esoteric Language: Experiences, Challenges, and Lessons [s]
Alex Rice		 Unboxed Dependent Types [s]
Constantine Theocharis, Ellis Kesterton
Löb's Theorem and Provability Predicates in Rocq [s]
Janis Bailitis, Dominik Kirst, Yannick Forster		 Rezk completions For (Elementary) Topoi [s]
Kobe Wullaert, Niels van der Weide		 Matching (Co)patterns with Cyclic Proofs [s]
Lide Grotenhuis, Daniël Otten		 A Two-level Foundation for the Calculus of Constructions [s]
Pietro Sabelli, Maria Emilia Maietti		 A Quantitative Dependent Type Theory with Recursion [s]
Oskar Eriksson, Nils Anders Danielsson, Andreas Abel
12:30–13:30 Lunch break Lunch break Lunch & Coffee break Lunch & Coffee break Lunch & Coffee break
13:30–14:10 Chair: Théo Winterhalter Chair: Benno van den Berg Chair: Malin Altenmüller Chair: Ambrus Kaposi Chair: Håkon Gylterud
Expansion in a Calculus with Explicit Substitutions [s]
Ana Jorge Almeida, Sandra Alves, Mário Florido		 Type Theory and Philosophical Logic [s]
Greg Restall		 Towards a computational quantum logic [s]
Alejandro Díaz-Caro		 A Timed Predicate Temporal Logic Sequent Calculus [s]
Javier Enriquez Mendoza, Sam Speight, Vincent Rahli		 Stellar — A Library for API Programming [s]
André Videla
Presheaves on Purpose [s]
Conor Mc Bride		 Constructive algebraic completeness of first-order bi-intuitionistic logic [s]
Dominik Kirst, Ian Shillito		 Internal Proofs of Strong Normalization [s]
Cody Roux		 Verfying Z3 RUP Proofs with the Interactive Theorem Provers Coq/Rocq and Agda [s]
Harry Bryant, Andrew Lawrence, Monika Seisenberger, Anton Setzer		 An Inductive Universe for Setoids [s]
Loïc Pujet
14:10–15:00 Thinning Thinnings: Safe and Efficient Binders [s]
April Gonçalves, Wen Kokke		 Chair: Sandra Alves Excursion to Loch Lomond
 Formalising Monitors for Distributed Deadlock Detection [s]
Radosław Jan Rowicki, Adrian Francalanza, Alceste Scalas		 Weihrauch Problems as Containers [s]
Ian Price, Cécilia Pradic
WEPN Opening and Welcome
Ecumenical logic [s]
Elaine Pimentel (14:15–15:15)
Categorical Normalization by Evaluation: A Novel Universal Property for Syntax [s]
David G. Berry, Marcelo Fiore		 Fair Termination for Resource-Aware Active Objects [s]
Francesco Dagnino, Paola Giannini, Violet Ka I Pun, Ulises Torrella		 Containers: Compositionality for Tensors [s]
Neil Ghani, Pierre Hyvernat, Artjoms Sinkarovs
Rational Codata as Syntax-with-Binding: Correct-by-Construction Foundations of the Modal μ-Calculus [s]
Sean Watters		 Mechanized safety of Jolteon consensus in Agda [s]
Orestis Melkonian, Mauro Jaskelioff, James Chapman		 Large Elimination and Indexed Types in Refinement Types [s]
Alessio Ferrarini, Niki Vazou
15:00–15:30 Coffee break Coffee break
(15:15–15:45)		 Coffee break Coffee break
15:30–17:00 Chair: Thorsten Altenkirch Chair: Sandra Alves Chair: Dominik Kirst Chair: Niels van der Weide
Dependent two-sided fibrations for directed type theory [s]
Fernando Chu, Paige Randall North		 Reasoning with strict symmetric monoidal categories in Agda [s]
Malin Altenmüller (15:45–16:15)		 Canonical Bidirectional Typing via Polarised System L [s]
Zanzi Mihejevs		 HoTTLean: Formalizing the Meta-Theory of HoTT in Lean [s]
Joseph Hua, Steve Awodey, Mario Carneiro, Sina Hazratpour, Wojciech Nawrocki, Spencer Woolfson, Yiming Xu
Synthetic-Inductive Category Theory [s]
Jacob Neumann		 An existential-free theory of arithmetic in all finite types [s]
Makoto Fujiwara		 Representing type theories in two-level type theory [s]
Nicolai Kraus, Tom de Jong
Directed equality with dinaturality [s]
Andrea Laretto, Fosco Loregian, Niccolò Veltri		 Type Theory of Acyclic and Cyclic Algorithms without Chain Memory [s]
Roussanka Loukanova (16:15–16:45)		 A Generalized Logical Framework [s]
András Kovács, Christian Sattler		 Lean4Lean: Mechanizing the Metatheory of Lean [s]
Mario Carneiro
A Type Theory for Comprehension Categories with Applications to Subtyping [s]
Niyousha Najmaei, Niels van der Weide, Benedikt Ahrens, Paige Randall North		 A Curry-Howard correspondence for intuitionistic inquisitive logic [s]
Ivo Pezlar, Vít Punčochář		 Solving Guarded Domain Equations in Presheaves Over Ordinals and Mechanizing It [s]
Sergei Stepanenko, Amin Timany
15 minute break 15 minute break
(16:45–17:00)		 Y is not typable in λ U [s]
Herman Geuvers, Joep Verkoelen		 15 minute break
17:00–18:15 Chair: Nicolai Kraus Discussion on gender balance issues [s]
(17:00–18:30)		 TYPES Business Meeting [s]
 Chair: Rasmus Møgelberg
Irregular models of type theory [s]
Andrew Wakelin Swan		 Cohomology in Synthetic Stone Duality [s]
Hugo Moeneclaey, Thierry Coquand, Felix Cherubini, Freek Geerligs
An algebraic internal groupoidal model of Martin-Löf type theory [s]
Calum Hughes		 Towards Formalising the Guard Checker of Rocq [s]
Yee-Jian Tan, Yannick Forster
Realizability Triposes from Sheaves [s]
Bruno da Rocha Paiva, Vincent Rahli		 Extensional concepts in intensional type theory, revisited [s]
Yufeng Li, Krzysztof Kapulkin
AdapTT: A Type Theory with Functorial Types [s]
Arthur Adjedj, Thibaut Benjamin, Meven Lennon-Bertrand, Kenji Maillard		 Lightweight Agda Formalization of Denotational Semantics [s]
Peter D. Mosses
18:15–19:30 Welcome Reception
Level 11, Livingstone Tower
19:30–22:00 Conference Dinner
Grosvenor Cafe

Sponsors

Gold sponsor

Jane Street

Bronze sponsors

Formal Vindications Well-typed IOHK

Other sponsors

Tunnock's