Idris, a general-purpose dependently typed programming language: Design and implementation
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 Fields
Computer science
Biology
Artificial intelligence
Ecology
Programming language
World Wide Web
Type (biology)
Semantics (computer science)
Syntax
Unification
USable
Programming paradigm
Inductive programming
Type theory
Programming domain
Functional logic programming
Lambda calculus
Abstract syntax
First-generation programming language
High-level programming language
Programming language specification
Very high-level programming language
Dependent type
Language primitive
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