Epigram (programming language)

This article has multiple issues. Please help improve it or discuss these issues on the talk page. (Learn how and when to remove these messages) The topic of this article may not meet Wikipedia's general notability guideline. Please help to demonstrate the notability of the topic by citing reliable secondary sources that are independent of the topic and provide significant coverage of it beyond a mere trivial mention. If notability cannot be shown, the article is likely to be merged, redirected, or deleted. Find sources: "Epigram" programming language – news · newspapers · books · scholar · JSTOR (August 2019) (Learn how and when to remove this message) This article includes a list of references, related reading, or external links, but its sources remain unclear because it lacks inline citations. Please help improve this article by introducing more precise citations. (August 2019) (Learn how and when to remove this message) This article relies largely or entirely on a single source. Relevant discussion may be found on the talk page. Please help improve this article by introducing citations to additional sources. Find sources: "Epigram" programming language – news · newspapers · books · scholar · JSTOR (February 2023) This article relies excessively on references to primary sources. Please improve this article by adding secondary or tertiary sources. Find sources: "Epigram" programming language – news · newspapers · books · scholar · JSTOR (February 2023) (Learn how and when to remove this message) (Learn how and when to remove this message)

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.

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. The system has been used under Linux, Windows, and macOS.

It is currently unmaintained, and version 2, which was intended to implement Observational Type Theory, was never officially released but exists in GitHub.