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;
formalizing mathematics using type theory;
links between type theory and
functional programming;
homotopy theory;
linguistics;
machine learning.
We encourage talks proposing new ways of applying 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.
Contributed Talks
TYPES solicits contributed talks to stimulate discussions. Selection of those will be based on extended abstracts of 2 pages.
Submission instructions
Extended abstracts:
are limited to 2 pages (not counting the bibliography),
Sebastian Ullrich (Lean Focused Research Organization)
Josef Urban (Czech Technical University in Prague, Czech Republic)
Nicolas Tabareau (INRIA, MTI Atlantique, Nantes University, France)
Niccolò Veltri (Tallinn University of Technology, Estonia)
Stephanie Weirich (University of Pennsylvania, US)
Post-proceedings
A post-proceedings volume will be published in the Leibniz International Proceedings in Informatics (LIPIcs) series. Submission to that volume will be open to everyone.
Tentative submission deadline for the post-proceedings: October 2026.