Examplesmechnican checks with Coq or Runtime Verification's K; strong type system with noninterference guarantee