Types Meeting 2013 Toulouse, 22-26 April 2013 http://www.irit.fr/TYPES2013/ SECOND CALL FOR PARTICIPATION [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, Denmark "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 http://www.irit.fr/TYPES2013/acceptedWithAbstracts.html (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 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. 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 http://www.irit.fr/TYPES2013/Registration.html where the fees can be studied offline (several payment options are available, in particular safe payment by credit card). SATELLITE EVENTS ----------------------------------------------------------------------- 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 http://www.math.univ-toulouse.fr/spip.php?article346 ----------------------------------------------------------------------- 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 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]