The Engineering Aspects of Proof-Environment Design

by Chetan Murthy
1994-1995

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.

The Engineering Aspects of Proof-Environment Design

by Chetan Murthy 1994-1995

by Chetan Murthy
1994-1995