The following pages link to Coq (Q12929):
Displaying 50 items.
- A formally verified cut-elimination procedure for linear nested sequents for tense logic (Q2142082) (← links)
- Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq (Q2142084) (← links)
- Exploiting verified neural networks via floating point numerical error (Q2145326) (← links)
- Automated verification of the parallel Bellman-Ford algorithm (Q2145339) (← links)
- A formal model of Algorand smart contracts (Q2145369) (← links)
- Abstraction and subsumption in modular verification of C programs (Q2147702) (← links)
- Verifying the conversion into CNF in dafny (Q2148786) (← links)
- Axiomatic reals and certified efficient exact real computation (Q2148797) (← links)
- Parametric Church's thesis: synthetic computability without choice (Q2151397) (← links)
- Constructive and mechanised meta-theory of intuitionistic epistemic logic (Q2151399) (← links)
- Formal verification of cP systems using Coq (Q2152300) (← links)
- Generalized arrays for Stainless frames (Q2152661) (← links)
- Program logic for higher-order probabilistic programs in Isabelle/HOL (Q2163157) (← links)
- Translation certification for smart contracts (Q2163161) (← links)
- SMTCoq: a plug-in for integrating SMT solvers into Coq (Q2164216) (← links)
- Certified verification of relational properties (Q2165505) (← links)
- Computer-assisted verification of four interval arithmetic operators (Q2175842) (← links)
- Certification of breadth-first algorithms by extraction (Q2176671) (← links)
- Verified self-explaining computation (Q2176673) (← links)
- A hierarchy of monadic effects for program verification using equational reasoning (Q2176680) (← links)
- System F in Agda, for fun and profit (Q2176683) (← links)
- Completeness theorems for first-order logic analysed in constructive type theory (Q2177578) (← links)
- Certification of nonclausal connection tableaux proofs (Q2180504) (← links)
- Herbrand constructivization for automated intuitionistic theorem proving (Q2180528) (← links)
- DRAT-based bit-vector proofs in CVC4 (Q2181940) (← links)
- Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (Q2198135) (← links)
- Proof-producing synthesis of CakeML from monadic HOL functions (Q2208292) (← links)
- Mac Lane's comparison theorem for the Kleisli construction formalized in Coq (Q2209259) (← links)
- Graph theory in Coq: minors, treewidth, and isomorphisms (Q2209536) (← links)
- Formalizing the LLL basis reduction algorithm and the LLL factorization algorithm in Isabelle/HOL (Q2209537) (← links)
- The \textsc{MetaCoq} project (Q2209542) (← links)
- Exploring the structure of an algebra text with locales (Q2209550) (← links)
- A library for formalization of linear error-correcting codes (Q2209551) (← links)
- Theorem prover for intuitionistic logic based on the inverse method (Q2216868) (← links)
- On a machine-checked proof for fraction arithmetic over a GCD domain (Q2217198) (← links)
- Dual and axiomatic systems for constructive S4, a formally verified equivalence (Q2219076) (← links)
- Formal adventures in convex and conical spaces (Q2219378) (← links)
- Leveraging the information contained in theory presentations (Q2219380) (← links)
- Metamath Zero: designing a theorem prover prover (Q2219381) (← links)
- Maintaining a library of formal mathematics (Q2219408) (← links)
- The Tactician. A seamless, interactive tactic learner and prover for Coq (Q2219409) (← links)
- Intuitionistic fixed point logic (Q2220485) (← links)
- Safe functional systems through integrity types and verified assembly (Q2220814) (← links)
- Certifying certainty and uncertainty in approximate membership query structures (Q2226742) (← links)
- System-level non-interference of constant-time cryptography. II: Verified static analysis and stealth memory (Q2228439) (← links)
- Verified software units (Q2233451) (← links)
- Deductive stability proofs for ordinary differential equations (Q2233505) (← links)
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML (Q2233509) (← links)
- Deductive verification of floating-point Java programs in KeY (Q2233510) (← links)
- Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14--17, 2014. Proceedings (Q2248021) (← links)
