|START Conference Manager|
We exhibit a type-directed, type-preserving and meaning-preserving translation of this imperative calculus into a pure calculus. Like the monadic translation, this is a store-passing translation. Here, however, the store is partitioned into multiple fragments, which are threaded through a computation only if they are relevant to it. Furthermore, the decomposition of the store into fragments can evolve dynamically to reflect ownership transfers.
The translation offers deep insight about the inner workings and soundness of the type system. If coupled with a semantic model of its target calculus, it leads to a semantic model of its imperative source calculus. Furthermore, it provides a foundation for our long-term objective of designing a system for specifying and certifying imperative programs with dynamic memory allocation.
START Conference Manager (V2.54.6)