type ) eventually takes. Full dependent types, as implemented in Epigram, are a powerful abstraction. (Unlike in Dependent ML, the value(s) depended upon may be of any valid type.) A sample of the new formal specification capabilities dependent types bring may be found in The Epigram Tutorial. See also ALF, a proof assistant among the predecessors of Epigram. Further reading External links EPSRC on ALF, lego and related; archived version from 2006 References Academic programming languages Functional languages Dependently typed languages Proof assistants Discontinued programming languages