An architecture for interactive program provers
From MaRDI portal
Recommendations
- Effective interactive proofs for higher-order imperative programs
- A Framework for Interactive Proof
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Interactive theorem proving from the perspective of Isabelle/Isar
- Towards Ludics Programming: Interactive Proof Search
- Interactive realizers: a new approach to program extraction from nonconstructive proofs
- A survey of interactive theorem proving
- Interactive and probabilistic proof-checking
- A logic of interactive proofs
- A logic of interactive proofs
Cited in
(14)- Integration of verification methods for program systems
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- Weakest pre-condition reasoning for Java programs with JML annotations
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- scientific article; zbMATH DE number 1706329 (Why is no real title available?)
- Tool support for proof engineering
- scientific article; zbMATH DE number 140007 (Why is no real title available?)
- scientific article; zbMATH DE number 2086601 (Why is no real title available?)
- An Interactive Driver for Goal-directed Proof Strategies
- scientific article; zbMATH DE number 3894447 (Why is no real title available?)
- The HOL-CSP Refinement Toolkit
- HOL-CSP Version 2.0
- A Sound Type System for Physical Quantities, Units, and Measurements
- Jive Data and Store Model
This page was built for publication: An architecture for interactive program provers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2729071)
