From Types to Type Theory to Proofs of Programs


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.

2016/03/07 (Mon) 14:00 to 15:30
Seminar room (IS 7F)
Logic Unit
Research Center for Software Verification
Title: From Types to Type Theory to Proofs of Programs

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.

PDF icon FromTypesToTT-Kanazawa160307.pdf137.54 KB
Mizuhito Ogawa <>