Idris, a general-purpose dependently typed programming language: Design and implementation

Volume: 23, Issue: 5, Pages: 552 - 593
Published: Sep 1, 2013
Abstract
Many components of a dependently typed programming language are by now well understood, for example, the underlying type theory, type checking, unification and evaluation. How to combine these components into a realistic and usable high-level language is, however, folklore, discovered anew by successive language implementors. In this paper, I describe the implementation of Idris , a new dependently typed functional programming language. Idris is...
Paper Details
Title
Idris, a general-purpose dependently typed programming language: Design and implementation
DOI
Published Date
Sep 1, 2013
Journal
Volume
23
Issue
5
Pages
552 - 593
Citation Distributions