Epigram is the name of a functional programming language with dependent types and of the IDE usually packaged with it. 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.

PropertyValue
dbpprop:abstract
  • Epigram is the name of a functional programming language with dependent types and of the IDE usually packaged with it. 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.
dbpprop:designer
  • Conor McBride and James McKinna
dbpprop:developer
  • the Epigram group
dbpprop:hasPhotoCollection
dbpprop:influencedBy
dbpprop:latestReleaseDate
dbpprop:latestReleaseVersion
dbpprop:license
  • Unspecified
dbpprop:name
  • Epigram
dbpprop:operatingSystem
dbpprop:paradigm
dbpprop:reference
dbpprop:typing
dbpprop:website
dbpprop:wikiPageUsesTemplate
dbpprop:year
  • 2004 (xsd:integer)
rdfs:comment
  • Epigram is the name of a functional programming language with dependent types and of the IDE usually packaged with it. 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.
rdfs:label
  • Epigram (programming language)
owl:sameAs
skos:subject
foaf:homepage
foaf:page
is dbpprop:disambiguates of
is dbpprop:influenced of
is dbpprop:influencedBy of
is dbpprop:redirect of