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 http://intuitionistic.org for more information.

Advertisements
Post a comment or leave a trackback: Trackback URL.

Trackbacks

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: