A proposal for broad spectrum proof certificates

DOI10.1007/978-3-642-25379-9_6MaRDI QIDQ3100201zbMATH OpenOpenAlexFDO

Authors Dale 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

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

Recommendations

• A semantic framework for proof evidence
• Foundational proof certificates in first-order logic
• The focused calculus of structures
• Proof certificates for equality reasoning
• The Proof Certifier Checkers

Cites work

• Autarkic computations in formal proofs
• Every Prime Has a Succinct Certificate
• Focused Inductive Theorem Proving
• Focusing and polarization in linear, intuitionistic, and classical logics
• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• Incorporating Tables into Proofs
• Kripke semantics and proof systems for combining intuitionistic logic and classical logic
• Logic Programming with Focusing Proofs in Linear Logic
• Polymorphic lemmas and definitions in \lambdaProlog and Twelf
• Theorem proving modulo
• Theorem Proving via General Matings
• Uniform proofs as a foundation for logic programming

Cited in

(11)

• Proof certificates in PVS
• A semantic framework for proof evidence
• Proof certificates for equality reasoning
• Proof search and certificates for evidential transactions
• Proof checking and logic programming
• Foundational proof certificates in first-order logic
• scientific article; zbMATH DE number 7204450 (Why is no real title available?)
• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
• A general proof certification framework for modal logic
• scientific article; zbMATH DE number 6741937 (Why is no real title available?)
• On mixed connectivity certificates

Describes a project that uses

Uses Software

• Teyjus
• Tac
• Automath

This page was built for publication: A proposal for broad spectrum proof certificates

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3100201)