Separation logic can handle that—it’s a program logic that subsumes typechecking and typestate, among other things. Your example, in pseudocode: // open :

Separation logic can handle that—it’s a program logic that subsumes typechecking and typestate, among other things. Your example, in pseudocode: // open : string -> file_mode -> (f : file) | f @ read * f @ close f = open "input.dat" Read // close : (f : file) | f @ read * f @ close -> () close f // getline : (f : file) | f @ read -> string | f @ read s = getline f “open” grants the “read” and “close” permissions to “f”; “close” revokes the “read” permission that “getline” requires, causing “getline” not to typecheck.