26 search results for "author:"Laurent Théry""

Showing 1 - 26
  1. coq-bertrand

    No documentation

    Correctness of Knuth's algorithm for prime numbers
    category:Mathematics/Arithmetic and Number Theory/Number theory category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs based on external tools category:Miscellaneous/Extracted Programs/Arithmetic keyword:Knuth's algorithm keyword:prime numbers keyword:Bertrand's postulate logpath:Bertrand date:2020-10-10
    Laurent Théry
    8.12.0
    LGPL-2.1-or-later
    Used by 0 other packages
    11 Oct 2020
  2. 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
  3. coq-buchberger

    No documentation

    Verified implementation in Coq of Buchberger's algorithm for computing Gröbner bases
    category:Mathematics/Algebra category:Miscellaneous/Extracted Programs/Combinatorics keyword:Gröbner basis keyword:polynomial ideal keyword:Buchberger's algorithm logpath:Buchberger date:2023-12-28
    Laurent Théry Henrik Persson
    8.18.0
    LGPL-2.1-or-later
    Used by 0 other packages
    28 Dec 2023
  4. coq-coqprime

    No documentation

    Certifying prime numbers in Coq
    Laurent Théry
    1.6.0
    LGPL-2.1-only
    Used by 1 other packages
    19 Dec 2024
  5. coq-coqprime-generator

    No documentation

    Certificate generator for prime numbers in Coq
    Laurent Théry
    1.1.2
    LGPL-2.1-only
    Used by 0 other packages
    16 Jan 2025
  6. coq-float

    No documentation

    Library for floating-point numbers
    keyword: floating-point arithmetic category: Computer Science/Data Types and Data Structures date: 2001
    Laurent Théry Sylvie Boldo
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  7. coq-geometric-algebra

    No documentation

    Grassman Cayley and Clifford formalisations
    logpath:GeometricAlgebra
    Laurent Théry
    0.8.12
    LGPL-2.1-only
    Used by 0 other packages
    27 Aug 2020
  8. coq-hanoi

    No documentation

    Hanoi tower in Coq
    keyword:hanoi tower logpath:hanoi
    Laurent Théry
    1.0.0
    MIT
    Used by 0 other packages
    20 Jan 2022
  9. coq-huffman

    No documentation

    Coq proof of the correctness of the Huffman coding algorithm
    category:Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms category:Miscellaneous/Extracted Programs/Combinatorics keyword:data compression keyword:code keyword:huffman tree logpath:Huffman date:2023-07-09
    Laurent Théry
    8.16.0
    LGPL-2.1-or-later
    Used by 0 other packages
    01 Aug 2023
  10. coq-mathcomp-analysis

    No documentation

    An analysis library for mathematical components
    category:Mathematics/Real Calculus and Topology keyword:analysis keyword:Cantor keyword:topology keyword:real numbers keyword:sequence keyword:convexity keyword:Landau notation keyword:logarithm keyword:sin keyword:cos keyword:tangent keyword:trigonometric function keyword:exponential keyword:differentiation keyword:derivative keyword:measure theory keyword:integration keyword:Lebesgue keyword:probability logpath:mathcomp.analysis
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.9.0
    CECILL-C
    Used by 7 other packages
    20 Feb 2025
  11. coq-mathcomp-analysis-stdlib

    No documentation

    A library to link real numbers from mathematical components and Stdlib
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.reals_stdlib
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.9.0
    CECILL-C
    Used by 0 other packages
    20 Feb 2025
  12. coq-mathcomp-classical

    No documentation

    A library for classical logic for mathematical components
    category:Mathematics/Logic/Classical logic keyword:classical logic keyword:logic keyword:sets keyword:set theory keyword:function keyword:cardinal keyword:filter logpath:mathcomp.classical
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.9.0
    CECILL-C
    Used by 2 other packages
    20 Feb 2025
  13. coq-mathcomp-experimental-reals

    No documentation

    A library for alternative real numbers for mathematical components
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.experimental_reals
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.9.0
    CECILL-C
    Used by 1 other packages
    20 Feb 2025
  14. coq-mathcomp-field-extra

    No documentation

    Extra Mathematical Components Library on Fields
    keyword:algebra keyword:field keyword:small scale reflection keyword:mathematical components keyword:odd order theorem
    Jeremy Avigad <> Andrea Asperti <> Stephane Le Roux <> Yves Bertot <> Laurence Rideau <> et al.
    1.6.1
    CeCILL-B
    Used by 1 other packages
    26 Jun 2019
  15. coq-mathcomp-odd-order

    No documentation

    The formal proof of the Feit-Thompson theorem
    keyword:finite groups keyword:Feit Thompson theorem keyword:small scale reflection keyword:mathematical components keyword:odd order theorem
    Jeremy Avigad <> Andrea Asperti <> Stephane Le Roux <> Yves Bertot <> Laurence Rideau <> et al.
    2.1.0
    CeCILL-B
    Used by 0 other packages
    04 Jan 2025
  16. coq-mathcomp-reals

    No documentation

    A library for real numbers for mathematical components
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals keyword:extended real numbers logpath:mathcomp.reals
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.9.0
    CECILL-C
    Used by 3 other packages
    20 Feb 2025
  17. coq-mathcomp-reals-stdlib

    No documentation

    A library to link real numbers from mathematical components and Stdlib
    category:Mathematics/Real Numbers keyword:real numbers keyword:reals logpath:mathcomp.reals_stdlib
    Reynald Affeldt Alessandro Bruni Yves Bertot Cyril Cohen Marie Kerjean et al.
    1.9.0
    CECILL-C
    Used by 4 other packages
    20 Feb 2025
  18. coq-mathcomp-tarjan

    No documentation

    Strongly connected component algorithms by Tarjan and Kosaraju using Coq and MathComp
    category:Computer Science/Graph Theory keyword:strongly connected components keyword:topological sorting keyword:Kosaraju keyword:Tarjan keyword:acyclicity keyword:graph theory logpath:mathcomp.tarjan date:2023-08-06
    Cyril Cohen Jean-Jacques Lévy Karl Palmskog Laurent Théry
    1.0.2
    CECILL-B
    Used by 0 other packages
    06 Aug 2023
  19. coq-poltac

    No documentation

    A set of tactics to deal with inequalities in Coq over N, Z and R:
    logpath:PolTac
    Laurent Théry
    0.8.12
    LGPL-2.1-only
    Used by 0 other packages
    27 Aug 2020
  20. coq-presburger

    No documentation

    Presburger's algorithm
    keyword: integers keyword: arithmetic keyword: decision procedure keyword: Presburger category: Mathematics/Logic/Foundations category: Mathematics/Arithmetic and Number Theory/Miscellaneous category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures date: March 2002
    Laurent Théry
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  21. coq-rsa

    No documentation

    Correctness of RSA algorithm
    keyword: RSA keyword: Chinese remainder keyword: Fermat's little theorem category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms date: 1999
    Jose C. Almeida Laurent Théry
    8.10.0
    LGPL-2.1-only
    Used by 0 other packages
    07 Dec 2019
  22. coq-ssreflect

    No documentation

    The Small Scale Reflection extension
    Jeremy Avigad <> Andrea Asperti <> Stephane Le Roux <> Yves Bertot <> Laurence Rideau <> et al.
    1.5.0
    CeCILL-B
    Used by 3 other packages
    13 May 2019
  23. 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
  24. 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
  25. coq-string

    No documentation

    Definition of strings in Coq
    keyword: string keyword: ascii character category: Miscellaneous/Coq Extensions date: 2002-03
    Laurent Théry
    8.6.0
    LGPL 2.1
    Used by 0 other packages
    20 Nov 2018
  26. coq-sudoku

    No documentation

    Sudoku solver certified in Coq
    category:Miscellaneous/Logical Puzzles and Entertainment keyword:puzzles keyword:Davis-Putnam keyword:sudoku logpath:Sudoku date:2022-10-19
    Laurent Théry
    8.16.0
    LGPL-2.1-or-later
    Used by 0 other packages
    19 Oct 2022