Jump to content

Epigram (programming language)

From Wikipedia, the free encyclopedia
This is an old revision of this page, as edited by Txa (talk | contribs) at 08:56, 24 May 2005 (page started). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.
(diff) ← Previous revision | Latest revision (diff) | Newer revision → (diff)

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 programs whose properties can be checked and certified by the compiler. Epigram exploits the proposition as types principle, and is based in Intuitionistic Type Theory.

Epigram was implemented by Conor McBride based on joint work with James McKinna. It's development is continued by the Epigram group in Nottinham, Durham, St Andrews and Royal Holloway in the UK. The current experimental implementation of the Epigram system is freely available from the Epigram webpage together with a user manual, a tutorial and some background material. The system has been used under Linux, Windows and Mac OS.

  • Conor McBride and James McKinna (2004), The view from the left, Journal of Functional Programming
  • Conor McBride (2004), The Epigram Prototype, a nod and two winks
  • Conor McBride (2004), The Epigram Tutorial
  • Thorsten Altenkirch, Conor McBride and James McKinna (2004), Why Dependent Types Matter