TYPES 2027, the 33rd International Conference on Types for Proofs and Programs, invites contributions on all aspects of type theory and its applications. The conference takes place in Udine, Italy, on 7-11 June 2027.
Scope
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. Topics 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;
- formalising mathematics using type theory;
- homotopy type theory and univalent foundations.
Participation is open to everybody working on or interested in these topics, whether or not they contribute a talk.
Contributed talks
Presentations are selected on the basis of an extended abstract of at most two pages, references included. Submitted abstracts are reviewed by the programme committee for relevance and quality; work in progress, work already presented elsewhere and overviews of larger projects are all in scope, as long as they are of interest to the TYPES community.
Full details are in the submission section below.
Invited speakers
to be announced
The invited speakers will be announced here well before the abstract submission deadline.
Post-proceedings
As in recent editions of the conference series, we intend to publish post-proceedings in the Leibniz International Proceedings in Informatics (LIPIcs) series. The call for papers is expected to open after the conference and to be open to all participants, not only to those who presented a talk. Submissions are full papers, reviewed to the standards of a journal publication.
Publication details, including page limits and the exact timeline, will be confirmed on this page. to be confirmed
Submission
What to submit
A contribution to TYPES 2027 is an extended abstract of at most two pages, including references. The abstract should make clear what the contribution is, why it is of interest to the TYPES community, and what the author intends to present in the talk.
Abstracts are reviewed by the programme committee. Selection is based on relevance to the scope of the conference and on the quality of the abstract; the review process is light-touch, in keeping with the character of the TYPES meetings as a working conference.
Format
Abstracts must be prepared with the LIPIcs LaTeX class (currently
lipics-v2021) and submitted in PDF. The style bundle and the instructions for
authors are published by Dagstuhl on the
LIPIcs series page,
which always carries the current release; the sources and an issue tracker are
on GitHub.
Compile with pdflatex, keep the standard bibliography style
(\bibstyle{plainurl}), use the sectioning macros the class provides, and do
not override its defaults for fonts, spacing or colours.
The same class is used for the post-proceedings, so an abstract prepared this way is already a step towards the full paper.
Where to submit
Submission is handled through HotCRP.
The site accepts account registrations now; submission itself opens in good time before the deadline of 19 February 2027. Each HotCRP installation keeps its own accounts, so an account on the site of another conference does not carry over and authors need to register on the TYPES 2027 instance. Abstracts can be revised there up to the deadline.
After acceptance
At least one author of each accepted abstract is expected to register and to present the contribution in Udine. Accepted abstracts are collected in a book of abstracts distributed to participants and published on this website.
A separate call for full papers for the post-proceedings is expected to open after the conference.
Important dates
| Event | Date |
|---|---|
| Abstract submission deadline | |
| Author notification | |
| Early registration deadline | |
| Camera-ready version deadline | |
| Late registration deadline | |
| TYPES 2027 conference |
All deadlines are anywhere on Earth (AoE).