Output details

Blaming the client: on data refinement in the presence of pointers

<10>Data refinement is an age-old technique in program design, whereby an abstract description of data structures are refined by concrete representations. This paper addresses the open problem of soundness of data refinement in the presence of low-level programming features used in the fundamental code such as operating systems, network code and device drivers which powers our computing infrastructure. O’Hearn’s expertise in logics for resources sparked insights concerning how to describe divisions amongst program components without relying on scope, allowing precise theorems about modular refinement reasoning encompassing address arithmetic and other low-level programming concepts, for the first time.