The following pages link to Coq (Q12929):
Displaying 50 items.
- Formal proofs of rounding error bounds. With application to an automatic positive definiteness check (Q2013318) (← links)
- Coquelicot: a user-friendly library of real analysis for Coq (Q2018661) (← links)
- Modular verification of programs with effects and effect handlers in Coq (Q2024352) (← links)
- A process calculus BigrTiMo of mobile systems and its formal semantics (Q2026376) (← links)
- Moessner's theorem: an exercise in coinductive reasoning in \textsc{Coq} (Q2026804) (← links)
- A generic and executable formalization of signature-based Gröbner basis algorithms (Q2028994) (← links)
- Formalization of the Poincaré disc model of hyperbolic geometry (Q2031408) (← links)
- \(\mathrm{HO}\pi\) in Coq (Q2031410) (← links)
- TacticToe: learning to prove with tactics (Q2031416) (← links)
- Automated proof of Bell-LaPadula security properties (Q2031424) (← links)
- Verification of dynamic bisimulation theorems in Coq (Q2035655) (← links)
- A proof assistant based formalisation of a subset of sequential core Erlang (Q2037429) (← links)
- CiMPG+F: a proof generator and fixer-upper for CafeOBJ specifications (Q2037935) (← links)
- Certified semantics for relational programming (Q2038082) (← links)
- Certifying Findel derivatives for blockchain (Q2043802) (← links)
- On solving quantified bit-vector constraints using invertibility conditions (Q2050109) (← links)
- Towards satisfiability modulo parametric bit-vectors (Q2051567) (← links)
- Distilling the requirements of Gödel's incompleteness theorems with a proof assistant (Q2051568) (← links)
- A symbolic-numeric validation algorithm for linear ODEs with Newton-Picard method (Q2051589) (← links)
- Isabelle's metalogic: formalization and proof checker (Q2055847) (← links)
- Harpoon: mechanizing metatheory interactively (Q2055903) (← links)
- Towards efficient verification of population protocols (Q2058386) (← links)
- Experiences from exporting major proof assistant libraries (Q2069875) (← links)
- Discovering and certifying lower bounds for the online bin stretching problem (Q2089680) (← links)
- Logic-independent proof search in logical frameworks (short paper) (Q2096460) (← links)
- Constructive hybrid games (Q2096468) (← links)
- Theorem proving as constraint solving with coherent logic (Q2102932) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- A formalization of SQL with nulls (Q2102947) (← links)
- Formalization of the computational theory of a Turing complete functional language model (Q2102949) (← links)
- A formalization of the Smith normal form in higher-order logic (Q2102950) (← links)
- From the universality of mathematical truth to the interoperability of proof systems (Q2104491) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- \textsc{Prawf}: an interactive proof system for program extraction (Q2106598) (← links)
- A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
- Verifying graph programs with monadic second-order logic (Q2117269) (← links)
- Formally computing with the non-computable (Q2117773) (← links)
- \texttt{slepice}: towards a verified implementation of type theory in type theory (Q2119108) (← links)
- A mechanically verified theory of contracts (Q2119969) (← links)
- A complete semantics of \(\mathbb{K}\) and its translation to Isabelle (Q2119971) (← links)
- Normalising Lustre preserves security (Q2119981) (← links)
- Formalizing geometric algebra in Lean (Q2128117) (← links)
- Online machine learning techniques for Coq: a comparison (Q2128797) (← links)
- A language with type-dependent equality (Q2128827) (← links)
- Proving soundness of extensional normal-form bisimilarities (Q2130582) (← links)
- On models of higher-order separation logic (Q2130583) (← links)
- Self-quotation in a typed, intensional lambda-calculus (Q2130593) (← links)
- A certified program for the Karatsuba method to multiply polynomials (Q2132545) (← links)
- Towards finding longer proofs (Q2142073) (← links)
- The role of entropy in guiding a connection prover (Q2142077) (← links)
