23rd International Conference on Types for Proofs and Programs,
TYPES 2017

Budapest, Hungary, 29 May - 1 June 2017

Background   Financial support   Invited speakers   Call for contributions   Registration   Programme   Accepted papers   Program committee   Venue   Accommodation   Contact

Budapest Tram Budapest Panorama HDR


The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalised and computer assisted reasoning and computer programming. The meetings from 1990 to 2008 were annual workshops of a sequence of five EU funded networking projects. Since 2009, 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).

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

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.

Financial support

The first two days of TYPES 2017, May 29 - 30 are organised by EUTypes Cost Action CA15123. On May 30 there will be an EUTypes Management Committee (MC) meeting, and on both days there will be WG meetings. This means that members of the EUTypes MC will be invited for these 2 days through the e-cost system, and their cost of travel and stay will be covered. There will likely be some funding for a limited number of other invited speakers. The funding is subject to COST rules, and invitations will be sent out via the e-cost system after the 1st of May.

Invited speakers

Contributed talks

We solicit contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pp formatted with easychair.cls. The submission site is https://easychair.org/conferences/?conf=types2017.

Important dates:

Camera-ready versions of the accepted contributions will be published in an informal book of abstracts for distribution at the workshop.


The conference early registration fee will be approximately 300 EUR for normal participants and 230 EUR for students. This will include daily lunches, coffee breaks, conference dinner and excursion.

We will inform everyone who will present a paper as soon as registration opens.


Program plan for Monday (29 May), Wednesday (31 May) and Thursday (1 June). Talks will last 20 minutes including questions. On Monday and Tuesday, 6 slots will be taken up by EUTypes MC and WG meetings.

9.00-10.00invited talk
10.00-10.30coffee break
10.30-12.30talks (6 slots)
14.20-16.00talks (5 slots)
16.10-16.30coffee break
16.30-18.10talks (5 slots)

Program plan for Tuesday (30 May).

9.00-10.00talks (3 slots)
10.00-10.30coffee break
10.30-12.30talks (6 slots)
12.30-14.30coffee break
from 14.30 excursion

Accepted papers

