Epigram

Epigram is a functional programming language with dependent types, and the integrated development environment (IDE) usually packaged with the language. 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 Curry–Howard correspondence, also termed the propositions as types principle, and is based on intuitionistic type theory. Wikipedia

Created Year: 2004
Designed by: Conor McBride

Wikidata: Q5382927

Influenced: Agda • Idris

Programming paradigms: functional programming

Language types: dependently typed programming language