PRL Seminars

In this talk, I discuss engineering aspects of the design of mechanized proof assistants and environments, issues that are not usually given attention.

I first evaluate three current systems, Nuprl 4, HOL 88 (Higher-Order Logic) and Coq V5.8 (the Calculus of Constructions) and, from an analysis of their strong and weak points, arrive at a design for a new system, Coq V5.10, which I have implemented at INRIA-Rocquencourt. This system is currently being developed and distributed within the European Union, and is used by at least two industrial partners for work in protocol verification, among other things.