[Caml-list] Types Meeting 2014 in Paris, 12 - 15 May: call for participation

[Caml-list] Types Meeting 2014 in Paris, 12 - 15 May: call for participation

[Hugo Herbelin]

                        Types Meeting 2014
                       Paris, 12-15 May 2014

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

                       CALL FOR PARTICIPATION

The 20th Conference "Types for Proofs and Programs" will take place at
the Institut Henri Poincaré (IHP) in Paris, France, from 12 to 15 May
2014, continued by the post-conference workshop "Proof, Computation,
Complexity" overlapping TYPES on May 15 afternoon and on May 16. Types
is this year an event associated to the special IHP trimester on
Semantics of proofs and certified mathematics
(https://ihp2014.pps.univ-paris-diderot.fr).

Invited speakers are

* Thierry Coquand, University of Gothenburg, Sweden
  A cubical set model of type theory

* Xavier Leroy, INRIA Paris-Rocquencourt, France
  Formal verification of a static analyzer: abstract interpretation in type theory

* Andy Pitts, University of Cambridge, UK
  Nominal sets in dependent type theory

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. It works as
a conference in our traditional workshop style and, this year, close
to 40 contributed talks are in the process of being selected by the
program committee on the basis of abstracts of up to two pages
(see http://www.pps.univ-paris-diderot.fr/types2014/Program).

Registration is open, with early rate until April 19.