Proof by computation in the Coq system
type: Item
instance of: scholarly article
title: Proof by computation in the Coq system
zbMATH Open document ID: 0984.68137
DOI: 10.1016/S0304-3975(00)00354-6
author: Martijn Oostdijk
author: Herman Geuvers
published in: Theoretical Computer Science
publication date: 2002-03-03T00:00:00Z
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 1715300
zbMATH Keywords: automated proof development system
zbMATH Keywords: type theory
describes a project that uses: Coq
describes a project that uses: LEGO
describes a project that uses: Automath
MaRDI profile type: MaRDI publication profile
cites work: Q4023825
cites work: Autarkic computations in formal proofs
cites work: A two-level approach towards lean proof-checking
cites work: Q4393449
cites work: Q3789525
Recommended article: A mechanized proof system of the third generation calculus in Coq
Recommended article: Q5472879
Recommended article: A Proof System for MSVL Programs in Coq
Recommended article: Formal proof of a machine closed theorem in Coq
Recommended article: Soundness and completeness proofs by coinductive methods
Recommended article: Proof reflection in Coq
Recommended article: Logical Approaches to Computational Barriers
Recommended article: Q3086937
Recommended article: Q4282573
Recommended article: Proof systems for Moss' coalgebraic logic
description: scientific article; zbMATH DE number 1715300