Mentions légales du service
An LR(1) parser generator for OCaml.
Why3 is a software verification platform, featuring a versatile ML-style language and interfaces to various powerful automated and interactive theorem provers.
Primary library for necro with standard tools (parse, type check, print, and transform Skeletal Semantics)
Verifiable online voting system
DEPRECATED, MOVED TO GITHUB https://github.com/MLanguage/mlang
Itauto: an Extensible Intuitionistic SAT Solver
Sources of the Abstract Categorial Development toolkit.
ProVerif symbolic protocol verifier
Mapping a tensor to a lower-dimensional tensor, optionally permuting its dimensions.
This project strives to generate loop iterating over these structures.
Heptagon is a synchronous dataflow language whose syntax and semantics is inspired from Lustre, with a syntax allowing the expression of control structures (e.g., switch or mode automata).
An OCaml library that provides facilities for memoization and fixed points.
Resources for course MPRI 2-4 on functional programming and type systems.
DEPRECATED, TRANSFERED TO GITHUB : https://github.com/CatalaLang/catala
A generator of debugger for the Skel language for semantics description
Separation Logic with Characteristic Formulae Entirely within Coq
An AVL calculator