[TYPES/announce] Types Meeting 2013 in Toulouse, 23 - 26 April: last call for contributions

[Ralph Matthes]

                        Types Meeting 2013
                    Toulouse, 23-26 April 2013

                   http://www.irit.fr/TYPES2013/

                    LAST CALL FOR CONTRIBUTIONS

The 19th Conference "Types for Proofs and Programs" will take place in
Toulouse, France, from 23 to 26 April 2013.

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.

Invited speakers:

* Steve Awodey, 
  School of Mathematics, Institute for Advanced Study, Princeton, U.S.A.
  & Department of Philosophy, Carnegie Mellon University, 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, TU Darmstadt, Germany
  "Types in Proof Mining"

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.

The 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.

Meanwhile, post-proceedings are confirmed to appear in LIPIcs (Leibniz
International Proceedings in Informatics), Schloss Dagstuhl, see
http://www.dagstuhl.de/en/publications/lipics 
(the same publisher as for the last TYPES meeting in Bergen in 2011)
There will be 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

Deadline for proposing a contributed talk: Monday, February 25
This means registering a submission to the EasyChair system, including
a short text-only abstract, and submitting the PDF file of an abstract 
typeset in LaTeX that fits on one or two pages, conforming to the 
EasyChair LaTeX class - for technical details, see the web page.
(In the first call for papers, there was a second, earlier deadline
for registering the submission 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 conference itself: Tuesday to Friday, April 23-26

The venue: 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. On the web site, there are links to
hotels and residences - even one of the latter only 500m walking 
distance from the lecture hall.

Thanks to our sponsors, notably Université Toulouse 1 Capitole,
granting the lecture hall in the city center, and IRIT (Institut de
Recherche en Informatique de Toulouse), the federative research 
structure FREMIT and Université Paul Sabatier (Toulouse 3) with 
financial support (other sources pending), 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 planned 
registration fees, please see the web site (a dedicated page 
accessible from the site).

Early registration (not yet open) will be until April 2.

-----------------------------------------------------------------------
Satellite event: On Monday, April 22, the twelfth international
workshop Proof, Computation, Complexity (PCC 2013) will be held 
on the campus of Toulouse Technical University.

Abstract submission deadline: February 25
Notification of acceptance: March 8

For the details, see http://www.irit.fr/TYPES2013/PCC2013/
-----------------------------------------------------------------------


Program Committee TYPES 2013

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, Tallinn Technical University, Estonia