User loginNavigation |
Compile and Statically VerifyA 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 | 4894 reads
|
Browse archives
Active forum topics |
Recent comments
13 weeks 2 days ago
13 weeks 3 days ago
13 weeks 3 days ago
35 weeks 4 days ago
39 weeks 6 days ago
41 weeks 3 days ago
41 weeks 3 days ago
44 weeks 1 day ago
48 weeks 5 days ago
48 weeks 5 days ago