×

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

Citations by Year