TYPES Meeting 2013 (April 22-26, 2013)

Post-conference news: post-proceedings appeared as vol.26 of LIPIcs on July 25, 2014

See here for an "Executive summary"

The 19th Conference "Types for Proofs and Programs" will take place in Toulouse, France, from 22 to 26 April 2013. The main conference will be held from April 23 (Tuesday) to 26 at Manufacture des Tabacs, Allée de Brienne, Toulouse - very close by foot to the old town center and the Garonne river (if you want to plan something with online maps, you may want to enter "toulouse school of economics" as search terms for the conference location).

Satellite events

Manufacture des Tabacs - seen from the canal

A marvellous picture of the town hall of Toulouse (6,6 MB, © Ville de Toulouse):

Le Capitole
© Ville de Toulouse

With institutional and/or financial support by: Université Toulouse 1 Capitole, Université Paul Sabatier, IRIT, FREMIT, Region Midi-Pyrénées and by So Toulouse

Logo UPS Logo IRIT Logo UT1 Logo Région Midi-Pyrénées Logo FREMIT Logo So Toulouse


The Types Meeting is 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. Since 1992, Types Meetings have been annual workshops of several multilateral scientific EU-financed projects, of which the Types Project was the most recent. Although organized in Europe, the meetings were always open internationally, as evidenced by invited speakers and authors of contributed talks. The previous TYPES meeting was held in Bergen, Norway in September 2011 and the one before in Warsaw, Poland in October 2010.

Topics and Scope

We invite all researchers to contribute talks on subjects related to the Types area of interest. These include, but are not limited to: We would like to especially encourage talks proposing new ways of applying type theory.

Invited Speakers

Steve Awodey, School of Mathematics, Institute for Advanced Study, Princeton, U.S.A. & Department of Philosophy, Carnegie Mellon University, Pittsburgh, U.S.A.
Higher Inductive Types in Homotopy Type Theory
Lars Birkedal, Department of Computer Science, Aarhus University, Denmark
Charge! a framework for higher-order separation logic in Coq.
Ulrich Kohlenbach, Department of Mathematics, Technische Universität Darmstadt, Germany
Types in Proof Mining


The contributed talks may be based on newly published papers or work submitted for publication, but also work in progress. There are no formal pre-proceedings, but we will make available the abstract book for the conference.

Post-proceedings are confirmed to appear in LIPIcs (Leibniz International Proceedings in Informatics), Schloss Dagstuhl (the same publisher as for the last TYPES meeting in Bergen in 2011). There is a separate call for papers, and participation in TYPES 2013 is no prerequisite for submission to the post-proceedings.

TYPES 2013 is intended to be a conference in our traditional workshop style. We expect submission of short abstracts that fit on one or two pages, presenting in sufficient detail the content of the talk and its relevance for TYPES, as judged by the program committee.

Submission is exclusively admitted electronically, through the EasyChair system. The submission site is https://www.easychair.org/conferences/?conf=types2013 (closed for submission).

Submissions (co-)authored by program comittee members other than the co-chairs are allowed and will be assessed in the EasyChair system that is perfectly capable of hiding information to program committee members with a conflict of interest.

The Venue

Some snapshots taken on February 17, 2013 with a cheap smartphone camera (click on any picture to get to a page with more information and bigger versions).
Square Boulingrin - stemming from bowling greena view towards Musée des Augustinsthe conference takes place about 100m from the left end of the picture

Some further snapshots taken on April 20 and 21, 2013 with the same camera.
Canal du Midi seen from Pont des Demoisellesat Canal du MidiSquare Boulingrin - stemming from bowling green

Toulouse in the South West of France is the fourth largest city of France and a lively university center with way over 100000 students. Toulouse offers numerous inexpensive accommodations, including student residences.

The participants are on their own in finding accommodation. There is the hotel list of the tourist office and a special list for residences. The résidence de Brienne seems to be the closest to the TYPES venue - just 500m walking distance to the lecture hall. Of course, there are other ways to find hotels in Toulouse. For scientists on short visits to Toulouse (e.g., for juries or project meetings), we typically choose friendly two-star hotels.

The Surroundings

Within a radius of 100km around Toulouse, one can find three "properties" on the World Heritage List of the UNESCO (listing in total close to a thousand).

Coming to Toulouse and other practical information

Strike at Lufthansa on Monday, April 22. List of cancelled flights (this is said to concern every European flight of Lufthansa going through Germany). A sublist I extracted from the cited list of cancelled flights with destination Toulouse

So Toulouse offers all participants a ticket for multiple free rides on the whole public transport system of Toulouse, in particular the airport bus and the subway. You'll get the Pass Transport at the registration desk of PCC on Monday at the IRIT resp. of TYPES on Tuesday at the Manufacture des Tabacs. It is valid until Saturday, April 27.

Getting from the airport to the city center: the preferred method is by the "navette" (the airport bus) that runs every 20 minutes and has several stops in the city center, joining well the two subway lines. The travel time to the first stop (Compans Caffarelli) is less than 15 minutes if the streets are not crowded, but much more at rush hour (bus and taxis run on a separate lane only in part).

