The Coq mailing list

[Fredrik Nordvall Forsberg <fredrik.nordvall-forsberg AT strath.ac.uk>]

                 Call for Participation

                      TYPES 2025
           31st International Conference on
             Types for Proofs and Programs

         Glasgow, Scotland, 9 -- 13 June 2025
        https://msp.cis.strath.ac.uk/types2025/

REGISTRATION
------------

Registration is now open; see 
https://msp.cis.strath.ac.uk/types2025/registration.html
for more information.

* Early registration until 12 May
* Late registration until 30 May

Students can register at a reduced fee. For details, see the above link.

Researchers from COST Inclusiveness Target Countries are reminded that
the European Research Network on Formal Proofs COST action has some
funding available for conference attendance, with a deadline of 4 May, see
https://europroofnet.github.io/grants/ .


INVITED SPEAKERS
----------------

Ingo Blechschmidt (University of Antwerp)
Sonia Marin (University of Birmingham)
Chris Martens (Northeastern University)
Christian Sattler (Chalmers University of Technology and University of 
Gothenburg)


CONTRIBUTED TALKS
-----------------

A list of accepted contributed talks can be found at 
https://msp.cis.strath.ac.uk/types2025/accepted.html .


COLOCATED EVENTS
----------------

* 10 June: Women in EuroProofNet 
(https://europroofnet.github.io/women-epn-2025/ )
* 16 -- 20 June: CALCO 2025 & MFPS XLI 
(https://www.coalg.org/calco-mfps-2025/ )


BACKGROUND
----------

The TYPES meetings are a forum to present new and ongoing work in all
aspects of type theory and its applications, especially in formalised
and computer assisted reasoning and computer programming.

The TYPES areas of interest include, but are not limited to:

* foundations of type theory and constructive mathematics;
* applications of type theory;
* dependently typed programming;
* industrial uses of type theory technology;
* meta-theoretic studies of type systems;
* proof assistants and proof technology;
* automation in computer-assisted reasoning;
* links between type theory and functional programming;
* formalizing mathematics using type theory.

In the spirit of workshops, talks may be based on newly published papers,
work submitted for publication, but also work in progress. Participation
in the meeting is primarily in person, as face-to-face interactions
are highly valuable. If you need to discuss remote participation,
please contact the organisers.


VISA ISSUES
-----------

Note that even if you are lucky enough to not require a visa to enter 
the UK,
you might still need to apply for electronic travel authorisation (ETA). 
In particular,
this applies to EU citizens. You can check what you need here:

https://www.gov.uk/check-uk-visa

If you do need a visa, we are happy to write you a letter of invitation,
confirming that you have registered for the conference. See the 
registration page for
more details.


SPONSORS
--------

Jane Street (Gold Sponsor)
Formal Vindications
Well-Typed
IOG
Tunnock's (Caramel Wafer sponsor)


PROGRAMME COMMITTEE
-------------------

Danel Ahman (University of Tartu, Estonia)
Guillaume Allais (University of Strathclyde, Scotland)
Malin Altenmüller (University of Edinburgh, Scotland)
Sandra Alves (University of Porto, Portugal)
Casper Bach (University of Southern Denmark, Denmark)
Ana Bove (Chalmers and University of Gothenburg, Sweden)
Liang-Ting Chen (Academia Sinica, Taiwan)
Vikraman Choudhury (University of Bologna, Italy)
Gilda Ferreira (Universidade Aberta, Portugal)
Daniel Gratzer (Aarhus University, Denmark)
Tom de Jong (University of Nottingham, England)
Dominik Kirst (Inria Paris, France)
Neel Krishnaswami (University of Cambridge, England)
András Kovács (University of Gothenburg and Chalmers, Sweden)
Peter LeFanu Lumsdaine (Stockholm University, Sweden)
Kenji Maillard (Inria Rennes-Bretagne Atlantique, France)
Max New (University of Michigan, United States of America)
Fredrik Nordvall Forsberg (University of Strathclyde, Scotland) (chair)
Elaine Pimentel (University College London, England)
Andrew Swan (University of Ljubljana, Slovenia)
Tarmo Uustalu (Reykjavík University, Iceland)
Niels van der Weide (Radboud University Nijmegen, The Netherlands)
Théo Winterhalter (Inria Saclay, France)
Maaike Zwart (IT University Copenhagen, Denmark)


TYPES STEERING COMMITTEE
------------------------

Eduardo Hermo Reyes (Formal Vindications, Spain)
Tom de Jong (University of Nottingham, England)
Rasmus Ejlers Møgelberg (IT University of Copenhagen, Denmark)
Fredrik Nordvall Forsberg (University of Strathclyde, Scotland)
Paige Randall North (Utrecht University, The Netherlands) (chair)
Benno van den Berg (University of Amsterdam, The Netherlands) (secretary)


ABOUT TYPES
-----------

The TYPES meetings from 1990 to 2008 were annual workshops of a sequence
of five EU funded networking projects. From 2009 onwards, TYPES has been
run as an independent conference series. Previous TYPES meetings were
held in Antibes (1990), Edinburgh (1991), Båstad (1992), Nijmegen
(1993), Båstad (1994), Torino (1995), Aussois (1996), Kloster Irsee
(1998), Lökeberg (1999), Durham (2000), Berg en Dal near Nijmegen
(2002), Torino (2003), Jouy-en-Josas near Paris (2004), Nottingham
(2006), Cividale del Friuli (2007), Torino (2008), Aussois (2009),
Warsaw (2010), Bergen (2011), Toulouse (2013), Paris (2014), Tallinn
(2015), Novi Sad (2016), Budapest (2017), Braga (2018), Oslo (2019),
Virtual (2021), Nantes (2022), València (2023), Copenhagen (2024).


CONTACT
-------

Email: CIS_types2025 AT groups.strath.ac.uk


ORGANISERS
----------

Guillaume Allais (University of Strathclyde, Scotland)
Stuart Gale (University of Strathclyde, Scotland)
Fredrik Nordvall Forsberg (University of Strathclyde, Scotland)