The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

                        Types Meeting 2014
                       Paris, 12-15 May 2014

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

                     2nd 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 and 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, 39
contributed talks have been 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 only until ** April 19 **.