Irdis swMATH ID: 9690 Software Authors: Description: 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 Homepage: http://www.idris-lang.org/ Related Software: Idris; Coq; Agda; Haskell; GitHub; Lean; Nuprl; F*; Epigram; ELPI; Automath; Beluga; Eff; Equations; Coq/SSReflect; ML; z3; Mtac; cubicaltt; Ynot Cited in: 22 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Idris, a general-purpose dependently typed programming language: design and implementation. Zbl 1295.68059Brady, Edwin 2013 all top 5 Cited by 52 Authors 2 Brady, Edwin C. 2 Cockx, Jesper 2 Farka, František 2 McBride, Conor Thomas 2 Rahli, Vincent 2 Weirich, Stephanie 1 Abel, Andreas M. 1 Affeldt, Reynald 1 Ahmed, Hamidhasan G. 1 Bi, Xuan 1 Bickford, Mark 1 Birkedal, Lars 1 Bizjak, Aleš 1 Botta, Nicola 1 Casinghino, Chris 1 Clouston, Ranald A. 1 Convent, Lukas 1 Czajka, Łukasz 1 Dagand, Pierre-Evariste 1 de Moura, Leonardo 1 Devriese, Dominique 1 Eisenberg, Richard A. 1 Garrigue, Jacques 1 Genovese, Fabrizio 1 Grathwohl, Hans Bugge 1 Gryzlov, Alex 1 Hammond, Kevin 1 Herold, Jelle 1 Ionescu, Cezar 1 Jansson, Patrik 1 Kaliszyk, Cezary 1 Knispel, Andre 1 Komendantskya, Ekaterina 1 Lindley, Sam 1 Liu, Yu David 1 McLaughlin, Craig A. 1 Møgelberg, Rasmus Ejlers 1 Nowak, David E. 1 Oliveira, Bruno C.d. S. 1 Perone, Marco 1 Piessens, Frank 1 Post, Erik 1 Saikawa, Takafumi 1 Selsam, Daniel 1 Sjöberg, Vilhelm 1 Skalka, Christian 1 Slama, Franck 1 Smith, Scott F. 1 Sozeau, Matthieu 1 Videla, André 1 Yang, Yanpeng 1 Ziliani, Beta Cited in 5 Serials 8 Journal of Functional Programming 1 Journal of Automated Reasoning 1 MSCS. Mathematical Structures in Computer Science 1 Higher-Order and Symbolic Computation 1 Theory and Practice of Logic Programming Cited in 5 Fields 22 Computer science (68-XX) 11 Mathematical logic and foundations (03-XX) 1 Category theory; homological algebra (18-XX) 1 Algebraic topology (55-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year