Explore projects

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 http://www.belenios.org

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

Javascript formalisation in Skeletal semantics

An AVL calculator