TYPES Meeting 2014
Paris, 12-15 May 2014

http://www.pps.univ-paris-diderot.fr/types2014/

FIRST CALL FOR CONTRIBUTIONS

The 20th Conference "Types for Proofs and Programs" will take place in
Paris, France, from 12 to 15 May 2014.

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:

* Thierry Coquand
* Xavier Leroy
* Andy Pitts

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;
* Homotopy type theory;
* 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, 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.

TYPES has post-proceedings which will be announced in a separate call
for papers. Participation in TYPES 2014 is no prerequisite for
submission to the post-proceedings.

TYPES 2014 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 for a contributed talk consists in a short LaTeX abstract
in EasyChair style that fits on one or two pages to be included in the
abstract book. The submission site is
https://www.easychair.org/conferences/?conf=types2014 .
Please announce your intention to submit an abstract by first
submitting a title one week in advance.

Dates:

* title: Friday February 21 (midnight GMT)
* submission of short abstracts: Friday February 28 (midnight GMT)
* notification of acceptance: Monday March 17
* final version of short abstracts: Friday April 11

The conference will be held at the Institut Henri Poincaré in the 5th
district of Paris. It will happen on week 4 of the special trimester
on Semantics of proofs and certified mathematics (see
http://ihp2014.pps.univ-paris-diderot.fr).

Satellite event: the 13th international workshop Proof, Computation,
Complexity (PCC 2014) will be held on May 15th and 16th.

Program Committee:

* Andreas Abel, Chalmers University of Technology and Gothenburg University
* Andrej Bauer, Fakulteta za matematiko in fiziko, Ljubljana
* Małgorzata Biernacka, University of Wroclaw
* Lars Birkedal, Aarhus University
* Paul Blain Levy, University of Birmingham
* Herman Geuvers, Radboud University and Eindhoven University of Technology
* Hugo Herbelin, Inria Paris-Rocquencourt (co-chair)
* Pierre Letouzey, University Paris-Diderot (co-chair)
* Ralph Matthes, IRIT, CNRS and University of Toulouse
* Conor McBride, University of Strathclyde
* Luís Pinto, University of Minho, Braga
* Claudio Sacerdoti, University of Bologna
* Aleksy Schubert, University of Warsaw
* Matthieu Sozeau, Inria Paris-Rocquencourt (co-chair)
* Thomas Streicher, TU Darmstadt