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.

Itauto: an Extensible Intuitionistic SAT Solver

DEPRECATED, MOVED TO GITHUB https://github.com/MLanguage/mlang

Verifiable online voting system http://www.belenios.org

Sources of the Abstract Categorial Development toolkit.

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).

ProVerif symbolic protocol verifier

Primary library for necro with standard tools (parse, type check, print, and transform Skeletal Semantics)

An OCaml library that provides facilities for memoization and fixed points.

Mapping a tensor to a lower-dimensional tensor, optionally permuting its dimensions. This project strives to generate loop iterating over these structures.

Separation Logic with Characteristic Formulae Entirely within Coq

A generator of debugger for the Skel language for semantics description

DEPRECATED, TRANSFERED TO GITHUB : https://github.com/CatalaLang/catala

An AVL calculator

Javascript formalisation in Skeletal semantics

Resources for course MPRI 2-4 on functional programming and type systems.