8 search results for "author:"Pierre Letouzey""

Showing 1 - 8
  1. coq-bignums

    No documentation

    Bignums, the Coq library of arbitrarily large numbers
    category:Miscellaneous/Coq Extensions category:Mathematics/Arithmetic and Number Theory/Number theory category:Mathematics/Arithmetic and Number Theory/Rational numbers keyword:integer numbers keyword:rational numbers keyword:arithmetic keyword:arbitrary precision logpath:Bignums date:2024-06-20
    Laurent Théry Benjamin Grégoire Arnaud Spiwack Evgeny Makarov Pierre Letouzey
    9.0.0+coq8.20
    LGPL-2.1-only
    Used by 10 other packages
    06 Sep 2024
  2. coq-corn

    No documentation

    The Coq Constructive Repository at Nijmegen
    category:Mathematics/Algebra category:Mathematics/Real Calculus and Topology category:Mathematics/Exact Real computation keyword:constructive mathematics keyword:algebra keyword:real calculus keyword:real numbers keyword:Fundamental Theorem of Algebra logpath:CoRN date:2024-04-23
    Evgeny Makarov Robbert Krebbers Eelis van der Weegen Bas Spitters Jelle Herold et al.
    8.19.0
    GPL-2.0
    Used by 0 other packages
    23 Apr 2024
  3. coq-fsets

    No documentation

    Finite Sets overs Ordered Types
    keyword: finite sets keyword: sorted lists keyword: balanced trees keyword: red-black trees keyword: AVL keyword: functors keyword: data structures category: Computer Science/Data Types and Data Structures category: Miscellaneous/Extracted Programs/Data structures
    Pierre Letouzey Jean-Christophe Filliâtre
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  4. coq-mmaps

    No documentation

    Several implementations of finite maps over arbitrary ordered types using Coq functors
    category:Computer Science/Data Types and Data Structures keyword:finite maps keyword:red-black trees keyword:AVL trees keyword:ordered types logpath:MMaps date:2024-01-08
    Pierre Letouzey Andrew W. Appel
    1.1
    LGPL-2.1-only
    Used by 0 other packages
    08 Jan 2024
  5. coq-qarith

    No documentation

    A Library for Rational Numbers (QArith)
    keyword: Q keyword: arithmetic keyword: rational numbers keyword: setoid keyword: ring category: Mathematics/Arithmetic and Number Theory/Rational numbers category: Miscellaneous/Extracted Programs/Arithmetic
    Pierre Letouzey
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  6. coq-stalmarck

    No documentation

    Verified implementation of Stålmarck's algorithm for proving tautologies in Coq
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures keyword:boolean formula keyword:tautology checker logpath:Stalmarck.Algorithm date:2024-06-30
    Pierre Letouzey Laurent Théry
    8.20.0
    LGPL-2.1-or-later
    Used by 1 other packages
    06 Sep 2024
  7. coq-stalmarck-tactic

    No documentation

    Coq tactic and verified tool for proving tautologies using Stålmarck's algorithm
    category:Miscellaneous/Coq Extensions category:Miscellaneous/Extracted Programs/Decision procedures keyword:boolean formula keyword:tautology checker keyword:tactics logpath:Stalmarck.Tactic date:2024-06-30
    Pierre Letouzey Laurent Théry
    8.20.0
    LGPL-2.1-or-later
    Used by 0 other packages
    06 Sep 2024
  8. coq-tait

    No documentation

    A normalization proof a la Tait for simply-typed lambda-calculus
    keyword: normalization keyword: lambda calculus keyword: extraction keyword: Tait proof keyword: normalization by evalution keyword: type theory category: Mathematics/Logic/Type theory category: Computer Science/Lambda Calculi category: Miscellaneous/Extracted Programs/Type checking unification and normalization date: 2004
    Pierre Letouzey Helmut Schwichtenberg
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019