Ian Orton and Andrew Pitts. Axioms for Univalence
Andrej Dudenhefner and Jakob Rehof. Lower End of the Linial-Post Spectrum
Patrick Bahr, Hans Bugge Grathwohl and Rasmus Ejlers Møgelberg. The Clocks Are Ticking: No More Delays! Reduction Semantics for Type Theory with Guarded Recursion
Aleš Bizjak and Rasmus Ejlers Møgelberg. Presheaf semantics for guarded dependent type theory
Thomas Winant, Jesper Cockx and Dominique Devriese. Expressive and Strongly Type-Safe Code Generation
Elvis Marlon Detty. Beque: a Library to Model and Reason About I/O in Coq
Sergei Soloviev. On Certain Group Structures in Type Theory
Francisco Ferreira, David Thibodeau and Brigitte Pientka. Dependent Type Theory with Contextual Types
Thierry Coquand, Bassel Mannaa and Fabian Ruch. A Model of Type Theory in Stacks
Colin Riba and Pierre Pradic. A Curry-Howard Approach to Church's Synthesis
Bogdan Aman and Gabriel Ciobanu. A Probabilistic Approach of Behavioural Types
Thibaut Balabonski, Marco Gaboardi, Chantal Kelller and Benoît Valiron. Regularity for Free
Luís Cruz-Filipe, Joao Marques-Silva and Peter Schneider-Kamp. The Boolean Pythagorean Triples Problem in Coq
Georgiana Elena Lungu and Zhaohui Luo. Extensions by Definition in Type Theory
Delia Kesner and Pierre Vial. Quantitative Types for the Lambda-Mu Calculus with Explicit and Implicit Replacement
Valentin Blot. An interpretation of system F through bar recursion
Amin Timany, Matthieu Sozeau and Bart Jacobs. Cumulative inductive types in Coq
Pierre-Marie Pédrot and Nicolas Tabareau. An Effectful Way to Eliminate Addiction to Dependence
José Espírito Santo, Ralph Matthes and Luís Pinto. Inhabitation in Simply-Typed Lambda-Calculus through a Lambda-Calculus for Proof Search
Rodolphe Lepigre. Theory and Demo of PML2: Proving Programs in ML
Benedikt Ahrens, Ralph Matthes and Anders Mörtberg. Syntax from multi-sorted binding signatures
Guillaume Brunerie. The Steenrod squares in homotopy type theory
Neil Ghani, Conor McBride, Fredrik Nordvall Forsberg and Stephan Spahn. Inductive-Recursive Definitions and Composition
Guillaume Allais. Typing with Leftovers: a Mechanisation of ILL
Branislava Živković and Milena Vujosevic Janicic. Parallelization of Software Verification Tool LAV
Robin Adams and Andrew Polonsky. A Type Theory with Native Homotopy Universes
Luigi Liquori and Claude Stolze. Intersection and Union Types from a Proof-functional Point of View
Adam Naumowicz. Adjective Clustering in the Mizar Type System
Jose Espirito Santo and Silvia Ghilezan. Characterization of strong normalizability for a lambda-calculus with co-control
Thorsten Altenkirch and Gun Pinyo. Monadic containers and universes
Thorsten Altenkirch. From setoid hell to homotopy heaven?
Manuel Bärenz and Sebastian Seufert. Verifying Functional Reactive Programs with Side Effects
Andrej Bauer, Philipp G. Haselwarter and Théo Winterhalter. A modular formalization of type theory in Coq
Thorsten Altenkirch, Paolo Capriotti, Thierry Coquand, Nils Anders Danielsson, Simon Huber and Nicolai Kraus. Type Theory with Weak J
Thorsten Altenkirch, Ambrus Kaposi and András Kovács. Normalisation by Evaluation for a Type Theory with Large Elimination
G. A. Kavvos. A Type-Theoretic Alternative to LISP
Felix Rech and Steven Schäfer. A Small Basis for Homotopy Type Theory
Nils Anders Danielsson and Víctor López Juan. Towards practical and sound out-of-order unification
Paolo Capriotti. Notions of type formers
Stefan Ciobaca and Vlad Andrei Tudose. Automatically Constructing a Type System from the Small-Steps Semantics
David Baelde, Amina Doumane, Guilhem Jaber and Alexis Saurin. Bouncing threads for infinitary proof theory
Ambrus Kaposi, András Kovács, Péter Diviánszky and Balázs Kőműves. Derivation of elimination principles from a context
Frederic Gilbert. Verifiable certificates for predicate subtyping
Gilles Dowek. Models and termination of proof reduction in the lambda Pi-calculus modulo theory
Tarmo Uustalu and Niccolò Veltri. Partiality and container monads
Gilles Dowek, Jean-Pierre Jouannaud, Assaf Ali and Jiaxiang Liu. Untyped Confluence In Dependent Type Theories
Thorsten Altenkirch, Paolo Capriotti and Bernhard Reus. Domain Theory in Type Theory via QIITs
Andreas Nuyts, Andrea Vezzosi and Dominique Devriese. Parametric Quantifiers for Dependent Types
Andreas Abel, Andrea Vezzosi and Théo Winterhalter. Normalization by Evaluation for Sized Dependent Types
Bashar Igried and Anton Setzer. Strong Bisimilarity Implies Trace Semantics in CSP-Agda
Anton Setzer. Modelling Bitcoins in Agda


Similarly to TYPES 2011 and TYPES 2013-2016, we intend to publish a post-proceedings volume in the Leibniz International Proceedings in Informatics (LIPIcs) series. Submission to that volume will be open for everyone. Tentative submission deadline: September 2017.

Program committee


The conference will be held in the Lágymányos South Building of Eötvös Loránd University, see the map below. The address is Pázmány Péter sétány 1/C, Budapest 1117, Hungary.


We reserved 55 rooms altogether in the following hotels (see the above map):

To get the above prices, please fill out the booking form and send it to the hotel through email, fax or post or just call the hotel.

Services such as booking.com and airbnb.com are known to work well in Budapest too.

The judgemental map of Budapest (google) is quite accurate about what the different areas are like. The conference venue is in the "more nerds" area.


Email: info@types2017.elte.hu

Organisers: Ambrus Kaposi, Tamás Kozsik, András Kovács and the Department of Programming Languages and Compilers at the Faculty of Informatics, Eötvös Loránd University.

Last update: 3 April 2017