The Engineering Aspects of Proof-Environment Design
by Chetan Murthy
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.