Formal Reasoning Using Distributed Assertions

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

Authors: Kaustuv Chaudhuri, Dale Miller 

Publication date: 3 May 2024

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

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Cites Work

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

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)