Interactive proofs in higher-order concurrent separation logic. (English) Zbl 1380.68341
Castagna, Giuseppe (ed.) et al., Proceedings of the 44th annual ACM SIGPLAN symposium on principles of programming languages, POPL ’17, Paris, France, January 15–21, 2017. New York, NY: Association for Computing Machinery (ACM) (ISBN 978-1-4503-4660-3). 205-217 (2017).
MSC:
| 68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |
| 03B70 | Logic in computer science |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Keywords:
Coq; fine-grained concurrency; interactive theorem proving; logical relations; separation logicSoftware:
CoqReferences:
| [1] | A. Ahmed. Semantics of Types for Mutable State. PhD thesis, Princeton University, 2004. |
| [2] | A. Ahmed. Step-indexed syntactic logical relations for recursive and quantified types. In ESOP, 2006. 10.1007/11693024_6 · Zbl 1178.68146 |
| [3] | A. Appel, P.-A. Melliès, C. Richards, and J. Vouillon. A very modal model of a modern, major, general type system. In POPL, 2007. 10.1145/1190216.1190235 · Zbl 1295.68072 |
| [4] | A. W. Appel. Tactics for Separation Logic, 2006. Available at http://www.cs.princeton.edu/ appel/papers/septacs.pdf. |
| [5] | A. W. Appel, editor. Program Logics for Certified Compilers. Cambridge University Press, 2014. · Zbl 1298.68009 |
| [6] | J. Bengtson, J. B. Jensen, and L. Birkedal. Charge! - A Framework for Higher-Order Separation Logic in Coq. In ITP, volume 7406 of LNCS, pages 315-331, 2012. · Zbl 1360.68741 |
| [7] | J. Berdine, C. Calcagno, and P. W. O’Hearn. Symbolic Execution with Separation Logic. In APLAS, volume 3780 of LNCS, pages 52-68, 2005. 10.1007/11575467_5 · Zbl 1159.68363 |
| [8] | L. Birkedal, B. Reus, J. Schwinghammer, K. Støvring, J. Thamsborg, and H. Yang. Step-indexed Kripke models over recursive worlds. In POPL, 2011. 10.1145/1926385.1926401 · Zbl 1284.68102 |
| [9] | A. Chlipala. The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier. In ICFP, pages 391-402, 2013. 10.1145/2500365.2500592 |
| [10] | Coq Development Team. The Coq Proof Assistant Reference Manual, 2016. Available at https://coq.inria.fr/doc/. |
| [11] | P. da Rocha Pinto, T. Dinsdale-Young, and P. Gardner. TaDA: A logic for time and data abstraction. In ECOOP, pages 207-231, 2014. 10.1007/978-3-662-44202-9_9 |
| [12] | D. Delahaye. A Tactic Language for the System Coq. In LPAR, volume 1955 of LNCS, pages 85-95, 2000. · Zbl 0988.68584 |
| [13] | T. Dinsdale-Young, M. Dodds, P. Gardner, M. Parkinson, and V. Vafeiadis. Concurrent abstract predicates. In ECOOP, pages 504-528, 2010. |
| [14] | D. Dreyer. ERC Project “RustBelt”, 2016. Available at http://plv.mpi-sws.org/rustbelt/. |
| [15] | D. Dreyer, A. Ahmed, and L. Birkedal. Logical step-indexed logical relations. LMCS, 7(2:16), 2011. |
| [16] | X. Feng. Local rely-guarantee reasoning. In POPL, pages 315-327, 2009. 10.1145/1480881.1480922 · Zbl 1315.68088 |
| [17] | X. Feng, R. Ferreira, and Z. Shao. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP, pages 173-188, 2007. · Zbl 1187.68150 |
| [18] | M. Fu, Y. Li, X. Feng, Z. Shao, and Y. Zhang. Reasoning about optimistic concurrency using a program logic for history. In CONCUR, pages 388-402, 2010. · Zbl 1287.03071 |
| [19] | M. Gordon and T. Melham, editors. Introduction to HOL. Cambridge University Press, 1993. · Zbl 0779.68007 |
| [20] | M. J. C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF, volume 78 of LNCS. Springer, 1979. · Zbl 0421.68039 |
| [21] | B. Jacobs, J. Smans, P. Philippaerts, F. Vogels, W. Penninckx, and F. Piessens. VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and Java. In NFM, volume 6617 of LNCS, pages 41-55, 2011. |
| [22] | J. B. Jensen, N. Benton, and A. Kennedy. High-level separation logic for low-level code. In POPL, pages 301-314, 2013. 10.1145/2429069.2429105 · Zbl 1301.68101 |
| [23] | R. Jung, R. Krebbers, L. Birkedal, and D. Dreyer. Higher-order ghost state. In ICFP, pages 256-269, 2016. 10.1145/2951913.2951943 · Zbl 1361.68066 |
| [24] | R. Jung, D. Swasey, F. Sieczkowski, K. Svendsen, A. Turon, L. Birkedal, and D. Dreyer. Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning. In POPL, pages 637-650, 2015. 10.1145/2676726.2676980 · Zbl 1346.68135 |
| [25] | R. Krebbers. The C standard formalized in Coq. PhD thesis, Radboud University, 2015. |
| [26] | R. Krebbers, R. Jung, A. Bizjak, J.-H. Jourdan, D. Dreyer, and L. Birkedal. The Essence of Higher-Order Concurrent Separation Logic, 2016. Draft. |
| [27] | M. Krogh-Jespersen, K. Svendsen, and L. Birkedal. A Logical Account of a Type-and-Effect System. In POPL, 2017. |
| [28] | G. Malecha and J. Bengtson. Extensible and Efficient Automation Through Reflective Tactics. In ESOP, volume 9632 of LNCS, pages 532-559, 2016. · Zbl 1335.68234 |
| [29] | A. McCreight. Practical Tactics for Separation Logic. In TPHOLs, volume 5674 of LNCS, pages 343-358, 2009. 10.1007/978-3-642-03359-9_24 · Zbl 1252.68261 |
| [30] | H. Nakano. A modality for recursion. In LICS, 2000. |
| [31] | A. Nanevski, R. Ley-Wild, I. Sergey, and G. A. Delbianco. Communicating state transition systems for fine-grained concurrent resources. In ESOP, pages 290-310, 2014. 10.1007/978-3-642-54833-8_16 · Zbl 1405.68219 |
| [32] | A. Nanevski, V. Vafeiadis, and J. Berdine. Structuring the verification of heap-manipulating programs. In POPL, pages 261-274, 2010. 10.1145/1706299.1706331 · Zbl 1312.68065 |
| [33] | A. Pilkiewicz and F. Pottier. The essence of monotonic state. In TLDI, 2011. 10.1145/1929553.1929565 |
| [34] | G. Plotkin and M. Abadi. A logic for parametric polymorphism. In TLCA, 1993. · Zbl 0788.68091 |
| [35] | S. Schäfer, T. Tebbi, and G. Smolka. Autosubst: Reasoning with de Bruijn Terms and Parallel Substitutions. In ITP, volume 9236 of LNCS, pages 359-374, 2015. · Zbl 1465.68037 |
| [36] | I. Sergey, A. Nanevski, and A. Banerjee. Mechanized verification of fine-grained concurrent programs. In PLDI, pages 77-87, 2015. 10.1145/2737924.2737964 |
| [37] | F. Sieczkowski, A. Bizjak, and L. Birkedal. ModuRes: A Coq library for modular reasoning about concurrent higher-order imperative programming languages. In ITP, volume 9236 of LNCS, pages 375- 390, 2015. · Zbl 1465.68038 |
| [38] | M. Sozeau and N. Oury. First-Class Type Classes. In TPHOLs, volume 5170 of LNCS, pages 278-293, 2008. 10.1007/978-3-540-71067-7_23 · Zbl 1165.68475 |
| [39] | B. Spitters and E. van der Weegen. Type classes for mathematics in type theory. MSCS, 21(4):795-825, 2011. · Zbl 1223.68105 |
| [40] | K. Svendsen and L. Birkedal. Impredicative concurrent abstract predicates. In ESOP, pages 149-168, 2014. 10.1007/978-3-642-54833-8_9 · Zbl 1405.68092 |
| [41] | K. Svendsen, L. Birkedal, and M. J. Parkinson. Modular reasoning about separation of concurrent data structures. In ESOP, pages 169- 188, 2013. 10.1007/978-3-642-37036-6_11 · Zbl 1381.68062 |
| [42] | A. Turon, D. Dreyer, and L. Birkedal. Unifying refinement and Hoarestyle reasoning in a logic for higher-order concurrency. In ICFP, pages 377-390, 2013. 10.1145/2500365.2500600 · Zbl 1323.68386 |
| [43] | V. Vafeiadis and M. Parkinson. A marriage of rely/guarantee and separation logic. In CONCUR, pages 256-271, 2007. · Zbl 1151.68556 |
| [44] | M. Wildmoser and T. Nipkow. Certifying Machine Code Safety: Shallow Versus Deep Embedding. In TPHOLs, volume 3223 of LNCS, pages 305-320, 2004. · Zbl 1099.68545 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
