Guillaume Melquiond : Projects

Gappa

G

Analyzed over 1 year ago

The Gappa tool helps developers to verify arithmetic properties on their numerical programs (either floating-point or fixed-point computations). It can also generate formal proofs of the properties for extra confidence. It has been successfully used with several projects, e.g. for writing some ... [More]

25.8K lines of code

2 current contributors

almost 5 years since last commit

3 users on Open Hub

Activity Not Available

0 Reviews

I Use This

Mostly written in C++

Licenses: gpl

Remake

I Use This

R

Analyzed 2 days ago

Remake is a build system that provides a Make-compatible rule-based syntax while supporting dynamic dependencies à la Redo. Its code is portable yet fits into a single file, so as to be easily shippable with any project.

2.27K lines of code

1 current contributors

almost 3 years since last commit

1 users on Open Hub

Inactive

0 Reviews

I Use This

Mostly written in C++

Licenses: gpl3_or_l...

Flocq

I Use This

F

Analyzed about 1 year ago

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.

35.7K lines of code

0 current contributors

over 6 years since last commit

0 users on Open Hub

Activity Not Available

0 Reviews

I Use This

Mostly written in coq

Licenses: lgpv3_or_...

Tags coq floating_point library mathematics rounding

Interval Package for Coq

I Use This

I

Analyzed about 2 years ago

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

30.1K lines of code

0 current contributors

over 5 years since last commit

0 users on Open Hub

Activity Not Available

0 Reviews

I Use This