OCaml Program
Checking:
Static
Dynamic
Hybrid
 
contract ack = {m | true} -> {n | true} -> {z | z > n} let rec ack m n = if m = 0 then n + 1 else if m > 0 && n = 0 then ack (m-1) 1 else ack (m-1) (ack m (n-1)) contract f = {x | true} -> {y | x 1 <= 0 || y 1 >= 0} -> {z | true } let f (x: int -> int) (y : int -> int) = 1 let g (n : int) = let h x y = x in f (h n) (h n)