Dr. Gilles Barthe

TYPE-THEORETIC FOUNDATIONS OF PROOF-ASSISTANTS

Abstract

Proof-development systems are extensively used in the formalization of programming languages, reactive and embedded systems, communication and cryptographic protocols... Many systems, including Coq and PVS, rely on powerful type systems.

The purpose of the course is to introduce the type-theoretic machinery underlying those systems. In the first part of the course, we shall introduce Pure Type Systems, a generic framework for defining many typed lambda-calculi and logics that appear in the literature. In particular, we shall focus on the Calculus of Constructions, that forms the basis of the proof-development system Coq, and on the lambda-cube, which provides a fine grain analysis of the Calculus of Constructions. The second part of the course shall be devoted to inductive definitions, and their use for representing data structures and mathematical theories.

Contact information:
Projet Oasis, INRIA Sophia-Antipolis
2004 Route des Lucioles
BP 93, 06902 Sophia Antipolis Cedex
France
Tél: (33) 4 92 38 79 38
Fax: (33) 4 92 38 79 71

EMAIL: Gilles.Barthe@sophia.inria.fr
WWW: http://www-sop.inria.fr/oasis/personnel/Gilles.Barthe/