Epigram is a functional programming language with dependent types and at the same time an interactive program development system. Epigram s type system is strong enough to express program specifications, the goal is to support a smooth transition from ordinary programming to integrated programs and proofs whose correctness can be checked and certified by the Compiler. Epigram exploits the propositions as types principle, and is based on Intuitionistic Type Theory.

The Epigram prototype was implemented by Conor McBride based on joint work with James McKinna. Its development is continued by the Epigram group in .

= External Links =