TYPES 2023
29th International Conference on Types for Proofs and Programs

TALKS AND SLIDES

Yannick Forster. Verified Extraction from Coq to OCaml. Invited Talk
Simona Ronchi della Rocca. Intersection and Simple types. Invited Talk (Talk recording)
Marie Kerjean. The differentiation monad. Invited Talk (Talk recording)
Andrej Bauer. On Isomorphism Invariance and Isomorphism Reflection in Type Theory. Invited Talk (Slides; Talk recording)
Ulrik Buchholtz, Tom de Jong and Egbert Rijke. On epimorphisms and acyclic types in univalent type theory (Slides; Talk recording)
Tom de Jong, Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu. The ordinals in set theory and type theory are the same (Slides; Talk recording)
Thiago Felicissimo. A Logical Framework for Computational Type Theories (Slides;Talk recording)
Lauren White, Laura Titolo and J. Tanner Slagel. Embedding Differential Temporal Dynamic Logic in PVS
Luís Cruz-Filipe, Lovro Lugović, Fabrizio Montesi, Marco Peressotti and Robert R. Rasmussen. Choreographic Programming in Coq (Slides; Talk recording)
Andreas Nuyts. Lax-Idempotent 2-Monads, Degrees of Relatedness, and Multilevel Type Theory (Slides; Talk recording)
András Kovács. Efficient Evaluation for Cubical Type Theories
Matthias Eberl. Dynamic Type Theory
Sam van Gool, Paul-André Melliès and Vincent Moreau. Profinite lambda-terms and parametricity (Talk recording)
Patrick Bahr and Rasmus Ejlers Møgelberg. Modal Types for Asynchronous FRP (Slides; Talk recording)
Andrej Dudenhefner, Felix Laarmann, Jakob Rehof and Christoph Stahl. Finite Combinatory Logic extended by a Boolean Query Language for Composition Synthesis
Benedikt Ahrens, Ralph Matthes and Kobe Wullaert. Formalized non-wellfounded syntax through monoidal categories
Ammar Karkour and Giselle Reis. A Formalization of Python's Execution Machinery (Slides; Talk recording)
Luc Chabassier and Bruno Barras. A graphical interface for diagrammatic proofs in proof assistants (Slides; Talk recording)
Thorsten Altenkirch and Stefania Damato. Revisiting Containers in Cubical Agda (Slides;Talk recording)
Daniël Otten and Benno van den Berg. Conservativity of Type Theory over Higher-order Arithmetic
Niels van der Weide. Enriched Categories in Univalent Foundations (Slides;Talk recording)
Yuta Takahashi. Towards an Interpretation of Inaccessible Sets in Martin-Löf Type Theory with One Mahlo Universe (Slides; Talk recording)
Joshua Chen, Tom de Jong, Nicolai Kraus and Stiephen Pradal. Categories as Semicategories with Identities (Slides; Talk recording)
Greta Coraglia and Jacopo Emmenegger. Categorical models of subtyping (Talk recording)
Jelle Wemmenhove, Cosmin Manea and Jim Portegies. Classification of Covering Spaces and Canonical Change of Baspoint (Slides; Talk recording)
Meven Lennon-Bertrand and Neel Krishnaswami. Decidable Type-Checking for Bidirectional Martin-Löf Type Theory (Slides;Talk recording)
Mohammad Shaheer, Giselle Reis and Bruno Woltzenlogel Paleo. Formalization of Blockchain Oracles in Coq (Slides; Talk recording)
Jesper Cockx. Operations On Syntax Should Not Inspect The Scope (Talk recording)
Théo Winterhalter. Composable partial functions in Coq, totally for free (Slides; Talk recording)
Jacob Neumann. Categorical Logic in Lean (Slides; Talk recording)
Lukas Abelt and Alcides Fonseca. LayeredTypes - Combining dependent and independent type systems (Slides; Talk recording)
Pierre Cagne and Patricia Johann. Partiality Wrecks GADTs' Functoriality (Slides; Talk recording)
Francesco Gavazzo, Riccardo Treglia and Gabriele Vanoni. Monadic Intersection Types (*)
Arthur Adjedj, Meven Lennon-Bertrand, Kenji Maillard and Loic Pujet. Engineering logical relations for λΠ□ in Coq (Talk recording)
Andreas Nuyts. A Lock Calculus for Multimode Type Theory (Slides; Talk recording)
Valentin Blot. Diller-Nahm Bar Recursion (Slides; Talk recording)
Gaëtan Gilbert, Yann Leray, Nicolas Tabareau and Théo Winterhalter. The Rewster: The Coq Proof Assistant with Rewrite Rules (Slides; Talk recording)
Bohdan Liesnikov and Jesper Cockx. Building an elaborator using extensible constraints (Slides; Talk recording)
Josselin Poiret, Andreas Nuyts, Joris Ceulemans, Malin Altenmüller and Lucas Escot. Read the mode and stay positive (Slides; Talk recording)
Hugo Herbelin and Dominik Kirst. New Observations on the Constructive Content of First-Order Completeness Theorems (Slides; Talk recording)
Pierre-Marie Pédrot, Nicolas Tabareau, Matthieu Sozeau and Gaëtan Gilbert. From Lost to the River: Embracing Sort Proliferation (Slides; Talk recording)
Yannick Forster, Dominik Kirst, Bruno da Rocha Paiva and Vincent Rahli. Markov’s Principles in Constructive Type Theory
Assia Mahboubi and Guillaume Melquiond. Manifest Termination
Peio Borthelle, Tom Hirschowitz, Guilhem Jaber and Yannick Zakowski. Games and Strategies using Coinductive Types (Slides; Talk recording)
Murdoch J. Gabbay and Orestis Melkonian. Nominal techniques as an Agda library (Slides; Talk recording)
Beniamino Accattoli, Adrienne Lancelot and Claudia Faggian. Normal Form Bisimulations by Value (Slides)
Herman Geuvers and Tonny Hurkens. Self-contained rules for classical and intuitionistic quantifiers (Slides; Talk recording)
Moana Jubert and Hugo Herbelin. Higher coherence equations of semi-simplicial types as n-cubes of proofs (Slides; Talk recording)
Felix Bradley and Zhaohui Luo. On the Metatheory of Subtype Universes
Fahad Alhabardi and Anton Setzer. A simple model of smart contracts in Agda (Slides; Talk recording)
Orestis Melkonian, Wouter Swierstra and James Chapman. Program logics for ledgers (Slides; Talk recording)
Lykourgos Mastorou, Niki Vazou and Michael Greenberg. Towards a Translation from Liquid Haskell to Coq (Slides; Talk recording)
Kobe Wullaert and Niels van der Weide. Rezk Completion of Structured Categories
Ambrus Kaposi. Towards quotient inductive-inductive-recursive types (Slides; Talk recording)
Michal Konecny, Sewon Park and Holger Thies. Extending cAERN to spaces of subsets
Paige North and Maximilien Péroux. Coinductive control of inductive data types (Slides; Talk recording)
José Espírito Santo, Dylan McDermott, Luís Pinto and Tarmo Uustalu. Consequences of the modal unification of the functional calling paradigms
Kazuhiko Sakaguchi. A record expansion translation for Coq
Cas van der Rest and Casper Bach Poulsen. Types and Semantics of Extensible Data Types (Slides; Talk recording)
José Espírito Santo, René Gazzari and Luís Pinto. Terms as Types: Calculations in the lambda-Calculus
Nuria Brede, Tim Richter, Patrik Jansson and Nicola Botta. Extensional Equality Preservation in Intensional MLTT (Slides; Talks recording)
Artjoms Sinkarovs and Sven-Bodo Scholz. Rank-polymorphic arrays within dependently-typed languages (Slides; Talk recording)
Thorsten Altenkirch, Ambrus Kaposi, Artjoms Sinkarovs and Tamás Végh. Towards dependent combinator calculus (Slides; Talk recording)
Ariel Grunfeld, Liron Cohen and Ross Tate. Monadic Realizability for Intuitionistic Higher-Order Logic (*)
 
(*): Video recording not available due to technical problems.
 

SPONSORS

UPV