Open Hub
Open Hub

Tags : Browse Projects

Select a tag to browse associated projects and drill deeper into the tag cloud.

  • coq (18)

    Coq proof assistant

    Compare

      Analyzed 29 days ago

    Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows: * to define functions or predicates, * to state mathematical theorems and software specifications, * to develop interactively formal proofs of these theorems, * to ... [More] check these proofs by a relatively small certification "kernel". [Less]

    335K lines of code

    74 current contributors

    2 months since last commit

    20 users on Open Hub

    Very High Activity
    4.875
       
    0 Reviews
    I Use This
    Mostly written in OCaml
    Licenses: lgpl
    Tags coq extraction functional functional_language language logic mathematics programming proof-assistant proof_assistant proving theorem 1 more...

    learn-haskell-coq-ml-etc

    Compare

      Analyzed 28 days ago

    Where I try code from Haskell (etc) books, articles, etc.

    53.6K lines of code

    1 current contributors

    almost 2 years since last commit

    1 users on Open Hub

    Very Low Activity
    0.0
     
    0 Reviews
    I Use This
    Mostly written in Haskell
    Licenses: No declared licenses
    Tags coq functional_programming haskell ml ocaml scala

    CompCert

    Compare

      Analyzed 29 days ago

    The CompCert project investigates the formal verification of realistic compilers usable for critical embedded software. Such verified compilers come with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. By ... [More] ruling out the possibility of compiler-introduced bugs, verified compilers strengthen the guarantees that can be obtained by applying formal methods to source programs. The main result of the project is the CompCert C verified compiler, a high-assurance compiler for almost all of the C language (ISO C99), generating efficient code for the PowerPC, ARM, RISC-V and x86 processors. [Less]

    203K lines of code

    0 current contributors

    3 months since last commit

    1 users on Open Hub

    Moderate Activity
    0.0
     
    0 Reviews
    I Use This
    Mostly written in coq
    Licenses: No declared licenses
    Tags c compiler coq formally-verified

    Mathematical Components (Coq)

    Compare

      Analyzed 29 days ago

    Mathematical Components are libraries of formalized mathematics developed using the Coq proof assistant. This project finds its roots in the formal proof of the Four Color Theorem. It has been used for large scale formalization projects, including a formal proof of the Odd Order (Feit-Thompson) ... [More] Theorem. The libraries are written using the Ssreflect proof language, now part of the standard distribution of the Coq proof assistant. This is an open source project, licensed under the CeCILL-B free software license agreement. [Less]

    103K lines of code

    0 current contributors

    2 months since last commit

    1 users on Open Hub

    Moderate Activity
    0.0
     
    0 Reviews
    I Use This
    Mostly written in coq
    Licenses: cecill_b
    Tags coq mathematics

    Coq ELPI

    Compare

      Analyzed 28 days ago

    Coq-Elpi provides a Coq plugin that lets one define new commands and tactics in Elpi (Embeddable λProlog Interpreter). For that purpose it provides an embedding of Coq's terms into λProlog using the Higher-Order Abstract Syntax approach (HOAS). It also exports to Elpi a comprehensive set of Coq's ... [More] primitives, so that one can print a message, access the environment of theorems and data types, define a new constant, declare implicit arguments, type classes instances, and so on. For convenience it also provides a quotation and anti-quotation for Coq's syntax, so that one can write {{ nat -> lp:X }} in the middle of a λProlog program instead of the equivalent AST prod `_` (global (indt «Coq.Init.Datatypes.nat»)) X. [Less]

    33.1K lines of code

    0 current contributors

    2 months since last commit

    1 users on Open Hub

    High Activity
    0.0
     
    0 Reviews
    I Use This
    Mostly written in coq
    Licenses: No declared licenses
    Tags coq prolog

    Flocq

    Compare

      No analysis available

    Flocq (Floats for Coq) is a floating-point formalization for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic. It also supports efficient numerical computations inside Coq.

    0 lines of code

    0 current contributors

    0 since last commit

    0 users on Open Hub

    Activity Not Available
    0.0
     
    0 Reviews
    I Use This
    Mostly written in language not available
    Licenses: lgpv3_or_...
    Tags coq floating_point library mathematics rounding

    software-foundations

    Compare

      Analyzed 29 days ago

    Software Foundations in Idris

    615 lines of code

    1 current contributors

    over 6 years since last commit

    0 users on Open Hub

    Inactive
    0.0
     
    0 Reviews
    I Use This
    Mostly written in Nix
    Licenses: No declared licenses
    Tags coq idris proof_assistant proofs textbook

    bonak

    Compare

      Analyzed 29 days ago

    🧊 An indexed construction of truncated n-types

    4.54K lines of code

    0 current contributors

    6 months since last commit

    0 users on Open Hub

    Very Low Activity
    0.0
     
    0 Reviews
    I Use This
    Mostly written in coq
    Licenses: lgpl
    Tags coq hott logic mathematics proving theorem

    Interval Package for Coq

    Compare

      No analysis available

    This library provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.

    0 lines of code

    0 current contributors

    0 since last commit

    0 users on Open Hub

    Activity Not Available
    0.0
     
    0 Reviews
    I Use This
    Mostly written in language not available
    Licenses: lgpl21
    Tags automated coq floating_point interval mathematics

    iron lambda

    Compare

      Analyzed 28 days ago

    Coq formalizations of functional languages

    39.7K lines of code

    0 current contributors

    almost 5 years since last commit

    0 users on Open Hub

    Inactive
    0.0
     
    0 Reviews
    I Use This
    Mostly written in coq
    Licenses: No declared licenses
    Tags coq functional functional_language language mathematics proof research theorem typetheory