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.

Workshop group photo

Date: 4-5 April 2024, in co-location with the HoTT/UF 2024 Workshop.

Place: Leuven, Belgium

Venue: Dept. of Computer Science
Celestijnenlaan 200A
3001 Heverlee (Leuven)
Talks: Auditorium Erik Duval, 200A.00.225
Collaborative room: Seminar room 200A.00.144
Livestream: https://livestream.kuleuven.be/?pin=829052
Note: If it freezes or does not load, reloading can help.

Local information - ⚠️⚠️ Please beware of accommodation-related scam emails targetting this specific event. ⚠️⚠️

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 programme will consist mainly of short talks and plenty of time for discussion. The meeting will be in person and is open to anyone interested in type theory. Talks can expose published work or work in progress. Submissions of open questions and topics to be discussed collectively are also welcome: please use the same form and clearly mark your entry as a discussion proposal, we will try to organize a few short discussion sessions.

Schedule and abstracts: Please see here

Invited speakers

Contributed talks

  • Vincent R.B. Blazy, Hugo Herbelin & Pierre Letouzey (Université Paris Cité): Explicit Cumulativity in CC_ω (Abstract - Slides - Video)
  • Joris Ceulemans, Andreas Nuyts, Dominique Devriese (KU Leuven): Admissibility of Substitution for Multimode Type Theory (Abstract - Slides - Video)
  • Joshua Chen, Nicolai Kraus (University of Nottingham): Constructing inverse diagrams in homotopical type theory (Abstract - Slides - Video)
  • Thiago Felicissimo (Inria/LMF/Deducteam): Generic bidirectional typing for dependent type theories (Abstract - Slides - Video)
  • Jonas Frey (Carnegie Mellon University): The shape of contexts (Abstract - Slides - Video)
  • Ambroise Lafont, Thomas Lamiaux, Benedikt Ahrens (École Polytechnique, ENS Saclay, Delft University of Technology): Initial semantics for polymorphic type systems (Abstract - Slides)
  • Roussanka Loukanova (Department of Algebra and Logic, Institute of Mathematics and Informatics, Bulgarian Academy of Sciences): Relations between let-Terms of Lambda-Calculus and where-Terms of Type-Theory of Recursion (Abstract - Slides - Video)
  • Jacob Neumann (University of Nottingham): Towards Modal SOGATs (Abstract - Blackboard - Video)
  • Josselin Poiret (Nantes Université and Inria, Galinette Team): A multiverse type theory (Abstract - Slides - Video)
  • Stelios Tsampas (Friedrich-Alexander-Universität Erlangen-Nürnberg): Logical Relations in Higher-Order Mathematical Operational Semantics (Abstract - Slides - Video)
  • Théo Winterhalter (Inria Saclay): Dependent ghosts enjoy reflection for free (Abstract - Slides - Video)

Deadlines

  • Submission of talk proposals: 2 February 2024 / 9 February 2024 (AoE)
  • Author notification: 16 February 2024
  • Funding requests: 23 February 2024 (AoE)
    • Please register also as EuroProofNet member (see below) by this deadline.
  • Funding notification: 4 March 2024
  • Registration: 8 March 2024 15 March 2024 (AoE)
  • Meeting itself: 4-5 April 2024

Funding: The reimbursement concerns the official dates of the WG6 meeting: Apr 4-5 (so not the co-located event). For information regarding reimbursement, please see here. The daily allowance has been fixed to 140 euros.

The action members who will be reimbursed will be selected among the applicants by taking into account the following criteria in order: planned contributions to the objectives and deliverables of the action; inclusive target countries; age; gender; team with low resources; balance over the action life time between people, teams, countries and working groups.

To apply for funding, fill out the funding and registration form before February 23. You can still confirm or cancel your registration after a decision on awarding funding has been made.

Please note that, in order to be eligible for reimbursement, you ALSO need to register as a EuroProofNet member. Information on how to apply can be found on the EuroProofNet home page, and the link to register as a EuroProofNet member is https://e-services.cost.eu/action/CA20111/working-groups/apply. Choose any work groups you like, but in particular WG6.

Current membership can be checked here (not alphabetical, despite appearances).

Submission of proposals: Submission form (Submission is closed.)

Registration: Registration form

Local information: Please see here.

Organizers: Marie Kerjean and Andreas Nuyts

Local Organizer: Andreas Nuyts