Logiciels

Affichage de fractales en Caml

Un exemple de programmation des widgets en Caml à l'aide de la librairie LablGTK2.

Démonstration des algorithmes de tris

Deux programmes écrits pour la Fête de la Science (en 2005) pour illustrer les principaux algorithmes de tris: le programme de démonstration (demo) et la course aux tris (race).

Quelques antiquités...

• Mldvi: un afficheur de fichiers DVI écrit en Objective Caml.
  Télécharger les sources.
• Htree: une librairie générique (écrite en Objective Caml) pour afficher des arbres à l'aide de la géométrie hyperbolique.
  Télécharger les sources.
• Ccmodel: une implémentation (en Objective Caml) du modèle finitiste proof-irrelevant du Calcul des Constructions.
  (ou: Comment faire vérifier par sa machine la cohérence logique du Calcul des Constructions en moins d'un dixième de seconde)
  Télécharger les sources.

IZF Dans Coq

• Pour Coq V 7.4: Télécharger les sources
• Pour Coq V 8.0: À venir...