From Types to Type Theory to Proofs of Programs
|Jean-Pierre Jouannaud graduated from Ecole Polytechnique de Paris and
obtained his doctorate from University Paris 6 in 1978. He was then a
professor successively at the universities of Nancy, then Paris-Sud,
and finally at Ecole Polytechnique, in France, as well as an invited
professor at a number of places, including Stanford Research Institute
and Stanford University in US (2 years), the Polytechnicum University
of Catalugna in Spain (1 year), Keio University in Tokyo (6 months),
Japan, National Taiwan University in Taipei (4 months), Taiwan, and
Tsinghua University in Beijing, China (5 years).
He is now Professor emeritus at University Paris-Sud and Ecole
Polytechnique in France.
Since the early 80’s, his research interests have been focusing on the interplay between deduction rules, rewrite rules, decision procedures, programming languages and type theory, in the development of programming languages (OBJ2), Rewriting tools (REVExxx), proof assistants (Coq and Dedukti), and in the application of these tools to the formal proof of systems.
During his career, he had a leading role in the creation of two conferences in areas at the heart to his interests: Rewriting Techniques and Applications (RTA, which merged with TLCA last year, becaming now Formal Structures in Computation and Deduction), and Certified Programs and Proofs (CPP). He served on a number of editorial boards and steering/scientific committees, including those of Information and Computation, Journal of Symbolic Computation, RTA, CSL, LICS, CPP, the Max-Planck Institute at Saarbrücken, and Academia Sinica at Taipei —his only duty left.
Abstract: We shall describe the long path which started from programming languages and utimately lead to proof assistants via the programming language ML and the type theory known as Martin L\"of's type theory. The lecture will try to make sense of various notions, such as the Curry-Howard correspondance, the tension between intentionality and extensionality in Martin L\"of's type theory, and the use of proof assistants to prove properties on prgrams written, say, in C.
Mizuhito Ogawa <email@example.com>