Idris

Purely functional programming language

2007Appeared

static typing, dependent typing, linear typing, uniqueness typingType system

1.3.3Latest version

Facts

Appeared: 2007
Type system: static typing, dependent typing, linear typing, uniqueness typing
Latest version: 1.3.3 (May 23, 2020)
Kind: proof assistant, purely functional programming language, dependently typed programming language
Paradigms: total functional programming, functional programming, purely functional programming
Designed by: Edwin Brady
Influenced by: Rocq prover, Agda, Haskell, Clean, Epigram
Implemented in: Haskell
File extensions: .idr .lidr
Licence: BSD licenses
Operating system: cross-platform
Influences listed: 5