Idris swMATH ID: 20011 Software Authors: Edwin Brady Description: 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. Homepage: https://www.idris-lang.org/ Related Software: Coq; Agda; Irdis; Haskell; Lean; Nuprl; Mtac; GitHub; HOL Light; ML; cubicaltt; Template-Coq; MetaCoq; HOL; F*; Rust; OEuf; CakeML; CertiCoq; ELPI Cited in: 38 Publications all top 5 Cited by 87 Authors 5 Brady, Edwin C. 4 Rahli, Vincent 3 Bickford, Mark 2 Abel, Andreas M. 2 Botta, Nicola 2 Christiansen, David R. 2 Cockx, Jesper 2 Cohen, Liron 2 Farka, František 2 Farmer, William M. 2 Ionescu, Cezar 2 Jansson, Patrik 2 McBride, Conor Thomas 2 Oliveira, Bruno C.d. S. 2 Sozeau, Matthieu 1 Affeldt, Reynald 1 Ahmed, Hamidhasan G. 1 Aldrich, Jonathan 1 Anand, Abhishek 1 Annenkov, Danil 1 Berger, Ulrich 1 Bi, Xuan 1 Birkedal, Lars 1 Bizjak, Aleš 1 Boulier, Simon 1 Carette, Jacques 1 Cauderlier, Raphaël 1 Clouston, Ranald A. 1 Cohen, Cyril 1 Constable, Robert Lee 1 Convent, Lukas 1 Czajka, Łukasz 1 Dagand, Pierre-Evariste 1 de Haas, W. Bas 1 de Moura, Leonardo 1 Devriese, Dominique 1 Dybjer, Peter 1 Eisenberg, Richard A. 1 Forster, Yannick 1 Garrigue, Jacques 1 Genovese, Fabrizio 1 Grathwohl, Hans Bugge 1 Gryzlov, Alex 1 Hammer, Matthew A. 1 Hammond, Kevin 1 Herold, Jelle 1 Kaliszyk, Cezary 1 Knispel, Andre 1 Kohlhase, Michael 1 Komendantskya, Ekaterina 1 Kunze, Fabian 1 Lawrence, Andrew 1 Lindley, Sam 1 Magalhães, José Pedro 1 Malecha, Gregory 1 Marntirosian, Koar 1 McLaughlin, Craig A. 1 Michaelson, Greg 1 Milo, Mikkel 1 Møgelberg, Rasmus Ejlers 1 Mörtberg, Anders 1 Müller, Dennis 1 Nielsen, Jakob Botsch 1 Nordvall Forsberg, Fredrik 1 Nowak, David E. 1 Omar, Cyrus 1 Perone, Marco 1 Piessens, Frank 1 Post, Erik 1 Rabe, Florian 1 Saikawa, Takafumi 1 Schrijvers, Tom 1 Seisenberger, Monika 1 Selsam, Daniel 1 Sharoda, Yasmine 1 Slama, Franck 1 Spitters, Bas 1 Swierstra, Wouter 1 Tabareau, Nicolas 1 Vezzosi, Andrea 1 Videla, André 1 Voysey, Ian 1 Wadler, Philip Lee 1 Weirich, Stephanie 1 Winterhalter, Théo 1 Yang, Yanpeng 1 Ziliani, Beta all top 5 Cited in 8 Serials 12 Journal of Functional Programming 2 Journal of Automated Reasoning 2 Logical Methods in Computer Science 1 Information and Computation 1 Formal Aspects of Computing 1 MSCS. Mathematical Structures in Computer Science 1 Journal of the ACM 1 Theory and Practice of Logic Programming all top 5 Cited in 7 Fields 38 Computer science (68-XX) 15 Mathematical logic and foundations (03-XX) 3 General and overarching topics; collections (00-XX) 1 Category theory; homological algebra (18-XX) 1 Algebraic topology (55-XX) 1 Operations research, mathematical programming (90-XX) 1 Game theory, economics, finance, and other social and behavioral sciences (91-XX) Citations by Year