Efficient reasoning about executable specifications in Coq
From MaRDI portal
(Redirected from Efficient reasoning about executable specifications in Coq)
Recommendations
- Synthesis of ML programs in the system Coq
- Producing certified functional code from inductive specifications
- Axiomatisations, proofs, and formal specifications of algorithms: Commented case studies in the coq proof assistant
- Efficient execution in an automated reasoning environment
- A formal executable semantics of the JavaCard platform
Cited in
(15)- Mechanical synthesis of sorting algorithms for binary trees by logic and combinatorial techniques
- Deciding Kleene algebra terms equivalence in Coq
- Deciding regular expressions (in-)equivalence in Coq
- A certified reduction strategy for homological image processing
- Analysing and Compiling Coroutines with Abstract Conjunctive Partial Deduction
- CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
- Using Structural Recursion for Corecursion
- Mechanically certifying formula-based Noetherian induction reasoning
- LF+ in Coq for "fast and loose" reasoning
- Handcrafted inversions made operational on operational semantics
- Efficient execution in an automated reasoning environment
- Extending Coq with Imperative Features and Its Application to SAT Verification
- The world's shortest correct exact real arithmetic program?
- Tool-assisted specification and verification of typed low-level languages
- Tilting at windmills with Coq: Formal verification of a compilation algorithm for parallel moves
This page was built for publication: Efficient reasoning about executable specifications in Coq
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4484330)
