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 22 articles , 1 standard article )

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

1 2 next

  1. Affeldt, Reynald; Garrigue, Jacques; Nowak, David; Saikawa, Takafumi: A trustful monad for axiomatic reasoning with probability and nondeterminism (2021)
  2. Farka, František: \textttslepice: towards a verified implementation of type theory in type theory (2021)
  3. Cockx, Jesper; Abel, Andreas: Elaborating dependent (co)pattern matching: no pattern left behind (2020)
  4. Convent, Lukas; Lindley, Sam; McBride, Conor; McLaughlin, Craig: Doo bee doo bee doo (2020)
  5. Genovese, Fabrizio; Gryzlov, Alex; Herold, Jelle; Knispel, Andre; Perone, Marco; Post, Erik; Videla, André: \textttidris-ct: a library to do category theory in Idris (2020)
  6. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  7. Farka, František; Komendantskya, Ekaterina; Hammond, Kevin: Proof-relevant Horn clauses for dependent type inference and term synthesis (2018)
  8. Rahli, Vincent; Bickford, Mark: Validating Brouwer’s continuity principle for numbers using named exceptions (2018)
  9. Botta, Nicola; Jansson, Patrik; Ionescu, Cezar: Contributions to a computational theory of policy advice and avoidability (2017)
  10. Dagand, Pierre-Evariste: The essence of ornaments (2017)
  11. Slama, Franck; Brady, Edwin: Automatically proving equivalence by type-safe reflection (2017)
  12. Ziliani, Beta; Sozeau, Matthieu: A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading (2017)
  13. Bizjak, Aleš; Grathwohl, Hans Bugge; Clouston, Ranald; Møgelberg, Rasmus E.; Birkedal, Lars: Guarded dependent type theory with coinductive types (2016)
  14. Cockx, Jesper; Devriese, Dominique; Piessens, Frank: Eliminating dependent pattern matching without K (2016)
  15. Eisenberg, Richard A.; Weirich, Stephanie; Ahmed, Hamidhasan G.: Visible type application (2016)
  16. McBride, Conor: I got plenty o’ nuttin’ (2016)
  17. Rahli, Vincent: Exercising Nuprl’s open-endedness (2016)
  18. Selsam, Daniel; de Moura, Leonardo: Congruence closure in intensional type theory (2016)
  19. Yang, Yanpeng; Bi, Xuan; Oliveira, Bruno C.d. S.: Unified syntax with iso-types (2016)
  20. Casinghino, Chris; Sjöberg, Vilhelm; Weirich, Stephanie: Combining proofs and programs in a dependently typed language (2014)

1 2 next