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 20150805 18:56  LtU Forum  previous forum topic  next forum topic  other blogs  2362 reads

Browse archivesActive forum topics 
Recent comments
10 hours 45 min ago
21 hours 27 min ago
1 day 5 hours ago
1 day 6 hours ago
1 day 7 hours ago
1 day 9 hours ago
1 day 10 hours ago
1 day 10 hours ago
1 day 15 hours ago
1 day 19 hours ago