TYPES 2025 postproceedings published

[Fredrik Nordvall Forsberg]

Dear all,

It is our pleasure to announce that the postproceedings of the 31st
International
Conference on Types for Proofs and Programs (TYPES 2025) is now available
open access from LIPIcs:

https://www.dagstuhl.de/dagpub/978-3-95977-441-3

The volume consists of the following papers:

* Owen Milner
  Choice Principles and Hypercompletion in HoTT
  https://doi.org/10.4230/LIPIcs.TYPES.2025.1

* Mario Carneiro
  Lean4Lean: Verifying a Typechecker for Lean, in Lean
  https://doi.org/10.4230/LIPIcs.TYPES.2025.2

* Vikraman Choudhury and Wind Wong
  Symmetries in Sorting
  https://doi.org/10.4230/LIPIcs.TYPES.2025.3

* Brandon Hewer and Graham Hutton
  HoTT Operads
  https://doi.org/10.4230/LIPIcs.TYPES.2025.4

* Robin Adams, Jean-Philippe Bernardy, Lorenzo Perticone, and Jeremy Pope
  A Graded Modal Type Theory for Pulse Schedules
  https://doi.org/10.4230/LIPIcs.TYPES.2025.5

* Casper Ståhl, Levs Gondelman, René Rydhof Hansen, and Danny Bøgsted
Poulsen
  Formalisation and Extension of Lagois Connections for Secure
Information Flow
  https://doi.org/10.4230/LIPIcs.TYPES.2025.6

* Besik Dundua, Furio Honsell, Temur Kutsia, Marina Lenisa, and Luigi
Liquori
  Towards Fuzzy Constructive Type Theories
  https://doi.org/10.4230/LIPIcs.TYPES.2025.7

* Kobe Wullaert and Niels van der Weide
  The Rezk Completion for Elementary Topoi
  https://doi.org/10.4230/LIPIcs.TYPES.2025.8

* Moana Jubert
  Kleisli Categories with Display Maps
  https://doi.org/10.4230/LIPIcs.TYPES.2025.9

* Evan Cavallo and Thierry Coquand
  Type-Theoretic Replacement and Univalent Completion: Applications and
Interpretations
  https://doi.org/10.4230/LIPIcs.TYPES.2025.10

* Rasmus Ejlers Møgelberg
  Multi-Clocked Guarded Recursion Beyond ω
  https://doi.org/10.4230/LIPIcs.TYPES.2025.11

* Antoine Van Muylder, Andreas Nuyts, and Dominique Devriese
  Nominal Type Theory by Nullary Internal Parametricity
  https://doi.org/10.4230/LIPIcs.TYPES.2025.12

* Malin Altenmüller and Conor Titania Mc Bride
  A Data Type of Intrinsically Plane Graphs in Agda
  https://doi.org/10.4230/LIPIcs.TYPES.2025.13

* Enrique Ruiz Hernández and Pedro Solórzano
  Functional Representability in Local Set Theories
  https://doi.org/10.4230/LIPIcs.TYPES.2025.14

* Stephan Alexander Spahn
  Mendler Dialgebras and Recursion Schemes of Mixed Variance
  https://doi.org/10.4230/LIPIcs.TYPES.2025.15

Thanks again to all authors and reviewers for all the hard work
going into making this an excellent volume!

Best wishes,
Fredrik Nordvall Forsberg and James McKinna
editors TYPES 2025 postproceedings