Coq/SSReflect
From MaRDI portal
Software:21343
swMATH9360MaRDI QIDQ21343FDOQ21343
Author name not available (Why is that?)
Cited In (73)
- A certified reduction strategy for homological image processing
- A library for algorithmic game theory in \textsf{Ssreflect/Coq}
- Finite Groups Representation Theory with Coq
- An Essence of SSReflect
- Implementation of Bourbaki's \textit{Elements of mathematics} in Coq. II: From natural numbers to real numbers
- Formalization techniques for asymptotic reasoning in classical analysis
- Foundations of dependent interoperability
- Verifying an algorithm computing discrete vector fields for digital imaging
- Graph theory in Coq: minors, treewidth, and isomorphisms
- 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
- 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
- Formally verified conditions for regularity of interval matrices
- 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
- Constructive Formalization of Hybrid Logic with Eventualities
- Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings
- Towards a certified computation of homology groups for digital images
- 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
- Constructive completeness for modal logic with transitive closure
- Formalization of Bing's shrinking method in geometric topology
- Theorem of three circles in Coq
- 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
- Regular language representations in the constructive type theory of Coq
- A Compact Proof of Decidability for Regular Expression Equivalence
- A Formalised Lower Bound on Undirected Graph Reachability
- A Language of Patterns for Subterm Selection
- 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
- 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
- Formalization of the Domination Chain with Weighted Parameters (Short Paper)
- Verified Operational Transformation for Trees
- From LCF to Isabelle/HOL
- 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
- A Coq formalization of finitely presented modules
- Formalization of Shannon's theorems
- Formally verified certificate checkers for hardest-to-round computation
- On the role of formalization in computational mathematics
- 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
- A formal library for elliptic curves in the Coq proof assistant
- ML4PG in computer algebra verification
- A machine-checked proof of the odd order theorem
- Hammer for Coq: automation for dependent type theory
- Formalized linear algebra over elementary divisor rings in \textsc{Coq}
- A formal proof of Sasaki-Murao algorithm
- Title not available (Why is that?)
- Advances in the Formalization of the Odd Order Theorem
- Engineering mathematics: the odd order theorem proof
This page was built for software: Coq/SSReflect
