Block or report user
  • Joined on Dec 5, 2010
  • C++ Updated Dec 6, 2016
  • An implementation of the Calculus of Inductive Construction

    OCaml Updated Jul 15, 2016
  • building a minimal certified library using frama-c

    C Updated Jun 29, 2016
  • why3 projects: combinatorial and sequential logic elements (from nand2tetris), some redefined theories (set, map), seplog theories

    1 Updated Jun 21, 2016
  • a little lib for holzero

    OCaml Updated Mar 30, 2015
  • Simple shallow embedding of a HOL logic, LCF style in coq

    Coq Updated Apr 3, 2013
  • A non-copying garbage collector (from ICFP2011)

    C 1 1 Updated Jan 29, 2013
  • personal version of some opam packages

    Updated Jan 25, 2013
  • several libraries for python development

    Python Updated Jan 11, 2013
  • attempt to build a tool for vdm using why3 as a backend for proof obligation

    OCaml 1 Updated Oct 3, 2012
  • A API for Interactive Brokers TWS in OCaml

    OCaml 1 Updated Aug 18, 2012
  • several old dev

    OCaml Updated Apr 23, 2012
  • another repo of old dev

    OCaml 1 2 Updated Nov 18, 2011