Coq/SSReflect

swMATH9360MaRDI QIDQ21343FDOQ21343

Author name not available (Why is that?)

Cited In (73)

• 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
• 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
• Formalization of Bing’s Shrinking Method in Geometric Topology
• 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
• Constructive completeness for modal logic with transitive closure
• 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
• 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
• An introduction to small scale reflection in Coq
• Point-free, set-free concrete linear algebra
• 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
• 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
• 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
• Engineering mathematics: the odd order theorem proof
• Finite Groups Representation Theory with Coq
• An Essence of SSReflect
• 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
• Verifying an algorithm computing discrete vector fields for digital imaging

This page was built for software: Coq/SSReflect