Lars Birkedal
8 records found
1
Authored
Non-interference is a program property that ensures the absence of information leaks. In the context of programming languages, there exist two common approaches for establishing non-interference: type systems and program logics. Type systems provide strong automation (by means ...
Scala step-by-step
Soundness for DOT with step-indexed logical relations in Iris
The metatheory of Scala's core type system - the Dependent Object Types (DOT) calculus - is hard to extend, like the metatheory of other type systems combining subtyping and dependent types. Soundness of important Scala features therefore remains an open problem in theory and ...
Iron
Managing obligations in higher-order concurrent separation logic
Iris from the ground up
A modular foundation for higher-order concurrent separation logic
ReLoC
A Mechanised Relational Logic for Fine-Grained Concurrency
Concurrent separation logics (CSLs) have come of age, and with age they have accumulated a great deal of complexity. Previous work on the Iris logic attempted to reduce the complex logical mechanisms of modern CSLs to two orthogonal concepts: partial commutative monoids (PCMs) ...