Coq/SSReflect - MaRDI portal

swMATH9360MaRDI QIDQ21343FDOQ21343

Author name not available (Why is that?)

Cited In (73)

Finite Groups Representation Theory with Coq
An Essence of SSReflect
Verifying an Algorithm Computing Discrete Vector Fields for Digital Imaging
Title not available (Why is that?)
A Certified Reduction Strategy for Homological Image Processing
A Library for Algorithmic Game Theory in Ssreflect/Coq
Foundations of dependent interoperability
Implementation of Bourbaki's Elements of Mathematics in Coq: Part Two, From Natural Numbers to Real Numbers
Graph theory in Coq: minors, treewidth, and isomorphisms
A Coq Formalization of Finitely Presented Modules
Deciding Regular Expressions (In-)Equivalence 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
Formalization of Shannon’s Theorems in SSReflect-Coq
Coherent and Strongly Discrete Rings in Type Theory
A Formal Library for Elliptic Curves in the Coq Proof Assistant
ML4PG in Computer Algebra Verification
Formalization of Error-Correcting Codes: From Hamming to Modern Coding Theory
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
Engineering mathematics
Formalization of Bing’s Shrinking Method in Geometric Topology
Title not available (Why is that?)
Title not available (Why is that?)
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 Constructive Theory of Regular Languages in Coq
Theorem of three circles in Coq
A formalization of multi-tape Turing machines
Coquet: A Coq Library for Verifying Hardware
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
Towards a Certified Computation of Homology Groups for Digital Images
Regular language representations in the constructive type theory of Coq
Formally Verified Conditions for Regularity of Interval Matrices
A Compact Proof of Decidability for Regular Expression Equivalence
A Formalised Lower Bound on Undirected Graph Reachability
Title not available (Why is that?)
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
A Machine-Checked Proof of the Odd Order Theorem
Recycling proof patterns in Coq: case studies
Packaging Mathematical Structures
Proof-relevant Horn Clauses for Dependent Type Inference and Term Synthesis
Formalized linear algebra over Elementary Divisor Rings in Coq
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
Formalization of Shannon's theorems
Formally verified certificate checkers for hardest-to-round computation
On the role of formalization in computational mathematics
Incidence Simplicial Matrices Formalized in Coq/SSReflect
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
Point-Free, Set-Free Concrete Linear Algebra
Hammer for Coq: automation for dependent type theory
Constructive Completeness for Modal Logic with Transitive Closure
Title not available (Why is that?)
Advances in the Formalization of the Odd Order Theorem
Formalization and Execution of Linear Algebra: From Theorems to Algorithms

This page was built for software: Coq/SSReflect