Visitor

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.

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.

Attachment	Size
FromTypesToTT-Kanazawa160307.pdf	137.54 KB