Poussin Interactive Demo


The 1st version of poussin (the second will be embedded in a bigger project): savannah page


Local archive: poussin.tar.gz

examples (to copy and paste):

multiplication of matrices (using dependant type)
proof of the associativity of addition over natural numbers
proof of the reverse induction principle of list
the first coq-challenge in poussin