245 search results for "tag:"date:""

Showing 201 - 245
  1. coq-reglang

    No documentation

    Representations of regular languages (i.e., regexps, various types of automata, and WS1S) with equivalence proofs, in Coq and MathComp
    category:Computer Science/Formal Languages Theory and Automata keyword:regular languages keyword:regular expressions keyword:finite automata keyword:two-way automata keyword:monadic second-order logic logpath:RegLang date:2024-01-19
    Christian Doczkal Jan-Oliver Kaiser Gert Smolka
    1.2.2
    CECILL-B
    Used by 1 other packages
    10 May 2025
  2. coq-relation-extraction

    No documentation

    Functions extraction from inductive relations
    keyword: extraction keyword: inductive relations keyword: semantics category: Computer Science/Semantics and Compilation/Compilation date: 2011
    Catherine Dubois, David Delahaye, Pierre-Nicolas Tollitte
    8.8.0
    Unknown
    Used by 0 other packages
    06 Feb 2019
  3. coq-robot

    No documentation

    Formal Foundations for Modeling Robot Manipulators
    keyword:robotics keyword:3D geometry logpath:robot date:2021-05-11
    Reynald Affeldt, AIST Cyril Cohen, Inria Laurent Thery, Inria
    0.1
    LGPL-2.1-or-later
    Used by 0 other packages
    11 May 2021
  4. 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
  5. coq-ruler-compass-geometry

    No documentation

    Ruler and compass geometry axiomatization
    keyword: geometry keyword: plane geometry keyword: ruler and compass geometry keyword: Euclidian geometry keyword: Hilbert's axioms category: Mathematics/Geometry/General date: 2007-11
    Jean Duprat <Jean.Duprat@ens-lyon.fr>
    8.10.0
    GNU Lesser Public License
    Used by 0 other packages
    07 Dec 2019
  6. coq-scev

    No documentation

    Proofs and simplification lemmas of an algebraic theory of recurrences
    keyword:mathematics category:Miscellaneous/Coq Extensions date:2016-09-01 logpath:coq-scev
    Siddharth Bhat
    1.0.1
    MIT
    Used by 0 other packages
    20 Nov 2018
  7. coq-simple-io

    No documentation

    IO monad for Coq
    date:2025-02-28 logpath:SimpleIO keyword:extraction keyword:effects
    Li-yao Xia Yishuai Li
    1.11.0
    MIT
    Used by 7 other packages
    28 Feb 2025
  8. coq-smc

    No documentation

    BDD based symbolic model checker for the modal mu-calculus
    keyword: BDD keyword: binary decision diagrams keyword: classical logic keyword: propositional logic keyword: garbage collection keyword: modal mu-calculus keyword: model checking keyword: symbolic model checking keyword: reflection category: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures date: 2002-11
    Kumar Neeraj Verma <verma@lsv.ens-cachan.fr>
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  9. coq-smlms

    No documentation

    A formal semantics capturing value binding in a language with a powerful module system such as OCaml.
    category:Computer Science/Semantics and Compilation/Semantics keywords: adequacy keywords: modules keywords: module types keywords: OCaml keywords: refactoring keywords: renaming keywords: semantics logpath:AbstractRenaming date:2023-02-14
    Hugo Férée
    1.0.0
    MIT
    Used by 0 other packages
    16 Feb 2023
  10. 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
  11. 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
  12. coq-stdpp

    No documentation

    An extended "Standard Library" for Coq
    date:2024-10-31 logpath:stdpp
    The std++ team
    1.11.0
    BSD-3-Clause
    Used by 4 other packages
    31 Oct 2024
  13. coq-stdpp-bitvector

    No documentation

    A library for bitvectors based on std++
    date:2024-10-31 logpath:stdpp.bitvector
    The std++ team
    1.11.0
    BSD-3-Clause
    Used by 1 other packages
    31 Oct 2024
  14. 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
  15. 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
  16. coq-sum-of-two-square

    No documentation

    Numbers equal to the sum of two square numbers
    keyword: number theory category: Mathematics/Arithmetic and Number Theory/Number theory date: 2004-12-13
    Laurent Thery
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  17. coq-switch

    No documentation

    A plugin to implement functionality similar to `switch` statement in C language
    category:Miscellaneous/Coq Extensions date:2023-12-13 logpath:Switch
    Vadim Zaliva <lord@crocodile.org>
    1.0.6
    MIT
    Used by 0 other packages
    13 Dec 2023
  18. 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
  19. coq-tarski-geometry

    No documentation

    Tarski's geometry
    keyword: geometry keyword: Tarski's geometry keyword: congruence keyword: between property keyword: orthogonality category: Mathematics/Geometry/General date: 2006-03
    Julien Narboux <Julien.Narboux@dpt-info.u-strasbg.fr> [http://dpt-info.u-strasbg.fr/~narboux/]
    8.10.0
    GPL
    Used by 0 other packages
    07 Dec 2019
  20. coq-tlc

    No documentation

    TLC: A Library for Classical Coq
    category:Computer Science/Data Types and Data Structures date:2024-02-09 keyword:classical logic logpath:TLC
    Arthur Charguéraud
    20240209
    MIT
    Used by 2 other packages
    13 Feb 2024
  21. coq-topology

    No documentation

    General topology in Coq
    category:Mathematics/Real Calculus and Topology date:2023-08-18 keyword:topology keyword:filters keyword:nets keyword:metric spaces keyword:real analysis keyword:Urysohn's lemma keyword:Tietze extension theorem logpath:Topology
    Daniel Schepler
    10.2.0
    LGPL-2.1-or-later
    Used by 0 other packages
    21 Aug 2023
  22. coq-tortoise-hare-algorithm

    No documentation

    Tortoise and the hare algorithm
    keyword: program verification keyword: paths keyword: cycle detection keyword: graphs keyword: graph theory keyword: finite sets keyword: Floyd category: Computer Science/Decision Procedures and Certified Algorithms/Correctness proofs of algorithms date: 2007-02
    Jean-Christophe Filliâtre
    8.10.0
    Unknown
    Used by 0 other packages
    07 Dec 2019
  23. coq-trakt

    No documentation

    A generic goal preprocessing tool for proof automation tactics in Coq
    category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures category:Miscellaneous/Coq Extensions keyword:automation keyword:elpi date:2022-05-16 logpath:Trakt
    Enzo Crance
    1.2c
    LGPL-3.0-or-later
    Used by 0 other packages
    19 Jun 2024
  24. coq-tree-automata

    No documentation

    Tree automatas
    keyword: tree automatas keyword: bottom up reflexion terms category: Computer Science/Formal Languages Theory and Automata date: september 1999
    Xavier Rival [http://www.eleves.ens.fr/home/rival]
    8.10.0
    LGPL 2.1
    Used by 0 other packages
    07 Dec 2019
  25. coq-tree-calculus

    No documentation

    A Coq library for tree calculus
    keyword:tree calculus keyword:reflective programs category:Computer Science/Lambda Calculi date:2020-09-20 logpath:Reflective
    Barry Jay
    1.0.0
    MIT
    Used by 0 other packages
    21 Sep 2020
  26. coq-typing-flags

    No documentation

    A Coq plugin to disable positivity check, guard check and termination check
    keyword:non-termination keyword:type-in-type category:Miscellaneous/Coq Extensions date:2019-11-02 logpath:TypingFlags
    Simon Boulier
    1.0
    Unknown
    Used by 0 other packages
    02 Nov 2019
  27. coq-unicoq

    No documentation

    An enhanced unification algorithm for Coq
    logpath:Unicoq date:2024-11-22
    Matthieu Sozeau <matthieu.sozeau@inria.fr> Beta Ziliani <beta@mpi-sws.org>
    1.6+8.20
    MIT
    Used by 1 other packages
    22 Nov 2024
  28. coq-vcfloat

    No documentation

    VCFloat: Floating Point Round-off Error Analysis
    date:2025-02-10 keyword:decision procedure keyword:floating-point arithmetic category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VCFloat
    Andrew W. Appel Ariel E. Kellison Tahina Ramananandro Paul Mountcastle Benoit Meister et al.
    2.3
    LGPL-3.0-or-later
    Used by 1 other packages
    10 Feb 2025
  29. coq-vellvm

    No documentation

    Coq library implementing (executable) semantics for LLVM IR
    date:2025-01-10 category:Computer Science/Programming Languages/Formal Definitions and Theory category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:semantics keyword:interpreter keyword:LLVM logpath:Vellvm
    Steve Zdancewic <stevez@cis.upenn.edu> Yannick Zakowski <yannick.zakowski@inria.fr> Calvin Beck <hobbes@seas.upenn.edu> Irene Yoon <euisuny@cis.upenn.edu> Gary (Hanxi) Chen <hanxic@seas.upenn.edu>
    v2.0.20250110
    GPL-3.0-or-later
    Used by 0 other packages
    11 Jan 2025
  30. coq-vlsm

    No documentation

    Coq formalization of validating labelled state transition and message production systems
    category:Computer Science/Concurrent Systems and Protocols/Theory of concurrent systems keyword:consensus keyword:fault tolerance keyword:distributed algorithms keyword:Paxos logpath:VLSM date:2023-12-15
    Mihai Calancea Denisa Diaconescu Wojciech Kołowski Elaine Li Brandon Moore et al.
    1.3
    BSD-3-Clause
    Used by 0 other packages
    15 Dec 2023
  31. coq-void

    No documentation

    MathComp instances for the empty type (Empty_set)
    keyword:empty type keyword:class instances category:Computer Science/Data Types and Data Structures date:2019-10-08 logpath:void
    Arthur Azevedo de Amorim
    0.1.0
    MIT
    Used by 0 other packages
    08 Oct 2019
  32. coq-vst

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2024-04-12
    Andrew W. Appel Lennart Beringer William Mansky Josiah Dodds Qinxiang Cao et al.
    3.0beta2
    BSD-2-Clause
    Used by 1 other packages
    15 Apr 2024
  33. coq-vst-32

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2024-03-20
    Andrew W. Appel Lennart Beringer Josiah Dodds Qinxiang Cao Aquinas Hobor et al.
    2.14
    BSD-2-Clause
    Used by 0 other packages
    21 Mar 2024
  34. coq-vst-64

    No documentation

    Verified Software Toolchain
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2020-08-02
    Andrew W. Appel Lennart Beringer Sandrine Blazy Qinxiang Cao Santiago Cuellar et al.
    2.6
    https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE
    Used by 0 other packages
    03 Aug 2020
  35. coq-vst-iris

    No documentation

    Verified Software Toolchain with Iris
    category:Computer Science/Semantics and Compilation/Semantics keyword:C logpath:VST date:2023-01-24
    William Mansky Shengyi Wang
    2.11.1
    https://raw.githubusercontent.com/PrincetonUniversity/VST/master/LICENSE
    Used by 0 other packages
    25 Jan 2023
  36. coq-vst-lib

    No documentation

    VSTlib: VST-verified C library for VST-verified clients
    date:2025-02-10 keyword:VST keyword:library keyword:malloc keyword:threads keyword:floating-point arithmetic category:Miscellaneous/Coq Extensions category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:VSTlib
    Andrew W. Appel William Mansky
    2.15.1
    BSD-2-Clause
    Used by 0 other packages
    10 Feb 2025
  37. coq-wasm

    No documentation

    Wasm formalisation in Coq
    keyword:WebAssembly category:Computer Science/Semantics and Compilation/Semantics date:2025-03-13 logpath:Wasm
    Martin Bodin Philippa Gardner Jean Pichon Xiaojia Rao Conrad Watt
    2.0.2
    MIT
    Used by 0 other packages
    14 Mar 2025
  38. coq-waterproof
    Documentation
    Coq proofs in a style that resembles non-mechanized mathematical proofs
    keyword:mathematics education category:Mathematics/Education date:2023-08-27 logpath:Waterproof
    Jelle Wemmenhove Balthazar Pathiachvili Cosmin Manea Lulof Pirée Adrian Vrămuleţ et al.
    2.0.1+8.17
    LGPL-3.0-or-later
    Used by 0 other packages
    27 Aug 2023
  39. 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
  40. coq-yalla

    No documentation

    Yalla library
    keyword:linear logic keyword:metatheory keyword:cut elimination category:Mathematics/Logic/Foundations date:2024-09-16 logpath:Yalla
    Olivier Laurent
    2.0.6
    LGPL-3.0-or-later
    Used by 0 other packages
    16 Sep 2024
  41. coq-zorns-lemma

    No documentation

    This library develops some basic set theory in Coq
    category:Mathematics/Logic/Set theory date:2023-08-18 keyword:set theory keyword:cardinals keyword:ordinal numbers keyword:finite keyword:countable keyword:quotients keyword:well-orders keyword:Zorn's lemma logpath:ZornsLemma
    Daniel Schepler
    10.2.0
    LGPL-2.1-or-later
    Used by 1 other packages
    21 Aug 2023
  42. rocq-bignums

    No documentation

    Bignums, the Rocq 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+rocq9.0
    LGPL-2.1-only
    Used by 1 other packages
    20 Mar 2025
  43. rocq-ollibs

    No documentation

    OL libraries
    keyword:standard library keyword:list keyword:permutation keyword:decidable equality keyword:finite multisets category:Mathematics/Combinatorics and Graph Theory date:2025-04-22 logpath:OLlibs
    Olivier Laurent Christophe Lucas
    2.1.0
    LGPL-3.0-or-later
    Used by 0 other packages
    23 Apr 2025
  44. rocq-vellvm

    No documentation

    Rocq library implementing (executable) semantics for LLVM IR
    date:2025-03-27 category:Computer Science/Programming Languages/Formal Definitions and Theory category:Computer Science/Semantics and Compilation/Compilation category:Computer Science/Semantics and Compilation/Semantics keyword:semantics keyword:interpreter keyword:LLVM logpath:Vellvm
    Steve Zdancewic <stevez@cis.upenn.edu> Yannick Zakowski <yannick.zakowski@inria.fr> Calvin Beck <hobbes@seas.upenn.edu> Irene Yoon <euisuny@cis.upenn.edu> Gary (Hanxi) Chen <hanxic@seas.upenn.edu>
    v2.1.20250327
    GPL-3.0-or-later
    Used by 0 other packages
    27 Mar 2025
  45. rocq-yalla

    No documentation

    Yalla library
    keyword:linear logic keyword:metatheory keyword:cut elimination category:Mathematics/Logic/Foundations date:2025-03-26 logpath:Yalla
    Olivier Laurent
    2.0.7
    LGPL-3.0-or-later
    Used by 0 other packages
    27 Mar 2025
... 3 4 5