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; Simple foreign function interface (to C); Compiler-supported interactive editing: the compiler helps you write code using the types; where clauses, with rule, simple case expressions, pattern matching let and lambda bindings; Dependent records with projection and update; Interfaces (similar to type classes in Haskell); Type-driven overloading resolution; do notation and idiom brackets; Indentation significant syntax; Extensible syntax; Cumulative universes; Totality checking; Hugs style interactive environment.

References in zbMATH (referenced in 33 articles )

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

1 2 next

  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. Michaelson, Greg: Book review of: B. Steffen et al., Mathematical foundations of advanced informatics. Volume 1. Inductive approaches (2019)
  4. Rahli, Vincent; Bickford, Mark; Cohen, Liron; Constable, Robert L.: Bar induction is compatible with constructive type theory (2019)
  5. Schrijvers, Tom; Oliveira, Bruno C. D. S.; Wadler, Philip; Marntirosian, Koar: COCHIS: stable and coherent implicits (2019)
  6. Carette, Jacques; Farmer, William M.; Sharoda, Yasmine: Biform theories: project description (2018)
  7. Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
  8. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  9. Farka, František; Komendantskya, Ekaterina; Hammond, Kevin: Proof-relevant Horn clauses for dependent type inference and term synthesis (2018)
  10. Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
  11. Müller, Dennis; Rabe, Florian; Kohlhase, Michael: Theories as types (2018)
  12. Rahli, Vincent; Bickford, Mark: Validating Brouwer’s continuity principle for numbers using named exceptions (2018)
  13. Rahli, Vincent; Cohen, Liron; Bickford, Mark: A verified theorem prover backend supported by a monotonic library (2018)
  14. Botta, Nicola; Jansson, Patrik; Ionescu, Cezar: Contributions to a computational theory of policy advice and avoidability (2017)
  15. Botta, Nicola; Jansson, Patrik; Ionescu, Cezar; Christiansen, David R.; Brady, Edwin: Sequential decision problems, dependent types and generic solutions (2017)
  16. Dagand, Pierre-Evariste: The essence of ornaments (2017)
  17. Omar, Cyrus; Voysey, Ian; Hilton, Michael; Aldrich, Jonathan; Hammer, Matthew A.: Hazelnut: a bidirectionally typed structure editor calculus (2017)
  18. Slama, Franck; Brady, Edwin: Automatically proving equivalence by type-safe reflection (2017)
  19. Swierstra, Wouter (ed.); Dybjer, Peter (ed.): Editorial: Special issue on programming with dependent types (2017)
  20. Ziliani, Beta; Sozeau, Matthieu: A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading (2017)

1 2 next