[Agda] Types Meeting 2013 in Toulouse, 22 - 26 April: 2nd call for participation

Ralph Matthes Ralph.Matthes at irit.fr
Fri Mar 29 17:04:05 CET 2013

                        Types Meeting 2013
                    Toulouse, 22-26 April 2013



[new: tutorial by Lars Birkedal on April 22, abstracts of contributed
talks are available, a remark that there are several payment options, 
titles and abstracts of talks by Steve Awodey and Ulrich Kohlenbach in
the CSPM workshop on April 26 are available, and also a dedicated CSPM
web page]

The 19th Conference "Types for Proofs and Programs" will take place in
Toulouse, France, from 22 to 26 April 2013 - including the pre-conference 
workshop PCC on April 22 and 23, a tutorial in the late afternoon of 
April 22 and the post-conference workshop CSPM in the afternoon of 
April 26. The scientific programme of the main event is from the morning 
of April 23 (Tuesday) until lunch time on April 26. For an overview of 
the whole planning, see the web site.

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 (abstracts are available on the web site):

* 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, 
  "Charge! a framework for higher-order separation logic in Coq."

* Ulrich Kohlenbach, Department of Mathematics, TU Darmstadt, Germany
  "Types in Proof Mining"

TYPES 2013 is intended to be a conference in our traditional workshop
style. The contributed talks were selected by the program committee on the
basis of abstracts of up to two pages (in EasyChair LaTeX style).

34 contributed talks were selected by the program committee, see their list
together with short (text-only) abstracts via the web site or directly at 

(To the authors: the deadline for the final version of LaTeX sources for 
inclusion of the abstracts into the abstract book is Monday, April 1st. 
The abstracts will then be made available on the web site.)

Post-proceedings of TYPES 2013 are confirmed to appear in LIPIcs (Leibniz
International Proceedings in Informatics), Schloss Dagstuhl, see
(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.

The conference itself: Tuesday to Friday, April 23-26 (end of scientific
programme on Friday planned for 12:30)

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 of the main event.

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. 

*** Early registration will be until      ***
*** Wednesday, April 3, 23:59 Paris time. ***

Access to the online registration system is through
where the fees can be studied offline (several payment options are 
available, in particular safe payment by credit card).

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.

The program committee of PCC 2013 selected 12 contributed talks on the basis 
of short abstracts.

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

A tutorial on separation logic by Lars Birkedal in the late afternoon 
of April 22: "An introduction to separation logic, and the benefits 
of going higher-order", within the seminar series 2013 "Logics and analyses 
for verifying graph transformation" of the IRIT.


Workshop CSPM "Computer Science, Philosophy, Mathematics", Friday, April 26,

a workshop hosted by the Mathematical Institute, and with financial support 
by FREMIT, with invited contributions as follows:
14:30-16:00 Steve Awodey: "Structuralism, Invariance, and Univalence"
16:15-17:45 Ulrich Kohlenbach: "Proof Theory : From the Foundations of 
            Mathematics to Applications in Core Mathematics" 

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.

There will be no extra fee for participating in the workshop CSPM.

For more details (e.g., abstracts and registration information for 
non-TYPES-participants), see the dedicated web page at

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

More information about the Agda mailing list