Output details

Idris, a General Purpose Dependently Typed Programming Language : Design and Implementation

<08>This paper presents the results of four years work in designing and implementing a language, Idris, capable of general purpose systems programming, and program verification, and which has been the basis of several publications. It gives the formal semantics of a minimal, independently verifiable core language. Most importantly, it gives an original method for translating Idris (or any high level language) into that core, by building proofs and exploiting a unification procedure. This method is extensible and composable and the paper demonstrates this by showing how new language features can be added easily, with a small set of operations.