- document
-
Hinrichsen, Jonas Kastberg (author), Bengtson, Jesper (author), Krebbers, R.J. (author)Message passing is a useful abstraction for implementing concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functional correctness of programs...journal article 2022
- document
-
Frumin, Dan (author), Krebbers, R.J. (author), Birkedal, Lars (author)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 of type checking), but they are inherently restrictive in the kind...conference paper 2021
- document
-
Hinrichsen, Jonas Kastberg (author), Louwrink, Daniƫl (author), Krebbers, R.J. (author), Bengtson, Jesper (author)Session types- A family of type systems for message-passing concurrency-have been subject to many extensions, where each extension comes with a separate proof of type safety. These extensions cannot be readily combined, and their proofs of type safety are generally not machine checked, making their correctness less trustworthy. We overcome...conference paper 2021
- document
-
Hinrichsen, J.K. (author), Bengtson, Jesper (author), Krebbers, R.J. (author)Message passing is a useful abstraction to implement concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functional correctness of programs that...journal article 2020
- document
-
Giarrusso, P.G. (author), Stefanesco, Leo (author), Timany, Amin (author), Birkedal, Lars (author), Krebbers, R.J. (author)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 in practice. To address some of these problems, we use a semantics...journal article 2020