Cited in
(only showing first 100 items - show all)- Two-Way Automata in Coq
- Completeness and Decidability Results for CTL in Coq
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- Foundations of dependent interoperability
- A formal library for elliptic curves in the Coq proof assistant
- Hammer for Coq: automation for dependent type theory
- ML4PG in computer algebra verification
- Verifying an algorithm computing discrete vector fields for digital imaging
- A machine-checked proof of the odd order theorem
- Formalized linear algebra over elementary divisor rings in \textsc{Coq}
- A formal proof of Sasaki-Murao algorithm
- scientific article; zbMATH DE number 7649962 (Why is no real title available?)
- Advances in the Formalization of the Odd Order Theorem
- Engineering mathematics: the odd order theorem proof
- Graph theory in Coq: minors, treewidth, and isomorphisms
- A constructive theory of regular languages in Coq
- Computing persistent homology within Coq/SSReflect
- JEFL: joint embedding of formal proof libraries
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- Coquet: a Coq library for verifying hardware
- Coherent and Strongly Discrete Rings in Type Theory
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- A certified reduction strategy for homological image processing
- Finite Groups Representation Theory with Coq
- Formally verified conditions for regularity of interval matrices
- A library for algorithmic game theory in \textsf{Ssreflect/Coq}
- An Essence of SSReflect
- Incidence simplicial matrices formalized in Coq/SSReflect
- Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
- Formalization of Shannon's theorems in SSReflect-Coq
- Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings
- Constructive Formalization of Hybrid Logic with Eventualities
- Towards a certified computation of homology groups for digital images
- Eisbach: a proof method language for Isabelle
- Completeness and decidability results for CTL in constructive type theory
- Interactive theorem proving. Preface of the special issue
- Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
- A semi-automatic proof of strong connectivity
- How to make ad hoc proof automation less ad hoc
- Computational Complexity Via Finite Types
- Constructive completeness for modal logic with transitive closure
- Theorem of three circles in Coq
- Formalization of Bing's shrinking method in geometric topology
- A formalization of multi-tape Turing machines
- Some applications of the formalization of the pumping lemma for context-free languages
- Proof mining with dependent types
- Program extraction for mutable arrays
- A formal study of Bernstein coefficients and polynomials
- CoqEAL
- Kenzo
- Matita
- CTL
- ML4PG
- ForMaRE
- CertiCrypt
- gaia
- EgoMath
- Coquet
- OpenSSL
- PDCoq
- Eisbach
- Mtac
- HoTT
- UniMath
- SynapsCountJ
- Fiat
- Tycon
- HoTTSQL
- Arrow Gibbard Satterthwaite
- Graph Theory
- Gauss Jordan Elimination
- Myhill-Nerode
- Presburger Automata
- Q*cert
- SEQUEL
- Regular Sets
- Finite Automata HF
- Girth-Chromatic
- Hereditarily Finite Sets
- Tame Graphs
- Rank Nullity
- Stable Matching
- SQLCert
- GeoCoq
- MSO_Regex_Equivalence
- SerAPI
- UALib
- Regular language representations in the constructive type theory of Coq
- A Compact Proof of Decidability for Regular Expression Equivalence
- A Language of Patterns for Subterm Selection
- A Formalised Lower Bound on Undirected Graph Reachability
- Some Wellfounded Trees in UniMath
- A Coq formalisation of SQL's execution engines
- A formal proof of the minor-exclusion property for treewidth-two graphs
- Towards formal foundations for game theory
- An introduction to small scale reflection in Coq
- Point-free, set-free concrete linear algebra
- Recycling proof patterns in Coq: case studies
- Formalization and execution of linear algebra: from theorems to algorithms
- Packaging Mathematical Structures
This page was built for software: Coq/SSReflect
