User loginNavigation 
An experiment: Refined types  a better type system for more secure softwareHi, fellow language enthusiasts! I recently finished an experimental, fairly simple, OCaml implementation of refined types. Refined types support logical predicates in function parameters and return types, for example: / : (int, i : int if i != 0) > int random1toN : (N : int if N >= 1) > (i : int if 1 <= i and i <= N) length : forall[t] (a : array[t]) > (l : int if l >= 0) get : forall[t] (a : array[t], i : int if i >= 0 and i < length(a)) > t
Refined types are checked by an external automatic theorem prover (Z3), and can prevent many common software errors, such as division by zero and outofbounds array access. Given correct refined types on functions Read more about it (and see the code) here! Any comments are welcome. By Tom PrimoÅ¾iÄ at 20140529 11:45  LtU Forum  previous forum topic  next forum topic  other blogs  1107 reads

Browse archives
Active forum topics 
Recent comments
13 hours 16 min ago
1 day 14 hours ago
1 day 18 hours ago
1 day 18 hours ago
1 day 19 hours ago
1 day 23 hours ago
2 days 30 min ago
2 days 4 hours ago
2 days 10 hours ago
2 days 15 hours ago