![]() |
COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. | ![]() |
University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Reasoning about Code Pointers (Separation Logic for Higher-Order Store)
Reasoning about Code Pointers (Separation Logic for Higher-Order Store)Add to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Tom Ridge. Separation Logic is a sub-structural logic that supports local reasoning for imperative programs with heaps. It is designed to elegantly describe sharing and aliasing properties of heap structures, thus facilitating the verification of programs with pointers. So far, various flavours of separation logic have been developed for heaps containing records of basic data types. Yet, languages like C or ML also allow procedures to be stored on the heap. Such type of heap is commonly referred to as “higher-order store’’. > This talk addresses the problem of lifting Separation Logic from first-order to higher-order store. To that end we endow a simple language including dynamic memory management with a Hoare-style logic featuring Separation Logic connectives. To prove soundness, Denotational Semantics is employed throughout but not just for conceptual clarity. Modeling higher-order store as recursive domain enables us to use powerful (and well established) results from Domain Theory. This approach also admits an elegant re-use of a proof rule we introduced in previous work to deal with recursion through the store. This is joint work with Jan Schwinghammer, Programming Systems Lab, Saarland University. This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsMedical Research Council Biostatistics Unit Centenary celebratory events cambridge architecture society Magdalene Society of MedievalistsOther talksPsychology and Suicidal Behaviour The homelands of the plague: Soviet disease ecology in Central Asia, 1920s–1950s Succulents with Altitude Internal Displacement in Cyprus and childhood: The view from genetic social psychology What we don’t know about the Universe from the very small to the very big : ONE DAY MEETING |