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 37 articles )

Showing results 1 to 20 of 37.
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. Sozeau, Matthieu; Anand, Abhishek; Boulier, Simon; Cohen, Cyril; Forster, Yannick; Kunze, Fabian; Malecha, Gregory; Tabareau, Nicolas; Winterhalter, Théo: The \textscMetaCoqproject (2020)
  7. Michaelson, Greg: Book review of: B. Steffen et al., Mathematical foundations of advanced informatics. Volume 1. Inductive approaches (2019)
  8. Rahli, Vincent; Bickford, Mark; Cohen, Liron; Constable, Robert L.: Bar induction is compatible with constructive type theory (2019)
  9. Schrijvers, Tom; Oliveira, Bruno C. D. S.; Wadler, Philip; Marntirosian, Koar: COCHIS: stable and coherent implicits (2019)
  10. Carette, Jacques; Farmer, William M.; Sharoda, Yasmine: Biform theories: project description (2018)
  11. Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
  12. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  13. Farka, František; Komendantskya, Ekaterina; Hammond, Kevin: Proof-relevant Horn clauses for dependent type inference and term synthesis (2018)
  14. Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
  15. Müller, Dennis; Rabe, Florian; Kohlhase, Michael: Theories as types (2018)
  16. Rahli, Vincent; Bickford, Mark: Validating Brouwer’s continuity principle for numbers using named exceptions (2018)
  17. Rahli, Vincent; Cohen, Liron; Bickford, Mark: A verified theorem prover backend supported by a monotonic library (2018)
  18. Botta, Nicola; Jansson, Patrik; Ionescu, Cezar: Contributions to a computational theory of policy advice and avoidability (2017)
  19. Botta, Nicola; Jansson, Patrik; Ionescu, Cezar; Christiansen, David R.; Brady, Edwin: Sequential decision problems, dependent types and generic solutions (2017)
  20. Dagand, Pierre-Evariste: The essence of ornaments (2017)

1 2 next