OCaml implementation of a typer for System FOmega (MPRI 2.4 project).
Why3 proofs of functions using dynamic programming (MPRI 2.36.1 project).