Proof-assistants using dependent type systems
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].
- scientific article; zbMATH DE number 6296049
- An introduction to programming and proving with dependent types in Coq
- Type theories from Barendregt's cube for theorem provers
- Crafting a Proof Assistant
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Proof assistants: history, ideas and future
- N. G. de Bruijn (1918--2012) and his road to Automath, the earliest proof checker
- Classical \(F_{\omega}\), orthogonality and symmetric candidates
- Fiat: deductive synthesis of abstract data types in a proof assistant
- A framework for defining logical frameworks
- Inductive and coinductive components of corecursive functions in Coq
- Dependently Typed Programming Based on Automated Theorem Proving
- An introduction to programming and proving with dependent types in Coq
- A module calculus for Pure Type Systems
- Crafting a Proof Assistant
- Local Theory Specifications in Isabelle/Isar
- scientific article; zbMATH DE number 683355 (Why is no real title available?)
- Cut Elimination in a Class of Sequent Calculi for Pure Type Systems
- Characteristics of de Bruijn’s early proof checker Automath
- Introduction to Type Theory
- Type theories from Barendregt's cube for theorem provers
- The challenge of computer mathematics
- Mtac: a monad for typed tactic programming in Coq
- scientific article; zbMATH DE number 6296049 (Why is no real title available?)
- Machine-checked security proofs of cryptographic signature schemes
- Primitive Floats in Coq
- Proof-term synthesis on dependent-type systems via explicit substitutions
- Electronic communication of mathematics and the interaction of computer algebra systems and proof assistants
- scientific article; zbMATH DE number 7756106 (Why is no real title available?)
- Formalizing two-level type theory with cofibrant exo-nat
- Pure type systems without explicit contexts
- Some probabilistic riddles and some logical solutions
- Computer theorem proving in mathematics
- Obituary: Nicolaas Govert de Bruijn (1918--2012). Mathematician, computer scientist, logician
- N. G. de Bruijn's contribution to the formalization of mathematics
This page was built for publication: Proof-assistants using dependent type systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2751370)
