A proposal for broad spectrum proof certificates

DOI10.1007/978-3-642-25379-9_6zbMATH Open1349.03027OpenAlexW131041899MaRDI QIDQ3100201FDOQ3100201

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

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

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)

Cites Work

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

Cited In (6)

• Proof checking and logic programming
• Title not available (Why is that?)
• Title not available (Why is that?)
• On mixed connectivity certificates
• The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem
• Proof certificates for equality reasoning

Uses Software

• Automath
• Tac
• Teyjus

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)