TY - GEN

T1 - Local actions for a curry-style operational semantics

AU - Stewart, Gordon

AU - Appel, Andrew W.

PY - 2011

Y1 - 2011

N2 - Soundness proofs of program logics such as Hoare logics and type systems are often made easier by decorating the operational semantics with information that is useful in the proof. However, modifying the operational semantics to carry around such information can make it more difficult to show that the operational semantics corresponds to what actually occurs on a real machine. In this work we present a program logic framework targeting operational semantics in Curry-style - that is, operational semantics without proof decorations such as separation algebras, share models, and step indexes. Although we target Curry-style operational semantics, our framework permits local reasoning via the frame rule and retains expressive assertions in the program logic. Soundness of the program logic is derived mechanically from simple properties of primitive commands and expressions. We demonstrate our framework by deriving a separation logic for the model of a core imperative programming language with external function calls. We also apply our framework in a more realistic setting in the soundness proof of a separation logic for CompCert's Cminor. Our proofs are machine-checked in Coq.

AB - Soundness proofs of program logics such as Hoare logics and type systems are often made easier by decorating the operational semantics with information that is useful in the proof. However, modifying the operational semantics to carry around such information can make it more difficult to show that the operational semantics corresponds to what actually occurs on a real machine. In this work we present a program logic framework targeting operational semantics in Curry-style - that is, operational semantics without proof decorations such as separation algebras, share models, and step indexes. Although we target Curry-style operational semantics, our framework permits local reasoning via the frame rule and retains expressive assertions in the program logic. Soundness of the program logic is derived mechanically from simple properties of primitive commands and expressions. We demonstrate our framework by deriving a separation logic for the model of a core imperative programming language with external function calls. We also apply our framework in a more realistic setting in the soundness proof of a separation logic for CompCert's Cminor. Our proofs are machine-checked in Coq.

KW - Curry-style operational semantics

KW - Local actions

KW - Separation logic

UR - http://www.scopus.com/inward/record.url?scp=79952163562&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=79952163562&partnerID=8YFLogxK

U2 - 10.1145/1929529.1929535

DO - 10.1145/1929529.1929535

M3 - Conference contribution

AN - SCOPUS:79952163562

SN - 9781450304870

T3 - PLPV'11 - Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification

SP - 31

EP - 42

BT - PLPV'11 - Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification

T2 - 5th ACM Workshop on Programming Languages Meets Program Verification, PLPV 2011

Y2 - 29 January 2011 through 29 January 2011

ER -