Formal Reasoning Using Distributed Assertions

DOI10.1007/978-3-031-43369-6_10MaRDI QIDQ6496629FDO

Authors Kaustuv Chaudhuri, Dale Miller

Publication date 3 May 2024

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Recommendations

• A semantic framework for proof evidence
• Information-intensive proof technology
• A general proof certification framework for modal logic
• The Proof Certifier Checkers
• Formal Verification of Distributed Algorithms

Cites work

• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• A case study in programming coinductive proofs: Howe's method
• A proof theory for generic judgments
• A semantic framework for proof evidence
• Abella: a system for reasoning about relational specifications
• Autarkic computations in formal proofs
• Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
• Dafny: an automatic program verifier for functional correctness
• How to identify, translate and combine logics?
• Mathematical Knowledge Management
• Mathematical knowledge management in HELM
• Nominal abstraction
• Nominal logic, a first order theory of names and binding
• POPLMark reloaded: mechanizing proofs by logical relations
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• The \textsc{MetaCoq} project
• The challenge of computer mathematics
• The future of logic: foundation-independence
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Theorem Proving in Higher Order Logics
• Tools and Algorithms for the Construction and Analysis of Systems
• Variations in Access Control Logic
• Why3 -- where programs meet provers

This page was built for publication: Formal Reasoning Using Distributed Assertions

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