Proof assistants: history, ideas and future
type: Item
instance of: scholarly article
title: Proof assistants: history, ideas and future
zbMATH Open document ID: 1192.68629
published in: Sādhanā
publication date: 2009-11-23T00:00:00Z
full work available at URL: https://www.ias.ac.in/describe/article/sadh/034/01/0003-0025
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 5637279
zbMATH Keywords: proof assistant
zbMATH Keywords: verification
zbMATH Keywords: logic
zbMATH Keywords: software correctness
zbMATH Keywords: formalized mathematics
author: Herman Geuvers
describes a project that uses: ActiveMath
describes a project that uses: Coq
describes a project that uses: ML
describes a project that uses: Isar
describes a project that uses: Automath
describes a project that uses: OMDoc
describes a project that uses: ACL2
describes a project that uses: HOL
describes a project that uses: Nuprl
describes a project that uses: NQTHM
describes a project that uses: kepler98
describes a project that uses: Isabelle
describes a project that uses: C-CoRN
describes a project that uses: LEGO
describes a project that uses: LCF
describes a project that uses: ALF
describes a project that uses: SAD
describes a project that uses: PoplMark
describes a project that uses: Flyspeck
describes a project that uses: Whelp
MaRDI profile type: Publication
OpenAlex ID: W2098909266
cites work: Q4817211
cites work: Mathematical Knowledge Management
cites work: Theorem Proving in Higher Order Logics
cites work: Q4664918
cites work: Proof-assistants using dependent type systems
cites work: Q4040283
cites work: Cooperative Repositories for Formal Proofs
cites work: Structural Analysis of Narratives with the Coq Proof Assistant
cites work: Q5815602
cites work: Q5287513
cites work: A proof of the Kepler conjecture
cites work: A framework for defining logics
cites work: Q2754046
cites work: Q4471938
cites work: Q5519616
cites work: Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
cites work: Q3999860
cites work: A type-theoretical alternative to ISWIM, CUCH, OWHY
cites work: On Correctness of Mathematical Texts from a Logical and Practical Point of View
cites work: Authoring Verified Documents by Interactive Proof Construction and Verification in Text-Editors
cites work: The Isabelle Framework
cites work: Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics
DOI: 10.1007/S12046-009-0001-5
description: scientific article; zbMATH DE number 5637279