4 search results for "tag:"category:Miscellaneous/Rocq Extensions""

Showing 1 - 4
  1. coq-paramcoq

    No documentation

    Plugin for generating parametricity statements to perform refinement proofs
    keyword:paramcoq keyword:parametricity keyword:OCaml modules category:Miscellaneous/Rocq Extensions logpath:Param date:2024-06-29
    Chantal Keller (Inria, École polytechnique) Marc Lasson (ÉNS de Lyon) Abhishek Anand Pierre Roux Emilio Jesús Gallego Arias et al.
    1.1.3+rocq9.0
    MIT
    Used by 4 other packages
    26 Mar 2025
  2. rocq-aac-tactics

    No documentation

    Rocq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators
    category:Miscellaneous/Rocq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:reflexive tactic keyword:rewriting keyword:rewriting modulo associativity and commutativity keyword:rewriting modulo ac keyword:decision procedure logpath:AAC_tactics date:2025-10-28
    Thomas Braibant Damien Pous Fabian Kunze
    9.0.0
    LGPL-3.0-or-later
    Used by 0 other packages
    28 Oct 2025
  3. rocq-micromega-plugin

    No documentation

    Micromega plugin for Rocq
    category:Miscellaneous/Rocq Extensions keyword:micromega logpath:micromega-plugin
    Frederic Besson
    1.0.0
    LGPL-2.1
    Used by 0 other packages
    16 Apr 2026
  4. rocq-verified-extraction

    No documentation

    Verified extraction from Rocq to OCaml
    keyword:extraction category:Miscellaneous/Rocq Extensions logpath:VerifiedExtraction
    Yannick Forster Matthieu Sozeau Nicolas Tabareau
    1.0.0+9.1
    MIT
    Used by 0 other packages
    13 Mar 2026