Formal Reasoning Using Distributed Assertions

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

Unnamed Author, Kaustuv Chaudhuri, Dale A. Miller

Publication date: 3 May 2024

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Cites Work

• The future of logic: foundation-independence
• The next 700 challenge problems for reasoning with higher-order abstract syntax representations. II: A survey
• Nominal abstraction
• Autarkic computations in formal proofs
• A semantic framework for proof evidence
• Mathematical knowledge management in HELM
• Nominal logic, a first order theory of names and binding
• The \textsc{MetaCoq} project
• The TPTP problem library and associated infrastructure and associated infrastructure. The FOF and CNF parts, v3.5.0
• Dafny: An Automatic Program Verifier for Functional Correctness
• A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
• How to identify, translate and combine logics?
• Variations in Access Control Logic
• Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions
• POPLMark reloaded: Mechanizing proofs by logical relations
• Abella: A System for Reasoning about Relational Specifications
• A case study in programming coinductive proofs: Howe’s method
• A proof theory for generic judgments
• The challenge of computer mathematics
• Mathematical Knowledge Management
• Why3 — Where Programs Meet Provers
• Theorem Proving in Higher Order Logics
• Tools and Algorithms for the Construction and Analysis of Systems

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