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

References in zbMATH (referenced in 19 articles , 1 standard article )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Cockx, Jesper; Abel, Andreas: Elaborating dependent (co)pattern matching: no pattern left behind (2020)
  2. Convent, Lukas; Lindley, Sam; McBride, Conor; McLaughlin, Craig: Doo bee doo bee doo (2020)
  3. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  4. Farka, František; Komendantskya, Ekaterina; Hammond, Kevin: Proof-relevant Horn clauses for dependent type inference and term synthesis (2018)
  5. Rahli, Vincent; Bickford, Mark: Validating Brouwer’s continuity principle for numbers using named exceptions (2018)
  6. Botta, Nicola; Jansson, Patrik; Ionescu, Cezar: Contributions to a computational theory of policy advice and avoidability (2017)
  7. Dagand, Pierre-Evariste: The essence of ornaments (2017)
  8. Slama, Franck; Brady, Edwin: Automatically proving equivalence by type-safe reflection (2017)
  9. Ziliani, Beta; Sozeau, Matthieu: A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading (2017)
  10. Bizjak, Aleš; Grathwohl, Hans Bugge; Clouston, Ranald; Møgelberg, Rasmus E.; Birkedal, Lars: Guarded dependent type theory with coinductive types (2016)
  11. Cockx, Jesper; Devriese, Dominique; Piessens, Frank: Eliminating dependent pattern matching without K (2016)
  12. Eisenberg, Richard A.; Weirich, Stephanie; Ahmed, Hamidhasan G.: Visible type application (2016)
  13. McBride, Conor: I got plenty o’ nuttin’ (2016)
  14. Rahli, Vincent: Exercising Nuprl’s open-endedness (2016)
  15. Selsam, Daniel; de Moura, Leonardo: Congruence closure in intensional type theory (2016)
  16. Yang, Yanpeng; Bi, Xuan; Oliveira, Bruno C.d. S.: Unified syntax with iso-types (2016)
  17. Casinghino, Chris; Sjöberg, Vilhelm; Weirich, Stephanie: Combining proofs and programs in a dependently typed language (2014)
  18. Brady, Edwin: Idris, a general-purpose dependently typed programming language: design and implementation (2013)
  19. Liu, Yu David; Skalka, Christian; Smith, Scott F.: Type-specialized staged programming with process separation (2011)