TYPES Meeting 2013 (April 22-26, 2013)
Post-conference news: post-proceedings appeared as vol.26 of LIPIcs on July 25, 2014
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
- Workshop PCC 2013 on April 22 (Monday) and April 23 see below.
- Workshop "Computer Science, Philosophy, Mathematics" with Steve Awodey and Ulrich Kohlenbach on April 26 (Friday), see below.
- Tutorial on separation logic by Lars Birkedal on Monday April 22, see below.
A marvellous picture of the town hall of Toulouse (6,6 MB, © Ville de Toulouse):
© 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
About TYPES
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:
- 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;
- Formalizing mathematics using type theory.
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
Submission
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.
-
Deadline for proposing a contributed talk: Monday, February 25 (later than required in the first call for papers sent in December 2012: there is now only a single deadline before acceptance).
This means registering a submission to the EasyChair system, including
a short text-only abstract. And also the PDF file of an abstract typeset in LaTeX that fits on one or two pages has to be submitted by that date, conforming to the EasyChair LaTeX class. The linked ZIP file contains besides easychair.cls a style guide. Under the Ubuntu system, it may be necessary to install the extra package texlive-latex3 (this contains the
so-called MH bundle, including empheq.sty), with LaTeX packages preloaded by the EasyChair class. For your convenience, you find here a LaTeX model of a TYPES'13 abstract - which shows the crucial LaTeX elements that are specific to EasyChair.
-
Notification of acceptance: Friday, March 8.
-
Deadline for final version of LaTeX sources for inclusion of the abstract into the abstract book: Monday, April 1st.
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).
Some further snapshots taken on April 20 and 21, 2013 with the same camera.
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).
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
Programme
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)
Registration
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.
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
- Birgit Elbl, UniBw München, Neubiberg, Germany
- Reinhard Kahle, Universidade Nova de Lisboa, Portugal
- Lars Kristiansen, University of Oslo, Norway
- Ralph Matthes, IRIT, CNRS and Univ. de Toulouse, France
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.
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).
Organizers
General Chair: Ralph Matthes
Program Committee
- José Espírito Santo, University of Minho, Braga, Portugal
- Herman Geuvers, Radboud University Nijmegen, Netherlands
- Silvia Ghilezan, University of Novi Sad, Serbia
- Hugo Herbelin, PPS, INRIA Rocquencourt-Paris, France
- Martin Hofmann, Ludwig-Maximilians-Universität München, Germany
- Zhaohui Luo, Royal Holloway, University of London, UK
- Ralph Matthes, IRIT, CNRS and Univ. de Toulouse, France (co-chair)
- Marino Miculan, University of Udine, Italy
- Bengt Nordström, Chalmers University of Technology, Göteborg, Sweden
- Erik Palmgren, Stockholm University, Sweden
- Andy Pitts, University of Cambridge, UK
- Sergei Soloviev, IRIT, Univ. de Toulouse, France (co-chair)
- Paweł Urzyczyn, University of Warsaw, Poland
- Tarmo Uustalu, Institute of Cybernetics, Tallinn Technical University, Estonia
Local Organization Committee
Steering Committee of the TYPES Conference Series (before the election of new members during the business meeting on April 24, 2013)
- Robert Atkey, University of Strathclyde, UK
- Marc Bezem, Bergen University, Norway
- Hugo Herbelin, also PC member
- Andrew Polonsky, Institute for Advanced Study, Princeton, USA
- Aleksy Schubert, Warsaw University, Poland
- Tarmo Uustalu, also PC member
Page maintained by:
Ralph Matthes https://www.irit.fr/~Ralph.Matthes/
Last modified (date in French): ven. juil. 25 14:30:00 CEST 2014
