9 search results for "author:"Damien Pous""

Showing 1 - 9
  1. coq-aac-tactics

    No documentation

    Coq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators
    category:Miscellaneous/Coq 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:2024-06-27
    Thomas Braibant Damien Pous Fabian Kunze
    8.20.0
    LGPL-3.0-or-later
    Used by 2 other packages
    06 Sep 2024
  2. coq-approx-models

    No documentation

    Rigorous approximations with a posteriori verified operations
    category:Mathematics/Approximation Theory keyword:approximation theory keyword:Chebyshev polynomials keyword:certificate-based approximation logpath:ApproxModels date:2021-06-15
    Florent Bréhard Assia Mahboubi Damien Pous
    1.0
    CECILL-B
    Used by 0 other packages
    16 Jun 2021
  3. coq-atbr

    No documentation

    Coq library and tactic for deciding Kleene algebras
    category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:Kleene algebra keyword:finite automata keyword:semiring keyword:matrices keyword:decision procedure keyword:reflexive tactic logpath:ATBR date:2024-06-30
    Thomas Braibant Damien Pous
    8.20.0
    LGPL-3.0-or-later
    Used by 0 other packages
    06 Sep 2024
  4. coq-coinduction

    No documentation

    A library for doing proofs by (enhanced) coinduction
    keyword:coinduction keyword:up to techniques keyword:companion keyword:bisimilarity logpath:Coinduction date:2024-09-18
    Damien Pous
    1.20
    LGPL-3.0-or-later
    Used by 1 other packages
    18 Sep 2024
  5. coq-coinduction-examples

    No documentation

    Examples on how to use the coq-coinduction library, for doing proofs by (enhanced) coinduction
    keyword:coinduction keyword:up to techniques keyword:companion keyword:bisimilarity keyword:divergence keyword:streams keyword:CCS logpath:CoinductionExamples
    Damien Pous
    1.7
    LGPL-3.0-or-later
    Used by 0 other packages
    13 Jul 2023
  6. coq-graph-theory

    No documentation

    General graph theory definitions and results in Coq and MathComp
    category:Computer Science/Graph Theory keyword:graph theory keyword:minors keyword:treewidth keyword:algebra logpath:GraphTheory.core date:2024-06-30
    Christian Doczkal Damien Pous
    0.9.5
    CECILL-B
    Used by 1 other packages
    30 Jun 2024
  7. coq-graph-theory-planar

    No documentation

    Graph theory results on planarity in Coq and MathComp
    category:Computer Science/Graph Theory keyword:graph theory keyword:planarity logpath:GraphTheory.planar date:2024-06-30
    Christian Doczkal Damien Pous
    0.9.5
    CECILL-B
    Used by 0 other packages
    30 Jun 2024
  8. coq-relation-algebra

    No documentation

    Relation Algebra and KAT in Coq
    keyword:relation algebra keyword:Kleene algebra with tests keyword:KAT keyword:allegories keyword:residuated structures keyword:automata keyword:regular expressions keyword:matrices category:Mathematics/Algebra logpath:RelationAlgebra
    Damien Pous <Damien.Pous@ens-lyon.fr> Christian Doczkal <christian.doczkal@ens-lyon.fr>
    1.7.11
    LGPL-3.0-or-later
    Used by 1 other packages
    18 Sep 2024
  9. coq-weak-up-to

    No documentation

    New Up-to Techniques for Weak Bisimulation
    keyword: weak bisimilarity keyword: weak bisimulation keyword: up-to techniques keyword: termination keyword: commutation keyword: Newman's lemma category: Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems date: 2005-02-22
    Damien Pous <damien.pous at ens-lyon.fr> [http://perso.ens-lyon.fr/damien.pous/]
    8.10.0
    GPL
    Used by 0 other packages
    07 Dec 2019