1. Appel, A.W.: Tactics for Separation Logic (2006), http://www.cs.princeton.edu/~appel/papers/septacs.pdf

  2. Appel, A.W., Blazy, S.: Separation Logic for Small-Step Cminor. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 5–21. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  3. Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI, pp. 234–245. ACM (2011)

    Google Scholar 

  4. Dijkstra, E.W.: Go To statement considered harmful. Communications of the ACM 11(3), 147–148 (1968); Letter to the Editor

    Article  MathSciNet  Google Scholar 

  5. Ellison, C., Rosu, G.: An executable formal semantics of C with applications. In: POPL, pp. 533–544 (2012)

    Google Scholar 

  6. Felleisen, M., Hieb, R.: The Revised Report on the Syntactic Theories of Sequential Control and State. Theoretical Computer Science 103(2), 235–271 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  7. Huet, G.P.: The Zipper. Journal of Functional Programming 7(5), 549–554 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  8. International Organization for Standardization. ISO/IEC 9899-2011: Programming languages – C. ISO Working Group 14 (2012)

    Google Scholar 

  9. Knuth, D.: Structured programming with go to statements. In: Classics in software engineering, pp. 257–321. Yourdon Press (1979)

    Google Scholar 

  10. Krebbers, R., Wiedijk, F.: A Formalization of the C99 Standard in HOL, Isabelle and Coq. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) MKM 2011 and Calculemus 2011. LNCS (LNAI), vol. 6824, pp. 301–303. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Leroy, X.: A formally verified compiler back-end. Journal of Automated Reasoning 43(4), 363–446 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  12. Leroy, X.: The CompCert verified compiler, software and commented proof (2012), http://compcert.inria.fr/

  13. Norrish, M.: C formalised in HOL. PhD thesis, University of Cambridge (1998)

    Google Scholar 

  14. O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  15. von Oheimb, D.: Hoare Logic for Mutual Recursion and Local Variables. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FSTTCS 1999. LNCS, vol. 1738, pp. 168–180. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  16. Parkinson, M.J., Bornat, R., Calcagno, C.: Variables as Resource in Hoare Logics. In: LICS, pp. 137–146 (2006)

    Google Scholar 

  17. Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. Mathematical Structures in Computer Science 21(4), 795–825 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  18. Tews, H.: Verifying Duff’s device: A simple compositional denotational semantics for Goto and computed jumps (2004)

    Google Scholar