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

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

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

• scientific article; zbMATH DE number 3859117 (Why is no real title available?)
• Autarkic computations in formal proofs
• Every Prime Has a Succinct Certificate
• Focused Inductive Theorem Proving
• Focusing and polarization in linear, intuitionistic, and classical logics
• 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 via General Matings
• Theorem proving modulo
• Uniform proofs as a foundation for logic programming

Cited in

(11)

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

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)