Coq/SSReflect
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Cubical Agda
- CoqEAL
- A semi-automatic proof of strong connectivity
- Program extraction for mutable arrays
- Hammer for Coq: automation for dependent type theory
- Regular language representations in the constructive type theory of Coq
- Certifying standard and stratified Datalog inference engines in SSReflect
- Using abstract stobjs in ACL2 to compute matrix normal forms
- Kenzo
- 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
- Matita
- CTL
- ML4PG
- ForMaRE
- CertiCrypt
- gaia
- EgoMath
- Coquet
- OpenSSL
- Graph theory in Coq: minors, treewidth, and isomorphisms
- PDCoq
- From LCF to Isabelle/HOL
- Some applications of the formalization of the pumping lemma for context-free languages
- Theorem of three circles in Coq
- Formalization of Shannon's theorems
- Formally verified certificate checkers for hardest-to-round computation
- Proof mining with dependent types
- Mtac
- Eisbach
- UniMath
- HoTT
- Formalization of Bing's shrinking method in geometric topology
- Some Wellfounded Trees in UniMath
- Two-Way Automata in Coq
- Verified Operational Transformation for Trees
- ML4PG in computer algebra verification
- Interactive theorem proving. Preface of the special issue
- Eisbach: a proof method language for Isabelle
- Completeness and decidability results for CTL in constructive type theory
- A formal library for elliptic curves in the Coq proof assistant
- A Coq formalization of finitely presented modules
- Completeness and Decidability Results for CTL in Coq
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination
- Towards a certified computation of homology groups for digital images
- An Essence of SSReflect
- Verifying an algorithm computing discrete vector fields for digital imaging
- Formalization of Shannon's theorems in SSReflect-Coq
- A Compact Proof of Decidability for Regular Expression Equivalence
- A Language of Patterns for Subterm Selection
- Deciding regular expressions (in-)equivalence in Coq
- Engineering mathematics: the odd order theorem proof
- A constructive theory of regular languages in Coq
- Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
- Computing persistent homology within Coq/SSReflect
- A certified reduction strategy for homological image processing
- Computational Complexity Via Finite Types
- An introduction to small scale reflection in Coq
- Advances in the Formalization of the Odd Order Theorem
- Point-free, set-free concrete linear algebra
- A formal study of Bernstein coefficients and polynomials
- Constructive Formalization of Hybrid Logic with Eventualities
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- Coquet: a Coq library for verifying hardware
- SynapsCountJ
- Packaging Mathematical Structures
- Fiat
- Formalization and execution of linear algebra: from theorems to algorithms
- Formally verified conditions for regularity of interval matrices
- Finite Groups Representation Theory with Coq
- Tycon
- On the role of formalization in computational mathematics
- HoTTSQL
- Myhill-Nerode
- Tame Graphs
- Graph Theory
- Presburger Automata
- Gauss Jordan Elimination
- Stable Matching
- Arrow Gibbard Satterthwaite
- Q*cert
- SQLCert
- SEQUEL
- Regular Sets
- Rank Nullity
- Girth-Chromatic
- Hereditarily Finite Sets
- Finite Automata HF
- MSO_Regex_Equivalence
- GeoCoq
- SerAPI
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- Foundations of dependent interoperability
- Recycling proof patterns in Coq: case studies
- Constructive completeness for modal logic with transitive closure
- Coherent and Strongly Discrete Rings in Type Theory
- A formal proof of Sasaki-Murao algorithm
- Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
- A library for algorithmic game theory in \textsf{Ssreflect/Coq}
This page was built for software: Coq/SSReflect
