Nick Benton
Microsoft Research
Cambridge, UK
Modelling and Reasoning about State
Abstract
Reasoning about programs that use dynamically allocated mutable storage is surprisingly difficult, especially in the presence of higher-order features such as first-class functions or code pointers. The hard problems in coming up with accurate models or usable program logics for languages that include these awkward features have many names, including aliasing, encapsulation, interference, privacy, ownership and freshness. I'll talk about some recent work that tries to use a relatively small number of ideas (chiefly relational parametricity and separation) to address these issues in several different contexts, including giving the semantics of ML-like languages, proving the correctness of static analyses and optimizing transformations, and specifying and verifying machine code programs.
Course materials
- N. Benton. Modelling and reasoning about state. Lecture slides [pdf].
- C. A. R. Hoare. An axiomatic basis for computer programming. Commun. of ACM, v. 12, n. 10, pp. 576-583, 1969.
- N. Benton. Simple relational correctness proofs for static analyses and program transformations. In Proc. of 31st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL '04, pp. 14-25. ACM Press, 2004.
- N. Benton, A. Kennedy, M. Hofmann, L. Beringer. Reading, writing and relations: Towards extensional semantics for effect analyses. In N. Kobayashi, ed., Proc. of the 4th Asian Symp. on Programming Languages and Systems, APLAS '06, v. 4279 of Lect. Notes in Comput. Sci., pp. 114-130. Springer, 2006.
- J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proc. of 17th Ann. IEEE Symp. on Logic in Computer Science, LICS '02, pp. 55-74. IEEE CS Press, 2002.
- A. R. Meyer, K. Sieber. Towards a fully abstract semantics for local variables. In Proc. of 15th ACM Symp. on Principles of Programming Languages, POPL '88, pp. 191-203. ACM Press, 1988.
- A. Pitts, I. Stark. Operational reasoning for functions with local state. In A. Gordon, A. Pitts, eds., Higher Order Operational Techniques in Semantics, Publ. of the Newton Inst., pp. 227-273. Cambridge University Press, 1998.
- N. Benton, B. Leperchey. Relational reasoning in a nominal semantics for storage. In P. Urzyczyn, ed., Proc. of 7th Int. Conf. on Typed Lambda Calculi and Applications, TLCA '05, v. 3461 of Lect. Notes in Comput. Sci., pp. 86-101. Springer, 2005.
- N. Benton. Abstracting allocation: The new new thing. In Z. Ézik, ed., Proc. of 20th Int. Wksh. on Computer Science Logic, CSL '06, v. 4207 of Lect. Notes in Comput. Sci., pp. 182-196. Springer, 2006.
- N. Benton, U. Zarfaty. Formalizing and verifying semantic type soundness for a simple compiler. In Proc. of 9th Int. ACM SIGPLAN Symp. on Principles and Practice of Declarative Programming, PPDP '07, pp. 1-12. ACM Press, 2007.
Last changed
March 12, 2008 23:52 EET
by
local organizers, ewscs08(at)cs.ioc.ee
EWSCS'08 page:
//cs.ioc.ee/ewscs/2008/