TYPES Meeting 2013 (April 22-26, 2013)

"Executive summary" of main web page

19TH MEETING TYPES FOR PROOFS AND PROGRAMS (TYPES 2013)

Call for Participation
April 22-26, Toulouse, France
https://www.irit.fr/TYPES2013/

AIMS

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 (Institute for Advanced Study, Princeton & Carnegie Mellon University, Pittsburgh)

"Higher Inductive Types in Homotopy Type Theory"

Lars Birkedal (Aarhus University)

"Charge! a framework for higher-order separation logic in Coq."

Ulrich Kohlenbach (Technische Universitaet Darmstadt)

"Types in Proof Mining"

34 contributed talks were selected by the program committee.

IMPORTANT DATES

• main conference: morning of April 23 to midday of April 26
• early registration ended Wednesday, April 3, 23:59 Paris time

Access to the online registration system (still open) is through https://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

• Twelfth international workshop Proof, Computation, Complexity (PCC 2013) with 12 selected contributed talks on April 22 and 23
• 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"
• Workshop CSPM "Computer Science, Philosophy, Mathematics" in the afternoon of April 26, 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"

All the details are accessible through the main web site of TYPES 2013.

Last modified (date in French): jeu. avril 4 19:39:51 CEST 2013