Idris
Topic history | v1 (current) | created by jjones
Details
Idris
see v1 | created by jjones | Add topic "Idris"
- Title
- Idris
- Description
- Idris is a purely-functional programming language with dependent types, optional lazy evaluation, and features such as a totality checker. Idris may be used as a proof assistant, but it is designed to be a general-purpose programming language similar to Haskell. The Idris type system is similar to Agda's, and proofs are similar to Coq's, including tactics (theorem proving functions/procedures) via elaborator reflection. Compared to Agda and Coq, Idris prioritizes management of side effects and support for embedded domain-specific languages. Idris compiles to C (relying on a custom copying garbage collector using Cheney's algorithm) and JavaScript (both browser- and Node.js-based). There are third-party code generators for other platforms, including JVM, CIL, and LLVM.Idris is named after a singing dragon from the 1970s UK children's television program Ivor the Engine.
- Link
- https://en.wikipedia.org/?curid=39035048
resources
treated in Type-driven development with Idris
has official A Crash Course in Idris 2
treated in Idris 2: Quantitative Type Theory in Action
authors
This topic has no history of related authors.