Irdis: a language with dependent types. Idris is a general purpose pure functional programming language with dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program’s behaviour can be specified precisely in the type. It is compiled, with eager evaluation. Its features are influenced by Haskell and ML, and include: Full dependent types with dependent pattern matching; where clauses, with rule, simple case expressions, pattern matching let and lambda bindings; Dependent records with projection and update; Type classes; Monad comprehensions; Syntactic conveniences for lists, tuples, dependent pairs; do notation and idiom brackets; Indentation significant syntax; Extensible syntax; Tactic based theorem proving (influenced by Coq); Cumulative universes; Totality checking; Simple foreign function interface (to C); Hugs style interactive environment
Keywords for this software
References in zbMATH (referenced in 3 articles , 1 standard article )
Showing results 1 to 3 of 3.
- Casinghino, Chris; Sjöberg, Vilhelm; Weirich, Stephanie: Combining proofs and programs in a dependently typed language (2014)
- Brady, Edwin: Idris, a general-purpose dependently typed programming language: design and implementation (2013)
- Liu, Yu David; Skalka, Christian; Smith, Scott F.: Type-specialized staged programming with process separation (2011)