Pangoline

An encoding of polymorphic higher-order logic theories into polymorphic first-order logic theories.

MlPost

A scientific drawing library for Ocaml.

Traces for Alt-Ergo in Coq

A little Coq development to interpret traces produced by the Alt-Ergo theorem prover for congruence closure and linear arithmetic. tgz

Valid XHTML 1.0 StrictPowered by CDucePowered by Caml