swMATH9360MaRDI QIDQ21343FDOQ21343
Author name not available (Why is that?)
Official website: http://coq.inria.fr/announcing-ssreflect-version-12
Cited In (only showing first 100 items - show all)
- Graph theory in Coq: minors, treewidth, and isomorphisms
- Monae
- Coquet: a Coq library for verifying hardware
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- A certified reduction strategy for homological image processing
- A library for algorithmic game theory in \textsf{Ssreflect/Coq}
- Finite Groups Representation Theory with Coq
- Incidence simplicial matrices formalized in Coq/SSReflect
- An Essence of SSReflect
- Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
- Formalization of Shannon's theorems in SSReflect-Coq
- Constructive Formalization of Hybrid Logic with Eventualities
- Towards a certified computation of homology groups for digital images
- Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
- Constructive completeness for modal logic with transitive closure
- Formalization of Bing's shrinking method in geometric topology
- Theorem of three circles in Coq
- Proof mining with dependent types
- A formal study of Bernstein coefficients and polynomials
- A Formalised Lower Bound on Undirected Graph Reachability
- Some Wellfounded Trees in UniMath
- Formalization of the Domination Chain with Weighted Parameters (Short Paper)
- Verified Operational Transformation for Trees
- From LCF to Isabelle/HOL
- Formalization techniques for asymptotic reasoning in classical analysis
- A Coq formalization of finitely presented modules
- Foundations of dependent interoperability
- A formal library for elliptic curves in the Coq proof assistant
- Verifying an algorithm computing discrete vector fields for digital imaging
- Advances in the Formalization of the Odd Order Theorem
- A constructive theory of regular languages in Coq
- Computing persistent homology within Coq/SSReflect
- A Decision Procedure for Regular Expression Equivalence in Type Theory
- JEFL: joint embedding of formal proof libraries
- Coherent and Strongly Discrete Rings in Type Theory
- Formally verified conditions for regularity of interval matrices
- Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings
- How to make ad hoc proof automation less ad hoc
- A semi-automatic proof of strong connectivity
- 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
- Computational Complexity Via Finite Types
- A formalization of multi-tape Turing machines
- Some applications of the formalization of the pumping lemma for context-free languages
- Program extraction for mutable arrays
- Regular language representations in the constructive type theory of Coq
- Kenzo
- Matita
- CTL
- A Compact Proof of Decidability for Regular Expression Equivalence
- ML4PG
- A Language of Patterns for Subterm Selection
- ForMaRE
- CertiCrypt
- gaia
- EgoMath
- Coquet
- OpenSSL
- PDCoq
- Eisbach
- Mtac
- HoTT
- 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
- 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
- Formalization and execution of linear algebra: from theorems to algorithms
- Recycling proof patterns in Coq: case studies
- Interactive theorem proving from the perspective of Isabelle/Isar
- Packaging Mathematical Structures
- UALib
- Certifying standard and stratified Datalog inference engines in SSReflect
- Using abstract stobjs in ACL2 to compute matrix normal forms
- Deciding regular expressions (in-)equivalence in Coq
- Formalization of Shannon's theorems
This page was built for software: Coq/SSReflect
