CentralNotice Idris (programming language) From Wikipedia, the free encyclopedia Jump to: navigation , search Idris Paradigm Functional Designed by Edwin Brady Stable release 0.9.16 / January 15, 2015 ( 2015-01-15 ) OS Cross-platform License BSD-3 Filename extensions .idr, .lidr Website Idris website Influenced by Agda , Coq , [ 1 ] Epigram , Haskell , [ 1 ] ML [ 1 ] Idris is a general-purpose pure functional programming language with dependent types . The type system is similar to the one used by Agda . The language supports interactive theorem-proving comparable to Coq , including tactics, while the focus remains on general-purpose programming even before theorem-proving. Other goals of Idris are "sufficient" performance, easy management of side-effects and support for implementing embedded domain specific languages . ...