Open Hub
Open Hub

Tags : Browse Projects

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

Coq proof assistant

Compare

  Analyzed 1 day 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]

341K lines of code

74 current contributors

2 days 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 1 day ago

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

53.6K lines of code

1 current contributors

over 2 years since last commit

1 users on Open Hub

Inactive
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 about 16 hours 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]

205K lines of code

0 current contributors

10 days 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 about 12 hours 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]

109K lines of code

0 current contributors

1 day 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 about 20 hours 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]

34.3K lines of code

0 current contributors

4 days 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 about 17 hours ago

Software Foundations in Idris

615 lines of code

1 current contributors

almost 7 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 about 12 hours ago

🧊 An indexed construction of truncated n-types

4.54K lines of code

0 current contributors

12 days 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 about 14 hours ago

Coq formalizations of functional languages

39.7K lines of code

0 current contributors

about 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