Jakarta

(Outil de validation de vérificateurs de bytecode)

• Auteurs : P. Courtieu, G. Dufay, J. Forest, S. Melo de Sousa
• Language de développement : OCAML (http://caml.inria.fr)
• Taille : 80 000 lignes de code

Coq

(Assistant à la preuve)

• Language de développement : OCAML (http://caml.inria.fr)
• Taille : 140 000 lignes de code (dont environ 10 000 pour les fonctions récursives non structurelles)
• Licence LGPL.

CiME

(Outil de récriture)

• Auteurs : E. Contejean, P. Courtieu, J. Forest, C. Marché, B. Monate, O. Pons, X. Urbain.
• Language de développement : OCAML (http://caml.inria.fr)
• Taille : 80 000 lignes de code (dont environ 10 000 pour la certification)
• Licence CeCill-C.

• Publications

This document was translated from L^AT_EX by H^EV^EA.