Proof assistants: history, ideas and future

DOI10.1007/s12046-009-0001-5zbMath1192.68629OpenAlexW2098909266MaRDI QIDQ1040001

Herman Geuvers

Publication date: 23 November 2009

Published in: Sādhanā (Search for Journal in Brave)

Full work available at URL: https://www.ias.ac.in/describe/article/sadh/034/01/0003-0025

zbMATH Keywords

verificationlogicproof assistantformalized mathematicssoftware correctness

Mathematics Subject Classification ID

Related Items

Computational logic: its origins and applications, Crystal: Integrating structured queries into a tactic language, Characteristics of de Bruijn’s early proof checker Automath, Adding Negation to Lambda Mu, Comprehending Isabelle/HOL’s Consistency, Programming and verifying a declarative first-order prover in Isabelle/HOL, The natural algorithmic approach of mixed trigonometric-polynomial problems, Social processes, program verification and all that

Uses Software

• ACL2
• Coq
• Isabelle
• ML
• Isar
• HOL
• ActiveMath
• Nuprl
• C-CoRN
• Automath
• OMDoc
• NQTHM
• LCF
• ALF
• LEGO
• SAD
• PoplMark
• Flyspeck
• kepler98
• Whelp

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
• A type-theoretical alternative to ISWIM, CUCH, OWHY
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• A proof of the Kepler conjecture
• Structural Analysis of Narratives with the Coq Proof Assistant
• The Isabelle Framework
• A framework for defining logics
• Mathematical Knowledge Management
• Cooperative Repositories for Formal Proofs
• Theorem Proving in Higher Order Logics
• Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors
• On Correctness of Mathematical Texts from a Logical and Practical Point of View
• Mathematical Knowledge Management