Don't go to the wrong site for the conference. On Monday, it is at the IRIT, Université Paul Sabatier (at the subway station with this name of line B - direction Ramonville - directions on campus, also in French), on Tuesday to Friday (until lunch), it is at the Manufacture des Tabacs, see the description and link at the top of this page (the closest subway station is Compans Caffarelli of line B). On Friday afternoon, it is at the IMT, Université Paul Sabatier, only 100m from the IRIT.

A map with the important places for the conference


Complete Program of all of TYPES 2013 (as of April 19). Every TYPES (and PCC) participant will get a printed copy of this program on arrival - together with some extra practical information on the back cover.

Schedule for all TYPES speakers (plain text, with links to provided PDF's of presentation slides)

Book of Abstracts (~7,4MB) with the final versions of the abstracts (version without colored cover pages, still over 7MB). Every registered TYPES participant will get a printed copy of the Book of Abstracts on arrival.

Approximate and preliminary schedule (all at Manufacture des Tabacs unless otherwise stated):

Monday April 22
PCC scientific programme from 10:00 to 17:30 (on the campus of Univ. Paul Sabatier)
17:30 - 18:45 "An introduction to separation logic, and the benefits of going higher-order (a tutorial)", by Lars Birkedal as part of the seminar series 2013 "Logics and analyses for verifying graph transformation" of the IRIT and as preparation for the TYPES meeting
Tuesday April 23
TYPES scientific programme from 10:00 to 12:00, starting with the invited talk by Steve Awodey (no specific programme for PCC)
TYPES and PCC scientific programme in parallel from 12:00 to 18:15
Wednesday April 24
TYPES scientific programme from 9:00 to 18:00, starting with the invited talk by Ulrich Kohlenbach
TYPES business meeting from 18:00 to 19:00
Thursday April 25
TYPES scientific programme from 9:00 to 12:30, starting with the invited talk by Lars Birkedal
after lunch guided visit of old town
3 hours without programme
gala dinner in the old town centre
Friday April 26
TYPES scientific programme from 9:30 to 12:30
Workshop CSPM from 14:30 to 17:45, see below for the scientific programme (on the campus of Univ. Paul Sabatier)


Thanks to our sponsors, notably Université Toulouse 1 Capitole, granting the lecture hall in the city center, and the Region Midi-Pyrénées, the IRIT (Institut de Recherche en Informatique de Toulouse), the federative research structure FREMIT and Université Paul Sabatier (Toulouse 3) with financial support, we are able to keep the participation fee low. Moreover, we operate a scheme of additional fee reduction for master and PhD students.

For the details, see the dedicated page. Early registration ended Wednesday, April 3, 23:59 Paris time.

Satellite Events

Workshop PCC

The twelfth international workshop Proof, Computation, Complexity (PCC 2013) is held on Monday, April 22, and Tuesday, April 23. On Monday, this takes place on the campus of Toulouse Technical University (which is well connected by underground with the city center and the airport bus) and on Tuesday, this is on the site of TYPES 2013. PCC 2013 is organised by

See the dedicated web page of PCC 2013.

A tutorial on separation logic by Lars Birkedal as part of the seminar series 2013 "Logics and analyses for verifying graph transformation" of the IRIT and as preparation for the TYPES meeting

Scheduled for Monday, April 22, 17:30 - 18:45 at the IRIT - the same venue as the workshop PCC on that day. Title: "An introduction to separation logic, and the benefits of going higher-order (a tutorial)". No registration is needed. A web site for the seminar series is in preparation. For the time being, the slides of the presentation are here.

Workshop CSPM "Computer Science, Philosophy, Mathematics"

a workshop on Friday April 26 organized by Sébastien Maronne, Mathematical Institute of Toulouse (IMT) and Sergei Soloviev, Computer Science Institute of Toulouse (IRIT), hosted by the Mathematical Institute, and with financial support by FREMIT.

14:30-16:00 Steve Awodey
Structuralism, Invariance, and Univalence, presentation slides
16:15-17:45 Ulrich Kohlenbach
Proof Theory : From the Foundations of Mathematics to Applications in Core Mathematics, presentation slides (update on May 7, ~2,3MB)

no extra fee for participating in the workshop

The workshop aims to stimulate discussions between computer scientists, philosphers and mathematicians and takes place in the Mathematical Institute, which requires approximately 20 minutes walk + 20 minutes on the subway from the main TYPES conference location.

The dedicated web page for CSPM at the Mathematical Institute was destroyed, there is still (as of July 2014) the announcement of the respective working group (click on the entry that is to be found at the bottom of the page).


General Chair: Ralph Matthes

Program Committee

Local Organization Committee

Steering Committee of the TYPES Conference Series (before the election of new members during the business meeting on April 24, 2013)

Page maintained by:

Ralph Matthes

Last modified (date in French): ven. juil. 25 14:30:00 CEST 2014