European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

Dates: 17-18 April 2025

Place: Genova, Italy

Venue:
Villa Giustiniani-Cambiaso,
Scuola Politecnica, Università di Genova
via Montallegro 1, Genova 16145

⚠️⚠️ Please beware of accommodation-related scam emails targeting this specific event.⚠️⚠️

Co-located with the HoTT/UF 2025 Workshop.

The aim of this meeting series is to bring together researchers working on the topics of Working Group 6 of EuroProofNet. The main focus is thus on the syntax and semantics of type theory. This includes, but is not limited to the goal of WG6:

The aim of this WG is to develop a comprehensive theory of type theories, which (i) accounts for its domain-specific variants and the type theories currently used in proof assistants, and (ii) allows for the modular reasoning about their syntax and semantics.

The meeting will be in person with support for remote participation and is open to anyone interested in type theory. Talks can present published work or work in progress.

Schedule and abstracts: please see here.

Invited speakers

Contributed talks

  • Thorsten Altenkirch (University of Nottingham)
    Containers in Higher Kinds [Abstract]
  • Mathis Bouverot-Dupuis (Ecole Normale Supérieure Paris)
    Code Generation via Meta-programming in Dependently Typed Proof Assistants [Abstract]
  • Cipriano Junior Cioffo (University of Pisa)
    A categorical account of the setoid model [Abstract]
  • Stefania Damato (University of Nottingham)
    Distributive Laws for Monadic Containers [Abstract]
  • Michele De Pascalis (Tallinn University of Technology)
    Monoid Structures on Indexed Containers [Abstract]
  • Maximilian Doré (University of Oxford)
    Linear Types with Dynamic Multiplicities in Dependent Type Theory [Abstract]
  • Andrea Giusto (University of Genoa)
    Fibrations with comprehension and their completion [Abstract]
  • Andrea Laretto (Tallinn University of Technology)
    Directed First-Order Logic [Abstract]
  • Niyousha Najmaei (Ecole Polytechnique Palaiseau)
    Syntax for non-full comprehension categories [Abstract]
  • Jacob Neumann (University of Nottingham)
    GATs, Cats, and CwFs: A Celestial Dance [Abstract]
  • Samuel Novotný (Technical University of Košice)
    Towards Resolving Type Inconsistencies in Transparent Intensional Logic [Abstract]
  • Lorenzo Perticone (Chalmers University of Technology)
    Parametric Distributive Laws: uniform monad composition [Abstract]
  • Iosif Petrakis (University of Verona)
    Categories with dependent and codependent arrows [Abstract]
  • Daniel Ranalter (University of Innsbruck)
    Erasure-Respecting Semantics for DHOL [Abstract]
  • Pietro Sabelli (Czech Academy of Sciences)
    On the conservativity of type theories with classical logic over arithmetic [Abstract]
  • Matteo Spadetto (Università degli Studi di Udine)
    A 2-categorical approach to the sematics of axiomatic dependent type theory [Abstract]
  • Théo Winterhalter (INRIA Saclay)
    Local abstraction over computation in type theory [Abstract]

Deadlines (AoE)

  • Submission of talk proposals: Friday 28 February
  • Author notification: Tuesday 4 March
  • Funding request: Friday 7 March
  • Registration: Friday 28 March

Submission of talk proposals: closed.

Registration: To register, please fill out this form.

Local information: Please see here.

Organizers: Francesco Dagnino and Jacopo Emmenegger