LFCS Seminar: 14 April 2020 - Arjen Rouvoet

Title: Intrinsically-typed interpretation of linear references using a shallow embedding of separation logic

Abstract:

By directly computing on an encoding of well-typed terms we can get language interpreters that are type-safe by construction. Previous work has shown that intrinsically-typed interpreters can sometimes avoid manual proof work. Moreover, the types can actually help us to implement a correct interpreter in one go. Unfortunately, proving type-safety of languages with linear references requires additional reasoning about resources to show that references are indeed never duplicated, nor discarded.  We show that we can hide the invariant and most of the proof work by systematically abstracting over the resource using a shallow embedding of separation logic in Agda. Linear references can then be interpreted nicely in a linear state monad that balances resource supply and demand under the hood

Affiliation:

Technical University Delft