The following pages link to Coq/SSReflect (Q21343):
Displayed 50 items.
- Interactive theorem proving. Preface of the special issue (Q287356) (← links)
- Eisbach: a proof method language for Isabelle (Q287365) (← links)
- Completeness and decidability results for CTL in constructive type theory (Q287375) (← links)
- On the role of formalization in computational mathematics (Q372699) (← links)
- Recycling proof patterns in Coq: case studies (Q475385) (← links)
- Intelligent computer mathematics. 18th symposium, Calculemus 2011, and 10th international conference, MKM 2011, Bertinoro, Italy, July 18--23, 2011. Proceedings (Q555659) (← links)
- A formalization of multi-tape Turing machines (Q744986) (← links)
- JEFL: joint embedding of formal proof libraries (Q831932) (← links)
- A semi-automatic proof of strong connectivity (Q1630027) (← links)
- Program extraction for mutable arrays (Q1648867) (← links)
- Hammer for Coq: automation for dependent type theory (Q1663240) (← links)
- Regular language representations in the constructive type theory of Coq (Q1663246) (← links)
- Certifying standard and stratified Datalog inference engines in SSReflect (Q1687733) (← links)
- Using abstract stobjs in ACL2 to compute matrix normal forms (Q1687754) (← links)
- A Coq formalisation of SQL's execution engines (Q1791148) (← links)
- A formal proof of the minor-exclusion property for treewidth-two graphs (Q1791156) (← links)
- Towards formal foundations for game theory (Q1791194) (← links)
- Graph theory in Coq: minors, treewidth, and isomorphisms (Q2209536) (← links)
- From LCF to Isabelle/HOL (Q2280211) (← links)
- Some applications of the formalization of the pumping lemma for context-free languages (Q2333674) (← links)
- Theorem of three circles in Coq (Q2351412) (← links)
- Formalization of Shannon's theorems (Q2352494) (← links)
- Formally verified certificate checkers for hardest-to-round computation (Q2352500) (← links)
- Proof mining with dependent types (Q2364689) (← links)
- Formalization of Bing’s Shrinking Method in Geometric Topology (Q2817290) (← links)
- Some Wellfounded Trees in UniMath (Q2819193) (← links)
- Two-Way Automata in Coq (Q2829256) (← links)
- Verified Operational Transformation for Trees (Q2829271) (← links)
- ML4PG in Computer Algebra Verification (Q2843038) (← links)
- A Formal Library for Elliptic Curves in the Coq Proof Assistant (Q2879245) (← links)
- A Coq Formalization of Finitely Presented Modules (Q2879252) (← links)
- Completeness and Decidability Results for CTL in Coq (Q2879254) (← links)
- Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination (Q2881068) (← links)
- Towards a Certified Computation of Homology Groups for Digital Images (Q2900562) (← links)
- An Essence of SSReflect (Q2907323) (← links)
- Verifying an Algorithm Computing Discrete Vector Fields for Digital Imaging (Q2907325) (← links)
- Formalization of Shannon’s Theorems in SSReflect-Coq (Q2914745) (← links)
- A Compact Proof of Decidability for Regular Expression Equivalence (Q2914749) (← links)
- A Language of Patterns for Subterm Selection (Q2914755) (← links)
- Deciding Regular Expressions (In-)Equivalence in Coq (Q2915138) (← links)
- Engineering mathematics (Q2931776) (← links)
- A Constructive Theory of Regular Languages in Coq (Q2938041) (← links)
- Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory (Q2945620) (← links)
- Computing persistent homology within Coq/SSReflect (Q2946715) (← links)
- A Certified Reduction Strategy for Homological Image Processing (Q2946732) (← links)
- Computational Complexity Via Finite Types (Q2946764) (← links)
- (Q3075246) (← links)
- Advances in the Formalization of the Odd Order Theorem (Q3087991) (← links)
- Point-Free, Set-Free Concrete Linear Algebra (Q3088000) (← links)
- A formal study of Bernstein coefficients and polynomials (Q3094174) (← links)