Abstract
We introduce an extension of Hoare logic for call-by-value higher-order functions with ML-like local reference generation. Local references may be generated dynamically and exported outside their scope, may store higher-order functions and may be used to construct complex mutable data structures. This primitive is captured logically using a predicate asserting reachability of a reference name from a possibly higher-order datum and quantifiers over hidden references. The logic enjoys three completeness properties: relative completeness, a logical characterisation of the contextual congruence and derivability of characteristic formulae. The axioms for reachability and local invariants play a fundamental role in reasoning about non-trivial programs combining higher-order procedures and dynamically generated references.
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
A full version of this paper: http://www.doc.ic.ac.uk/~yoshida/local
Berger, M., Honda, K., Yoshida, N.: A logical analysis of aliasing for higher-order imperative functions. In: ICFP’05, pp. 280–293 (2005)
Biering, B., Birkedal, L., Torp-Smith, N.: Bi hyperdoctrines and higher-order separation logic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 233–247. Springer, Heidelberg (2005)
Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules. In: LICS’05, pp. 260–269 (2005)
Bornat, R., Calcagno, C., O’Hearn, P.: Local reasoning, separation and aliasing. In: Workshop SPACE (2004)
Gabbay, M., Pitts, A.: A New Approach to Abstract Syntax Involving Binders. In: Proc. LICS ’99, pp. 214–224 (1999)
Hoare, C.A.R.: An axiomatic basis of computer programming. CACM 12 (1969)
Hoare, C.A.R.: Proof of correctness of data representations. Acta Inf. 1, 271–281 (1972)
Hoare, C.A.R., Wirth, N.: Axiomatic semantics of Pascal. Toplas 1(2), 226–244 (1979)
Honda, K.: From process logic to program logic. In: ICFP’04, pp. 163–174. ACM Press, New York (2004)
Honda, K., Berger, M., Yoshida, N.: Descriptive and relative completeness for logics for higher-order functions. In: Bugliesi, M., et al. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 360–371. Springer, Heidelberg (2006)
Honda, K., Yoshida, N.: A compositional logic for polymorphic higher-order functions. In: PPDP’04, pp. 191–202. ACM Press, New York (2004)
Honda, K., Yoshida, N., Berger, M.: An observationally complete program logic for imperative higher-order functions. In: LICS’05, pp. 270–279 (2005), Full version is at http://www.doc.ic.ac.uk/~yoshida/local
Honsell, F., et al.: A variable typed logic of effects. Inf. Comput. 119(1), 55–90 (1995)
Koutavas, V., Wand, M.: Small bisimulations for reasoning about higher-order imperative programs. In: Proc. POPL (2006)
Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL’06, pp. 115–126. ACM Press, New York (2006)
Mendelson, E.: Introduction to Mathematical Logic. Wadsworth Inc., Boston (1987)
Meyer, A.R., Sieber, K.: Towards fully abstract semantics for local variables. In: POPL’88, pp. 191–203 (1988)
Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Transactions on Computational Logic 6(4), 749–783 (2005)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, parts I and II. Info. & Comp. 100(1), 1–77 (1992)
Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare type theory. In: ICFP06, pp. 62–73. ACM Press, New York (2006)
Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)
Pitts, A.M.: Reasoning about local variables with operationally-based logical relations. In: Algol-Like Languages, vol. 2, pp. 173–193. Birkhäuser, Basel (1997)
Pitts, A.M.: Nominal logic, a first order theory of names and binding. Information and Computation 186, 165–193 (2003)
Pitts, A.M., Stark, I.D.B.: Operational reasoning for functions with local state. In: Higher Order Operational Techniques in Semantics, pp. 227–273. Cambridge University Press, Cambridge (1998)
Reus, B., Schwinghammer, J.: Separation logic for higher-order store. In: Ésik, Z. (ed.) CSL 2006. LNCS, vol. 4207, pp. 575–590. Springer, Heidelberg (2006)
Reus, B., Streicher, T.: About Hoare logics for higher-order store. In: Caires, L., et al. (eds.) ICALP 2005. LNCS, vol. 3580, pp. 1337–1348. Springer, Heidelberg (2005)
Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS’02 (2002)
Reynolds, J.C.: Idealized Algol and its specification logic. In: Tools and Notions for Program Construction (1982)
Stark, I.: Names and Higher-Order Functions. PhD thesis, University of Cambridge (1994)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Yoshida, N., Honda, K., Berger, M. (2007). Logical Reasoning for Higher-Order Functions with Local State. In: Seidl, H. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2007. Lecture Notes in Computer Science, vol 4423. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71389-0_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-71389-0_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71388-3
Online ISBN: 978-3-540-71389-0
eBook Packages: Computer ScienceComputer Science (R0)