Abstract
We introduce a Hoare logic for call-by-value higher-order functional languages with control operators such as callcc. The key idea is to build the assertion language and proof rules around an explicit logical representation of jumps and their dual ’places-to-jump-to’. This enables the assertion language to capture precisely the intensional and extensional effects of jumping by internalising rely/guarantee reasoning, leading to simple proof rules for higher-order functions with callcc. We show that the logic can reason easily about non-trivial uses of callcc. The logic matches exactly with the operational semantics of the target language (observational completeness), is relatively complete in Cook’s sense and allows efficient generation of characteristic formulae.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Inf. & Comp. 163, 409–470 (2000)
Aspinall, D., Beringer, L., Hofmann, M., Loidl, H.-W., Momigliano, A.: A program logic for resource verification. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 34–49. Springer, Heidelberg (2004)
Bannwart, F., Müller, P.: A program logic for bytecode. ENTCS 141(1), 255–273 (2005)
Benton, N.: A Typed, Compositional Logic for a Stack-Based Abstract Machine. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 364–380. Springer, Heidelberg (2005)
Berger, M., Honda, K., Yoshida, N.: A logical analysis of aliasing for higher-order imperative functions. In: Proc. ICFP, pp. 280–293 (2005); Full version to appear in JFP
Berger, M., Honda, K., Yoshida, N.: Completeness and logical full abstraction in modal logics for typed mobile processes. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds.) ICALP 2008, Part II. LNCS, vol. 5126, pp. 99–111. Springer, Heidelberg (2008)
Beringer, L., Hofmann, M.: A bytecode logic for JML and types. In: Kobayashi, N. (ed.) APLAS 2006. LNCS, vol. 4279, pp. 389–405. Springer, Heidelberg (2006)
Caires, L.: Spatial-behavioral types, distributed services, and resources. In: Montanari, U., Sannella, D., Bruni, R. (eds.) TGC 2006. LNCS, vol. 4661, pp. 98–115. Springer, Heidelberg (2007)
Cardelli, L., Gordon, A.D.: Anytime, Anywhere. Modal Logics for Mobile Ambients. In: Proc. POPL, pp. 365–377 (2000)
Clint, M., Hoare, C.A.R.: Program Proving: Jumps and Functions. Acta Informatica 1, 214–224 (1972)
Duba, B.F., Harper, R., MacQueen, D.: Typing First-Class Continuations in ML. In: Proc. POPL, pp. 163–173 (1991)
Harper, R., Lillibridge, M.: Operational Interpretations of an Extension of F ω with Control Operators. Journal of Functional Programming 6(3), 393–417 (1996)
Honda, K.: Processes and games. ENTCS 71 (2002)
Honda, K., Berger, M., Yoshida, N.: Descriptive and Relative Completeness of Logics for Higher-Order Functions. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 360–371. Springer, Heidelberg (2006)
Honda, K., Yoshida, N.: A uniform type structure for secure information flow. In: POPL 2002, pp. 81–92. ACM Press, New York (2002); Full version to appear in ACM TOPLAS
Honda, K., Yoshida, N.: A compositional logic for polymorphic higher-order functions. In: Proc. PPDP 2004, pp. 191–202. ACM Press, New York (2004)
Honda, K., Yoshida, N., Berger, M.: Control in the π-calculus. In: Proc. CW 2004, ACM Press, New York (2004)
Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order functions. In: LICS 2005, pp. 270–279 (2005)
Hyland, J.M.E., Ong, C.H.L.: On full abstraction for PCF. Inf. & Comp. 163, 285–408 (2000)
Jones, C.B.: Specification and Design of (Parallel) Programs. In: IFIP Congress, pp. 321–332 (1983)
Laird, J.: A Semantic Analysis of Control. PhD thesis, Univ. of Edinburgh (1998)
Longley, J.: When is a functional program not a functional program? SIGPLAN Not. 34(9), 1–7 (1999)
Longley, J., Plotkin, G.: Logical Full Abstraction and PCF. In: Tbilisi Symposium on Logic, Language and Information. CSLI (1998)
Ni, Z., Shao, Z.: Certified Assembly Programming with Embedded Code Pointers. In: Proc. POPL (2006)
Ong, C.-H.L., Stewart, C.A.: A Curry-Howard foundation for functional computation with control. In: Proc. POPL, pp. 215–227 (1997)
Parigot, M.: λμ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In: Voronkov, A. (ed.) LPAR 1992. LNCS, vol. 624, pp. 190–201. Springer, Heidelberg (1992)
Plotkin, G.: Call-By-Name, Call-By-Value, and the λ-Calculus. TCS 1(2), 125–159 (1975)
Riecke, J.G., Thielecke, H.: Typed exceptions and continuations cannot macro-express each other. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 635–644. Springer, Heidelberg (1999)
Saabas, A., Uustalu, T.: A Compositional Natural Semantics and Hoare Logic for Low-Level Languages. In: Proc. Workshop Structural Operational Semantics, SOS (2006)
Stirling, C.: A complete compositional proof system for a subset of CCS. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 475–486. Springer, Heidelberg (1985)
Stirling, C.: Modal logics for communicating systems. TCS 49, 311–347 (1987)
Tan, G., Appel, A.W.: A Compositional Logic for Control Flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 80–94. Springer, Heidelberg (2005)
Thielecke, H.: Continuations, functions and jumps. Bulletin of EATCS, Logic Column 8 (1999)
Thielecke, H.: Frame rules from answer types for code pointers. In: Proc. POPL, pp. 309–319 (2006)
Winskel, G.: A complete proof system for SCCS with modal assertions. In: Maheshwari, S.N. (ed.) FSTTCS 1985. LNCS, vol. 206, pp. 392–410. Springer, Heidelberg (1985)
Yoshida, N., Honda, K., Berger, M.: Logical reasoning for higher-order functions with local state. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, pp. 361–377. Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berger, M. (2010). Program Logics for Sequential Higher-Order Control. In: Arbab, F., Sirjani, M. (eds) Fundamentals of Software Engineering. FSEN 2009. Lecture Notes in Computer Science, vol 5961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11623-0_11
Download citation
DOI: https://doi.org/10.1007/978-3-642-11623-0_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11622-3
Online ISBN: 978-3-642-11623-0
eBook Packages: Computer ScienceComputer Science (R0)