Accepted Talk Proposals

• Pierre-Marie Pédrot. “Proofs are programs” in MLTT
• Yoan Géran. A Canonical Form for Universe Levels in Impredicative Type Theory
• Axel Ljungström and Loïc Pujet. A Constructive Cellular Approximation Theorem in HoTT
• Fernando Chu, Éléonore Mangel and Paige Randall North. A directed homotopy type theory for 1-categories
• Nikolaj Sidorenco, Laura Brædder, Lasse Letager Hansen, Eske Hoy Nielsen and Bas Spitters. A formal security analysis of Blockchain voting
• Kobe Wullaert. A formal study of the Rezk completion
• Kayleigh Lieverse, Lucas Escot and Jesper Cockx. A generic translation from case trees to eliminators
• Daniel Gratzer and Lars Birkedal. A modal deconstruction of Loeb induction
• Martin Baillon, Yannick Forster, Assia Mahboubi, Pierre-Marie Pédrot and Matthieu Piquerez. A zoo of continuity properties in constructive type theory
• Thorsten Altenkirch and Ambrus Kaposi. Coherent Categories with Families
• Danel Ahman and Andrej Bauer. Comodule Representations of Second-Order Functionals
• Philipp Joram and Niccolò Veltri. Comparing Quotient- and Symmetric Containers
• Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu. Constructive Ordinal Exponentiation in Homotopy Type Theory
• Clemens Kupke, Fredrik Nordvall Forsberg and Sean Watters. Extensional Finite Sets and Multisets in Type Theory
• José Espírito Santo, Ralph Matthes and Luís Pinto. Faithful interpretations of LJT and LJQ into polarized logic
• Márk Széles. Formalisation of a probabilistic type theory
• Max Zeuner and Matthias Hutzler. Grothendieck’s Functor of Points Approach to Schemes in Type Theory – Constructivity and Size Issues
• Henning Basold and Herman Geuvers. Harmony in Duality
• Hugo Herbelin. How much do System T recursors lift to dependent types?
• Sori Lee. Identity types in predicate logic
• Matthew Sirman, Meven Lennon-Bertrand and Neel Krishnaswami. Implementing Observational Equality with Normalisation by Evaluation
• Thorsten Altenkirch, Ambrus Kaposi, Michael Shulman and Elif Üsküplü. Internal relational parametricity, without an interval
• Yuta Takahashi. Large Universe Construction by Indexed Induction-Recursion in Agda
• Bruno da Rocha Paiva, Liron Cohen, Yannick Forster, Dominik Kirst and Vincent Rahli. Limited Principles of Omniscience in Constructive Type Theory
• Joachim Kristensen, Tobias Reinhard and Michael Kirkedal Thomsen. Looking Back: A Probabilistic Inverse Perspective on Test Generation
• Orestis Melkonian, Mauro Jaskelioff, James Chapman and Jon Rossie. Mechanizing BFT consensus protocols in Agda
• Herman Geuvers and Tonny Hurkens. Normalization of Natural Deduction for Classical Predicate Logic
• 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
• Andrew Swan. Oracle modalities
• Sam Speight. Partial Combinatory Algebras for Intensional Type Theory
• András Kovács. Polarized Lambda-Calculus at Runtime, Dependent Types at Compile Time
• Thierry Coquand and Jonas Höfer. Poset Type Theory
• Haoyi Zeng, Yannick Forster and Dominik Kirst. Post’s Problem and the Priority Method in CIC
• Peter Dybjer and Anton Setzer. Predicativity of the Mahlo Universe in Type Theory
• Mikkel Kragh Mathiesen and Ken Friis Larsen. Proof and Consequences: Separating Construction and Checking of eBPF Loops
• Dominique Larchey-Wendling. Quasi Morphisms for Almost Full Relations
• Benno van den Berg. Recent progress in the theory of effective Kan fibrations in simplicial sets
• Axel Ljungström and David Wärn. Revisiting the Steenrod Squares in HoTT
• Daniël Otten and Matteo Spadetto. Semantics of Axiomatic Type Theory
• Hugo Herbelin. Size-preserving dependent elimination
• Kenji Maillard. Splitting Booleans with Normalization-by-Evaluation
• Viktor Bense, Ambrus Kaposi and Szumi Xie. Strict syntax of type theory via alpha-normalisation
• Freek Geerligs, Thierry Coquand and Felix Cherubini. Synthetic Stone duality
• Felix Bradley and Zhaohui Luo. Temporal Operators for Dependent Event Types
• Fahad Alhabardi and Anton Setzer. Termination-checked Solidity-style smart contracts in Agda in the presence of Turing completeness
• Dominik Kirst and Haoyi Zeng. The Blurred Drinker Paradox and Blurred Choice Axioms for the Downward Löwenheim-Skolem Theorem
• Niels van der Weide. The Internal Language of Univalent Categories
• Nima Rasekh, Niels van der Weide, Benedikt Ahrens and Paige Randall North. The Univalence Maxim and Univalent Double Categories
• Bruno Barras, Thiago Felicissimo and Théo Winterhalter. Towards a logical framework modulo rewriting and equational theories
• Yulong Huang and Jeremy Yallop. Towards Quantitative Inductive Families
• Ambrus Kaposi and Szumi Xie. Type theory in type theory using single substitutions
• Kanstantsin Nisht and Andreas Abel. Type-Based Termination Checking in Agda
• Håkon Robbestad Gylterud and Elisabeth Bonnevier. Univalent Material Set Theory: Hierarchies of n-types
• Ulrik Buchholtz, Daniel Gratzer and Jonathan Weinberger. Universes in simplicial type theory
• Jacob Neumann. Updates on Paranatural Category Theory
• Pablo Barenbaum, Delia Kesner and Mariana Milicich. Useful Evaluation, Quantitatively
• Reynald Affeldt, Alessandro Bruni, Pierre Roux and Takafumi Saikawa. Yet another formal theory of probabilities (with an application to random sampling)

SPONSORS

HOST