Abstract
The overall topic of this thesis is modular reasoning for higher-order languages with state. The thesis consists of four mostly independent chapters that each deal with a different aspect of reasoning about higher-order languages with state. The unifying theme throughout all four chapters is higher-order separation logic.
The first chapter presents a higher-order separation logic for a higher-order subset of C#. One of the interesting issues that arises when reasoning about higher-order code in an imperative language, is the combination of mutable variables and variable capture. In C#, anonymous methods can have externally observable state effects on both the heap and the stack, through captured variables. However, despite state effects on the stack it is still not possible to alias stack variables in this subset of C#. We exploit this to define a logic that allows us to treat captured variables as resources, without breaking Hoare’s assignment rule.
The second chapter is concerned with the problem of reasoning about sharing in a higher-order concurrent language. When specifying shared mutable data structures, the appropriate specification depends on how clients intend to share instances of the data structures. To ensure modular reasoning, we need a generic specification that clients can refine with their desired sharing discipline. In the second chapter we present a new higher-order separation logic and a new style of specification that clients can refine with a sharing discipline of their choice.
The third chapter of the thesis is a case study of the C# joins library. What makes this library interesting as a case study is that it combines a lot of advanced features (higher-order code with effects, concurrency, recursion through the store, shared mutable state, and fine-grained synchronization) to implement a high-level interface for defining synchronization primitives in C#. Due to the declarative nature of this interface, synchronization primitives implemented using the joins library admit fairly simple informal correctness arguments. We present an abstract specification of the joins library that extends these informal correctness arguments to fully formal partial correctness proofs. Using the logic developed in the second chapter, we verify a lock-based implementation of the joins library against this abstract joins specification.
The last chapter is concerned with the problem of extending a pure dependent type theory with effects. The motivation is to take advantage of an existing implementation of a pure dependent type theory to obtain an implementation of a formal proof system based on higher-order separation logic. In particular, we extend the Calculus of Inductive Constructions with monadically encapsulated stateful and potentially non-terminating computations. The monadic computation types are indexed with pre- and postconditions and act as partial correctness specifications. The type theory supports local reasoning about state through a notion of disjointness strongly inspired by separation logic.
The first chapter presents a higher-order separation logic for a higher-order subset of C#. One of the interesting issues that arises when reasoning about higher-order code in an imperative language, is the combination of mutable variables and variable capture. In C#, anonymous methods can have externally observable state effects on both the heap and the stack, through captured variables. However, despite state effects on the stack it is still not possible to alias stack variables in this subset of C#. We exploit this to define a logic that allows us to treat captured variables as resources, without breaking Hoare’s assignment rule.
The second chapter is concerned with the problem of reasoning about sharing in a higher-order concurrent language. When specifying shared mutable data structures, the appropriate specification depends on how clients intend to share instances of the data structures. To ensure modular reasoning, we need a generic specification that clients can refine with their desired sharing discipline. In the second chapter we present a new higher-order separation logic and a new style of specification that clients can refine with a sharing discipline of their choice.
The third chapter of the thesis is a case study of the C# joins library. What makes this library interesting as a case study is that it combines a lot of advanced features (higher-order code with effects, concurrency, recursion through the store, shared mutable state, and fine-grained synchronization) to implement a high-level interface for defining synchronization primitives in C#. Due to the declarative nature of this interface, synchronization primitives implemented using the joins library admit fairly simple informal correctness arguments. We present an abstract specification of the joins library that extends these informal correctness arguments to fully formal partial correctness proofs. Using the logic developed in the second chapter, we verify a lock-based implementation of the joins library against this abstract joins specification.
The last chapter is concerned with the problem of extending a pure dependent type theory with effects. The motivation is to take advantage of an existing implementation of a pure dependent type theory to obtain an implementation of a formal proof system based on higher-order separation logic. In particular, we extend the Calculus of Inductive Constructions with monadically encapsulated stateful and potentially non-terminating computations. The monadic computation types are indexed with pre- and postconditions and act as partial correctness specifications. The type theory supports local reasoning about state through a notion of disjointness strongly inspired by separation logic.
| Originalsprog | Engelsk |
|---|
| Forlag | IT-Universitetet i København |
|---|---|
| Antal sider | 301 |
| ISBN (Trykt) | 978-87-7949-281-3 |
| Status | Udgivet - 2013 |
| Navn | ITU-DS |
|---|---|
| Nummer | 86 |
| ISSN | 1602-3536 |