Arnaud Spiwack's homepage

Version & licenses
Creative Commons License

Personal Information

Post-doc in Computing Sciences

Cri, Mines ParisTech



Cellphone :

+33 6 72 02 68 03


Here are the software I contribute to:

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

I have more experimental things going on:

  • Cosa a Coq implementation of a Shape abstract domain. Its target language is Compcert C (more precisely the C minor intermediate language). Cosa is meant to be used together with the abstract domains of the Verasco project.
  • My github address may be a good place to get fresh news.