Compile and Statically Verify | Lambda the Ultimate

Compile and Statically Verify

A new release of the Albatross compiler and a completely updated language description is available.

The new release has a complete coverage of induction with inductive datatypes and inductively defined sets and relations. The latter one adds great descriptive power to the language.

Furthermore proofs have been simplified by adding syntax support so that proofs written well are also well readable. Syntax support is available for proofs by induction, by contradiction, existential proofs, case split, transitivity proofs.

Download the compiler and the base library.

Read the language description as a gitbook.

Any comments on the language and any suggestions on expected language features are welcome.

By hbrandl at 2016-10-05 15:45 | LtU Forum | previous forum topic | next forum topic | other blogs | 5493 reads

Albatros documentation?

Is there any detailed documentation? I'm curious about this language.

By Ivan V. at Wed, 2016-10-05 19:09 | login or register to post comments

See above. There is a link

See above. There is a link to the language description.

By hbrandl at Wed, 2016-10-05 19:37 | login or register to post comments

Got it,

download as PDF worked :)

By Ivan V. at Thu, 2016-10-06 05:19 | login or register to post comments

"Read" should work as well.

"Read" should work as well.

By hbrandl at Thu, 2016-10-06 05:52 | login or register to post comments

Works,

sorry, i didn't look left for a chapter list. Thanks for the answer.

By Ivan V. at Thu, 2016-10-06 10:28 | login or register to post comments

Self definition

I wonder, what does it take to define Albatross in itself? But maybe it's not relevant...

By Ivan V. at Thu, 2016-10-06 19:22 | login or register to post comments

That is one of the goals.

That is one of the goals. But there is still some work to be done before this is possible.

By hbrandl at Fri, 2016-10-07 07:12 | login or register to post comments