21st International Conference on Types for Proofs and Programs,
TYPES 2015

Tallinn, Estonia, 18-21 May 2015


Invited talks + tutorials

Programme (with slides) - Book of abstracts - Participants


TYPES 2015 places on a Google map - TYPES 2015 places on a Delfi map

Travel information

(please register by 8 May!)

Photography by Marko Leppik

360 deg Tallinn panoramas


The TYPES meetings are a forum to present new and on-going work in all aspects of type theory and its applications, especially in formalized 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).

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

We encourage talks proposing new ways of applying type theory.

Invited talks

Gilles Barthe (IMDEA Software)
Computer-aided cryptography

Andrej Bauer (University of Ljubljana)
The troublesome reflection rule

Peter Selinger (Dalhousie University)
Types for quantum computing


Joachim Kock (Universitat Autňnoma de Barcelona)
Polynomial functors: a general framework for induction and substitution

Peter LeFanu Lumsdaine (Stockholm University)
Higher inductive types: what we understand, what we don't

Contributed talks

We solicit contributed talks. Selection of those will be based on extended abstracts/short papers of 2 pp formatted with easychair.cls. Submission is via EasyChair by 20 March 2015 (was 13 March). The authors will be notified of acceptance/rejection by 10 April 2015 (was 3 April).

Camera-ready versions of the accepted contributions, due by 1 May 2015 (was 24 April), will be published in an informal book of abstracts for distribution at the workshop.


Similarly to TYPES 2011, 2013, 2014, we will publish a post-proceedings in the Leibniz International Proceedings in Informatics (LIPIcs) series. Submission to this volume is open for everyone. Intents to submit by 2 October 2015, papers due by 27 November 2015. See the call for details.

Programme committee

Andrea Asperti (Universitŕ di Bologna)
Robert Atkey (University of Edinburgh)
Ulrich Berger (Swansea University)
Jean-Philippe Bernardy (Chalmers University of Technology)
Edwin Brady (University of St Andrews)
Joëlle Despeyroux (INRIA Sophia Antipolis - Méditerranée)
Herman Geuvers (Radboud Universiteit Nijmegen)
Sam Lindley (University of Edinburgh)
Assia Mahboubi (INRIA Saclay - Ile de France)
Ralph Matthes (IRIT, CNRS and Université Paul Sabatier)
Aleksandar Nanevski (IMDEA Software)
Christine Paulin-Mohring (LRI, Université Paris-Sud)
Simona Ronchi Della Rocca (Universitŕ di Torino)
Ulrich Schöpp (Ludwig-Maximilians-Universität München)
Bas Spitters (Carnegie Mellon University → Aarhus Universitet)
Pawel Urzyczyn (University of Warsaw)
Tarmo Uustalu (Institute of Cybernetics, Tallinn) (chair)


Here is the programme.

For your travel planning, the conference will begin Mon 18 May morning at 9, so you should plan to arrive on Sun. On Thu 21 May we will end by 15.30. You can make it to any of the evening flights of Thu (they have departure times 17.30 and later).


The scientific programme will take place at the House of the Brotherhood of the Blackheads in the Old Town. (Those of you that attended ICFP 2005 in Tallinn - it was 10 years ago, can you imagine this! - will recognize the place.) We will also get lunches there.

Social programme

Mon 18 May evening we will have an excursion to and reception at the Seaplane Harbour. Wed 20 May evening we will have a banquet at Restaurant Platz in the Rotermanni quarter..


Please register here by 8 May (but preferrably soonest, this really helps us plan). The fee of 350 EUR covers both the coffee breaks and lunches during the four days of the meeting as well as the welcome reception Mon and banquet Wed. You can pay by credit card online or by bank transfer.


Please arrange your accommodation on your own. Meriton Old Town Garden Hotel is just across the street from the conference venue. Other recommendable mid-range hotels in the Old Town include Merchant's House, Savoy Boutique Hotel, Bern, Taanilinna, Meriton Old Town Hotel; in the immediate vicinity Nordic Hotel Forum, Meriton Grand Conference & Spa, L'Ermitage. Another option is to book an apartment in the Old Town, there are many providers. Check booking.com and Tripadvisor.


The main airlines serving Tallinn are Lufthansa, Finnair, Air Baltic and Estonian Air (in co-op with KLM, Brussels Airlines or SAS, depending on the route). You will most likely end up travelling via Frankfurt, Helsinki, Riga or Amsterdam/Brussels/Copenhagen/Oslo/Stockholm.

The airport is just 4 kms from the city center. So late arrival or early departure times are not to be feared.

Country information

In the nutshell: Estonia is in Schengen, uses the Euro, credit card payments are accepted almost universally (but not by drivers of cheaper taxis), in May we observe Eastern European Summer Time (=EEST=GMT+3), standard European power sockets, 220 V/50 Hz.


Logic and semantics group, Institute of Cybernetics, Tallinn University of Technology


ERDF through the EXCS and Coinduction projects

Tarmo Uustalu
Last update 14 September 2015