Proof-assistants using dependent type systems (Q2751370)

This chapter discusses the underlying ideas of the development of proof-assistants based on type theory. Proof checking consists of the automated verification of mathematical theories by a formalization of its primitive notions; once a theory is formalized, its correctness is verified by a small program, the proof-checker, but in order to make the formalization process feasible, an interactive proof-development system is needed. A proof assistant is the combination of a proof-development system and a proof checker. The chapter is structured in two main sections: the first one deals with the type-theoretic notions for proof checking, introduces the propositions-as-types paradigm and surveys the treatment of functions, reduction, conversion, computation and equality. The next section presents different type systems for proof checking, most of the commonly used have inductive types, but there are still many other parameters to consider. Later, the chapter presents a concrete proof-assistant at work. Specifically, a {\text{Coq}} session is presented in which a theory is developed for the toy-statement that every natural number has a prime divisor. The final section presents a comparison and discussion of advantages and disadvantages of several proof-assistants.NEWLINENEWLINEFor the entire collection see [Zbl 0964.00020].