Axiomatisations, proofs, and formal specifications of algorithms: Commented case studies in the coq proof assistant
From MaRDI portal
Recommendations
- Computer-Assisted Proofs in Analysis and Programming in Logic: A case Study
- Formalizing in Coq Hidden Algebras to Specify Symbolic Computation Systems
- Formalizing Stålmarck's algorithm in Coq
- Proof by computation in the Coq system
- Coinduction: automata, formal proof, companions (invited paper)
- Proof systems for structured algebraic specifications: An overview
- Formalizing implicative algebras in Coq
- Observational equivalence and program extraction in the Coq proof assistant
- Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant
- Programs, proofs and parametrized specifications
Cited in
(14)- Synthesis of ML programs in the system Coq
- A Coq formalisation of SQL's execution engines
- Concrete semantics with Coq and CoqHammer
- Formalizing Stålmarck's algorithm in Coq
- HOCore in Coq
- Program calculation in Coq
- A Short Presentation of Coq
- Canonical Big Operators
- Efficient reasoning about executable specifications in Coq
- Certifying the fast Fourier transform with Coq
- Programming Languages and Systems
- Using Coq to Prove Properties of the Cache Level of a Functional Video-on-Demand Server
- Coq and hardware verification: a case study
- High-level modelling for typed functional programming
This page was built for publication: Axiomatisations, proofs, and formal specifications of algorithms: Commented case studies in the coq proof assistant
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4357063)
