Arnaud Spiwack's homepage

Version & licenses
Creative Commons License

Personal Information

Director, Research

Modus Create



Cellphone :

+33 6 72 02 68 03


Here are some software I contribute to:

I have more experimental things going on:

Here are some software I used to contribute to in the past:

  • Coq the most successful implementation of a dependent type theory. Serves both as a programming language and a proof assistant. Coq is a central object in my research.
  • Melt an Ocaml library and preprocessor to generate Latex documents. It saved me countless hours and immense frustration. It is still a little too much tailored to the needs of the few contributors, and development is going slowly. But you may still consider using it.