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

Showing 1 - 6

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
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
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
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
coq-reduction-effects

No documentation

A Coq plugin to add reduction side effects to some Coq reduction strategies

logpath:ReductionEffect

Hugo Herbelin

0.1.5

MPL-2.0

Used by 0 other packages

28 Sep 2023
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