A Proposal for Broad Spectrum Proof Certificates

DOI10.1007/978-3-642-25379-9_6zbMath1349.03027OpenAlexW131041899MaRDI QIDQ3100201

Dale A. Miller

Publication date: 22 November 2011

Published in: Certified Programs and Proofs (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-25379-9_6

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Structure of proofs (03F07)

Related Items

Proof checking and logic programming, Proof certificates for equality reasoning, The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem, Unnamed Item

Uses Software

• Automath
• Tac
• Teyjus

Cites Work

• Unnamed Item
• Kripke semantics and proof systems for combining intuitionistic logic and classical logic
• Focusing and polarization in linear, intuitionistic, and classical logics
• Theorem proving modulo
• Autarkic computations in formal proofs
• Uniform proofs as a foundation for logic programming
• Incorporating Tables into Proofs
• Theorem Proving via General Matings
• Logic Programming with Focusing Proofs in Linear Logic
• Every Prime Has a Succinct Certificate
• Polymorphic lemmas and definitions in $\lambda$Prolog and Twelf
• Focused Inductive Theorem Proving
• Least and Greatest Fixed Points in Linear Logic