Monthly Archives: October 2013

A new kind of programming language

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.

See for more information.


Heidelberg Laureate Forum

I participated in the 1st Heidelberg Laureate Forum last week and contributed a couple of blog posts to the official HLF blog. You can find them here: