Epigram is a functional programming language with dependent types. Epigram also refers to the 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 propositions as types principle, and is based on intuitionistic type theory.

Property Value
dbo:abstract
  • Epigram is a functional programming language with dependent types. Epigram also refers to the 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 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 in the 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 Mac OS X. It is currently unmaintained, and version 2, which was intended to implement Observational Type Theory, was never officially released, however there exists a GitHub mirror, last updated in 2012. (en)
dbo:designer
dbo:influenced
dbo:influencedBy
dbo:latestReleaseDate
  • 2006-10-11 (xsd:date)
dbo:latestReleaseVersion
  • 1
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 1933143 (xsd:integer)
dbo:wikiPageRevisionID
  • 737824254 (xsd:integer)
dbp:developer
  • Unmaintained
dbp:license
  • MIT
dbp:operatingSystem
dbp:paradigm
dbp:typing
dbp:year
  • 2004 (xsd:integer)
dct:subject
http://purl.org/linguistics/gold/hypernym
rdf:type
rdfs:comment
  • Epigram is a functional programming language with dependent types. Epigram also refers to the 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 propositions as types principle, and is based on intuitionistic type theory. (en)
rdfs:label
  • Epigram (programming language) (en)
owl:sameAs
prov:wasDerivedFrom
foaf:isPrimaryTopicOf
foaf:name
  • Epigram (en)
is dbo:influenced of
is dbo:influencedBy of
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is foaf:primaryTopic of