by Johan Georg Granström
This project appears to have gone dormant. It will be removed from the list soon unless new activity is noted.
Language using intuitionistic type theory without recursive types.

(Copied from home page:)

The intuitionistic programming language (IPL) is a new open source programming language, implemented in OCaml, combining a very high level of abstraction with compilation to efficient LLVM bytecode.

The semantics of IPL is intuitionistic type theory without recursive types. Type-theoretic constructs, such as lambda abstraction, pairing, and proof objects, are eliminated at compile time using a new algorithm which translates any type-theoretic term of base type, in a context where all variables are of base type, into clean LLVM bytecode.

The features of IPL make it suitable for mission critical software: a very high level of abstraction; type-theoretic verification possibilities; integrated unit testing; compilation to LLVM bytecode; and seamless integration with existing toolchains, including binary interoperability with C and C++.

compile euler(x i32) i32 = block {
  new c = new_i32(0);
  for z in 0..x {
    if srem(z, 3, refl) == 0 || srem(z, 5, refl) == 0 {
      c := c + z;
  yield(get c);
Information updated 08/28/15
View Comments