TYPES 2024
30th International Conference on Types for Proofs and Programs, 10 ‑ 14 June 2024

Slides

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

IT University of Copenhagen