«Oracle Semantics Aquinas Hobor A Dissertation Presented to the Faculty of Princeton University in Candidacy for the Degree of Doctor of Philosophy ...»
tional semantics. In Proceedings of the 24th Conference on the Mathematical Foundations of Programming Semantics (MFPS 2008), 2008.
[Dij68] Edsger W. Dijkstra. Cooperating sequential processes. In
[Doc08] Robert Dockins. Share models, 2008. Private conversation & Coq implementation.
[Flo67] Robert W. Floyd. Assigning meanings to programs. In Proceedings of Symposia in Applied Mathematics, pages 19– 32, Providence, Rhode Island, 1967.
[GBC+ 07] Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv. Local reasoning for storable locks and threads. In Proceedings 5th Asian Symposium on Programming Languages and Systems (APLAS’07), 2007.
[GBCS07] Alexey Gotsman, Josh Berdine, Byron Cook, and Mooly
Sagiv. Thread-modular shape analysis. In PLDI ’07:
2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2007.
17th Annual International Symposium on Computer Architecture (ISCA 1990), pages 15–26, May 1990.
[Got08] Alexey Gotsman. private conversation, 2008.
[Han93] P. Brinch Hansen. Monitors and concurrent pascal: A personal history. In 2nd ACM Conference on the History of Programming Languages, pages 1–35, 1993.
[HAZ08a] Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. Oracle semantics for concurrent separation logic.
In Proceedings of the 17th European Symposium on Programming (ESOP 2008), pages 353–367, 2008.
[HAZ08b] Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. Oracle semantics for concurrent separation logic (extended version). Technical Report TR-825-08, Princeton University, June 2008.
[Hoa69] C A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):578–580, October 1969.
[Hoa74] C A. R. Hoare. Monitors: An operating system structur
[IO01] Samin Ishtiaq and Peter O’Hearn. BI as an assertion language for mutable data structures. In POPL 2001: The 28th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, pages 14–26. ACM Press, January 2001.
[Jon83] C. B. Jones. Speciﬁcation and design of (parallel) programs.
In IFIP Congress, pages 321–332, 1983.
[LB08] Xavier Leroy and Sandrine Blazy. Formal veriﬁcation of a c-like memory model and its uses for verifying program transformations. Journal of Automated Reasoning, 41(1):1– 31, 2008.
[Ler06] Xavier Leroy. Formal certiﬁcation of a compiler back-end, or: programming a compiler with a proof assistant. In 33rd symposium Principles of Programming Languages, pages 42–54, 2006.
[LPP05] Dirk Leinenbach, Wolfgang Paul, and Elena Petrova. Towards the formal veriﬁcation of a C0 compiler: Code generation and implementation correctness. In IEEE Conference on Software Engineering and Formal Methods, 2005.
[Moo89] J. Strother Moore. A mechanically veriﬁed language implementation. In Journal of Automated Reasoning, 5(4), pages 461–492, 1989.
[Nec97] George C. Necula. Proof-carrying code. In Procedings of
www.dcs.qmul.ac.uk/∼ohearn/furtherreading.html. Web page fetched June 30th, 2008.
[O’H07] Peter W. O’Hearn. Resources, concurrency and local reasoning. Theoretical Computer Science, 375(1):271–307, May 2007.
[Par05] Matthew J. Parkinson. Local Reasoning for Java. PhD thesis, University of Cambridge, 2005.
[Ric08] Christopher D. Richards. The Approximation Modality in Models of Higher-Order Types. PhD thesis, Princeton University, 2008. Unpublished Draft.
[Sch06] Norbert Schirmer. Veriﬁcation of Sequential Imperative