User loginNavigation |
Albatross has grown two mighty wings: Induction and RecursionThe version 0.2 of the Albatross programming language / proof assistant has been released. It has some new features. The most important ones are induction and recursion which come together with inductive data types. With these two features Albatross approaches the expressiveness of Coq. It is possible to declare lists, trees, define recursive functions on them and prove properties of these functions. The documentation contains examples of lists, binary trees and a verified insertion sort algorithm. All the examples a fully verifiable with the version 0.2 of the Albatross compiler (download here). Some of the key features of Albatross:
By hbrandl at 2015-08-05 18:56 | LtU Forum | previous forum topic | next forum topic | other blogs | 2898 reads
|
Browse archives
Active forum topics
|
Recent comments
14 weeks 6 days ago
19 weeks 1 day ago
20 weeks 5 days ago
20 weeks 5 days ago
23 weeks 3 days ago
28 weeks 13 hours ago
28 weeks 15 hours ago
28 weeks 3 days ago
28 weeks 3 days ago
31 weeks 2 days ago