The Epigram prototype was implemented by Conor McBride based on joint work with James McKinna.
Its development is continued by the Epigram group in Nottingham, Durham, St Andrews, and Royal Holloway, University of London in the United Kingdom (UK).
The current experimental implementation of the Epigram system is freely available together with a user manual, a tutorial and some background material.
It is currently unmaintained, and version 2, which was intended to implement Observational Type Theory, was never officially released but exists in GitHub.
Epigram uses a two-dimensional, natural deduction style syntax, with versions in LaTeX and ASCII.
If nothing is on the top, then the bottom statement is always true: "zero is of type Nat (in all cases)."
Full dependent types, as implemented in Epigram, are a powerful abstraction.
A sample of the new formal specification capabilities dependent types bring may be found in The Epigram Tutorial.