6 search results for "author:"Hugo Herbelin""

Showing 1 - 6
  1. coq-coqoban

    No documentation

    Coqoban (Sokoban in Coq)
    category:Miscellaneous/Logical Puzzles and Entertainment keyword:Sokoban keyword:puzzles logpath:Coqoban
    Jasper Stein Hugo Herbelin
    8.13.0
    LGPL-2.1-or-later
    Used by 0 other packages
    21 Aug 2021
  2. coq-higman-nw

    No documentation

    A program from an A-translated impredicative proof of Higman's Lemma
    keyword: A-translation keyword: Higman's lemma keyword: impredicativity keyword: System F keyword: extraction category: Mathematics/Logic category: Mathematics/Combinatorics and Graph Theory category: Miscellaneous/Extracted Programs/Combinatorics
    Hugo Herbelin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  3. coq-paradoxes

    No documentation

    Paradoxes in Set Theory and Type Theory
    keyword: Reynolds paradox keyword: Burali-Forti paradox keyword: Diaconescu paradox keyword: set theory keyword: system U keyword: inconsistency keyword: Hurkens paradox category: Mathematics/Logic/Foundations
    Bruno Barras Thierry Coquand Hugo Herbelin Benjamin Werner
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  4. coq-ptsatr

    No documentation

    PTSATR
    keyword: pure type systems keyword: judgmental equality keyword: Church-Rosser keyword: confluence keyword: subject reduction keyword: pi injectivity category: Mathematics/Logic/Type theory
    Vincent Siles <vincent.siles@ens-lyon.org> [http://www.lix.polytechnique.fr/~vsiles] Hugo Herbelin <hugo.herbelin@inria.fr> [http://pauillac.inria.fr/~herbelin/]
    8.10.0
    LGPL
    Used by 1 other packages
    07 Dec 2019
  5. coq-reduction-effects

    No documentation

    A Coq plugin to add reduction side effects to some Coq reduction strategies
    logpath:ReductionEffect
    Hugo Herbelin
    0.1.6
    MPL-2.0
    Used by 0 other packages
    08 Sep 2025
  6. coq-schroeder

    No documentation

    The Theorem of Schroeder-Bernstein
    keyword: Schroeder-Bernstein keyword: set theory category: Mathematics/Logic/Set theory
    Hugo herbelin
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019