Peter Thiemann

LJGS: Gradual Security Types for Object-Oriented Languages

2016 · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics)

LJGS is a lightweight Java core calculus with a gradual security type system. The calculus guarantees secure information flow for sequential, class-based, typed object-oriented programming with mutable objects and virtual method calls. An LJGS program …

Intrinsically Typed Sessions with Callbacks (Functional Pearl)

2023 · Proceedings of the ACM on Programming Languages

All formalizations of session types rely on linear types for soundness as session-typed communication channels must change their type at every operation. Embedded language implementations of session types follow suit. They either rely on clever …

Law and Order for Typestate with Borrowing

2024 · arXiv (Cornell University)

Typestate systems are notoriously complex as they require sophisticated machinery for tracking aliasing. We propose a new, transition-oriented foundation for typestate in the setting of impure functional programming. Our approach relies on ordered types for …