7 search results for "tag:"category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms""

Showing 1 - 7
  1. coq-belgames

    No documentation

    BelGames: A Formal Theory of Games of Incomplete Information Based on Non-Monotonic Capacities in the Coq Proof Assistant
    keyword:games of incomplete information keyword:belief functions theory keyword:imprecise probability theory category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms logpath:BelGames date:2023-11-26
    Pierre Pomeret-Coquot Erik Martin-Dorel Hélène Fargier
    2.0.0
    MIT
    Used by 0 other packages
    06 Nov 2023
  2. coq-color

    No documentation

    A library on rewriting theory and termination
    date:2024-04-16 logpath:CoLoR category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Computer Science/Data Types and Data Structures category:Computer Science/Lambda Calculi category:Mathematics/Algebra category:Mathematics/Combinatorics and Graph Theory category:Mathematics/Logic/Type theory category:Miscellaneous/Extracted Programs/Type checking unification and normalization keyword:rewriting keyword:termination keyword:lambda calculus keyword:list keyword:multiset keyword:polynomial keyword:vectors keyword:matrices keyword:FSet keyword:FMap keyword:term keyword:context keyword:substitution keyword:universal algebra keyword:varyadic term keyword:string keyword:alpha-equivalence keyword:de Bruijn indices keyword:simple types keyword:matching keyword:unification keyword:relation keyword:ordering keyword:quasi-ordering keyword:lexicographic ordering keyword:ring keyword:semiring keyword:well-foundedness keyword:noetherian keyword:finitely branching keyword:dependent choice keyword:infinite sequences keyword:non-termination keyword:loop keyword:graph keyword:path keyword:transitive closure keyword:strongly connected components keyword:topological ordering keyword:rpo keyword:horpo keyword:dependency pair keyword:dependency graph keyword:semantic labeling keyword:reducibility keyword:Girard keyword:fixpoint theorem keyword:Tarski keyword:pigeon-hole principle keyword:Ramsey theorem
    Frédéric Blanqui Adam Koprowski Sébastien Hinderer Pierre-Yves Strub Sidi Ould Biha et al.
    1.8.5
    CeCILL-2.1
    Used by 0 other packages
    16 Apr 2024
  3. coq-coqeal

    No documentation

    CoqEAL - The Coq Effective Algebra Library
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keyword:effective algebra keyword:elementary divisor rings keyword:Smith normal form keyword:mathematical components keyword:Bareiss keyword:Karatsuba multiplication keyword:refinements logpath:CoqEAL
    Guillaume Cano Cyril Cohen Maxime Dénès Érik Martin-Dorel Anders Mörtberg et al.
    2.1.1
    MIT
    Used by 4 other packages
    08 Dec 2025
  4. coq-coqeal-refinements

    No documentation

    A refinement framework (for algebra)
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keyword:Karatsuba multiplication keyword:refinements logpath:CoqEAL_refinements
    Guillaume Cano Cyril Cohen Maxime Dénès Anders Mörtberg Vincent Siles
    0.9.1
    MIT
    Used by 0 other packages
    25 Nov 2015
  5. coq-huffman

    No documentation

    Coq proof of the correctness of the Huffman coding algorithm
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Miscellaneous/Extracted Programs/Combinatorics keyword:data compression keyword:code keyword:huffman tree logpath:Huffman date:2023-07-09
    Laurent Théry
    8.16.0
    LGPL-2.1-or-later
    Used by 0 other packages
    01 Aug 2023
  6. coq-jmlcoq

    No documentation

    Coq definition of the JML specification language and a verified runtime assertion checker for JML
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms keyword:JML keyword:Java Modeling Language keyword:runtime verification logpath:JML date:2022-06-26
    Hermann Lehner David Pichardie Andreas Kägi
    8.15.0
    MIT
    Used by 0 other packages
    10 Sep 2022
  7. coq-regexp-brzozowski

    No documentation

    Decision procedures for regular expression equivalence in Coq using Mathematical Components
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Computer Science/Formal Languages Theory and Automata keyword:regular expressions keyword:decision procedure keyword:relation algebra logpath:RegexpBrzozowski date:2023-10-14
    Thierry Coquand Vincent Siles
    1.2
    MIT
    Used by 0 other packages
    14 Oct 2023