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

Showing 1 - 2
  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