About: Epigram (programming language)     Goto   Sponge   NotDistinct   Permalink

An Entity of Type : yago:WikicatDependentlyTypedLanguages, within Data Space : dbpedia.org associated with source document(s)

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.

AttributesValues
rdf:type
rdfs:label
  • Epigram (programming language)
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.
sameAs
dct:subject
Wikipage page ID
Wikipage revision ID
Link from a Wikipage to another Wikipage
Link from a Wikipage to an external page
foaf:name
  • Epigram
foaf:isPrimaryTopicOf
prov:wasDerivedFrom
has 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.
designer
influenced
influenced by
latest release date
latest release version
  • 1
developer
  • Unmaintained
license
  • MIT
operating system
paradigm
typing
year
http://purl.org/voc/vrank#hasRank
http://purl.org/li...ics/gold/hypernym
is Link from a Wikipage to another Wikipage of
Faceted Search & Find service v1.17_git39 as of Aug 09 2019


Alternative Linked Data Documents: PivotViewer | iSPARQL | ODE     Content Formats:       RDF       ODATA       Microdata      About   
This material is Open Knowledge   W3C Semantic Web Technology [RDF Data] Valid XHTML + RDFa
OpenLink Virtuoso version 07.20.3235 as of Jun 25 2020, on Linux (x86_64-generic-linux-glibc25), Single-Server Edition (61 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2020 OpenLink Software