Jeremy G. Siek

Mechanized Type Safety for Gradual Information Flow

2021

We model a security-typed language with gradual information flow labels in a proof assistant, demonstrate its potential application to parsing and securing sensitive user input data, present the semantics as a definitional interpreter, and prove …

Big types in little runtime: open-world soundness and collaborative blame for gradual type systems

2017 · ACM SIGPLAN Notices

Gradual typing combines static and dynamic typing in the same language, offering programmers the error detection and strong guarantees of static types and the rapid prototyping and flexible programming idioms of dynamic types. Many gradually …