Mymms Interactive
Demo

Mymms is a project of computer algebra system based upon a proof assistant.

Kernel Interactive
Demo

examples (to copy and paste):
A set of simple testsA simpl matrix implementation using dependent types

A set of simple tests to illustrate overloading and coercion

The first Coq challenge

Some simple encoding (illustration of shadow typing)

Poussin Interactive
Demo

examples (to copy and paste):
A set of simple testsIllustration of automatically generated induction principles

Minima Interactive
Demo

examples (to copy and paste):
A set of simple tests about mutually recursive definitionsThe booleans

The numbers