Polymorphism and separation in hoare type theory

ABSTRACT

In previous work, we proposed a Hoare Type Theory (HTT) which combines effectful higher-order functions, dependent types and Hoare Logic specifications into a unified framework. However, the framework did not support polymorphism, and ailed to provide a modular treatment of state in specifications. In this paper, we address these shortcomings by showing that the addition of polymorphism alone is sufficient for capturing modular state specifications in the style of Separation Logic. Furthermore, we argue that polymorphism is an essential ingredient of the extension, as the treatment of higher-order functions requires operations not encodable via the spatial connectives of Separation Logic.

REFERENCES

• 1: M. Abadi and K.R.M. Leino. A logic of object-oriented programs. In Verification: Theory and Practice, pages 11--41. Springer-Verlag, 2004.
• 2: M. Barnett, K.R.M. Leino, and W. Schulte. The Spec# programming system: An overview. In CASSIS 2004, Lecture Notes in Computer Science. Springer, 2004.
• 3: Martin Berger , Kohei Honda , Nobuko Yoshida, A logical analysis of aliasing in imperative higher-order functions, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 4: B. Biering, L. Birkedal, and N. Torp-Smith. BI hyperdoctrines, Higher-Order Separation Logic, and Abstraction. Technical Report ITU-TR-2005-69, IT University of Copenhagen, Copenhagen, Denmark, July 2005.
• 5: Lars Birkedal , Noah Torp-Smith , John C. Reynolds, Local reasoning about a copying garbage collector, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.220-231, January 14-16, 2004, Venice, Italy
• 6: Hongseok Yang, Semantics of Separation-Logic Typing and Higher-Order Frame Rules, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), p.260-269, June 26-29, 2005 [doi>10.1109/LICS.2005.47]
• 7: Robert Cartwright , Derek Oppen, Unrestricted procedure calls in Hoare's logic, Proceedings of the 5th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.131-140, January 23-25, 1978, Tucson, Arizona [doi>10.1145/512760.512774]
• 8: A. Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2):56--68, Jun 1940.
• 9: S.A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal of Computing, 7(1):70--90, 1978.
• 10: D.L. Detlefs, K.R.M. Leino, G. Nelson, and J.B. Saxe. Extended static checking. Compaq Systems Research Center, Research Report 159, December 1998.
• 11: David Evans , David Larochelle, Improving Security Using Extensible Lightweight Static Analysis, IEEE Software, v.19 n.1, p.42-51, January 2002 [doi>10.1109/52.976940 ]
• 12: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 13: M. Hofmann. Extensional Concepts in Intensional Type Theory. PhD thesis, Department of Computer Science, University of Edinburgh, July 1995. Avaliable as Technical Report ECS-LFCS-95-327.
• 14: An Observationally Complete Program Logic for Imperative Higher-Order Frame Rules, Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS' 05), p.260-279, June 26-29, 2005 [doi>10.1109/LICS.2005.5]
• 15: W.A. Howard. The formulae-as-types notion of construction. In To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479--490. Academic Press, 1980.
• 16: Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
• 17: Simon L. Peyton Jones , Philip Wadler, Imperative functional programming, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.71-84, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158524]
• 18: N. Krishnaswami. Separation logic for a higher-order typed language. In Workshop on Semantics, Program Analysis and Computing Environments for Memory Management, SPACE'06, pages 73--82, 2006.
• 19: K.R.M. Leino, G. Nelson, and J.B. Saxe. ESC/Java User's Manual. Compaq Systems Research Center, October 2000. Technical Note 2000-002.
• 20: Yitzhak Mandelbaum , David Walker , Robert Harper, An effective theory of type refinements, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.213-225, August 25-29, 2003, Uppsala, Sweden
• 21: P. Martin-Löf. On the meanings of the logical constants and the justifications of the logical laws. Nordic Journal of Philosophical Logic, 1 1):11--60, 1996.
• 22: C. McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999.
• 23: J.L. McCarthy. Towards a mathematical science of computation. In IFIP Congress, pages 21--28, 1962.
• 24: E. Moggi, Computational lambda-calculus and monads, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.14-23, June 1989, Pacific Grove, California, United States
• 25: Eugenio Moggi, Notions of computation and monads, Information and Computation, v.93 n.1, p.55-92, July 1991 [doi>10.1016/0890-5401(91)90052-4]
• 26: A. Nanevski and G. Morrisett. Dependent type theory of stateful higher-order functions. Technical Report TR-24-05, Harvard University, December 2005.
• 27: A. Nanevski, G. Morrisett, and L. Birkedal. Polymorphism and Separation in Hoare Type Theory. Technical Report TR-10-06, Harvard University, April 2006. Available at http://www.eecs.harvard.edu/~aleks/papers/hoarelogic/httsep.pdf.
• 28: A. Nanevski, F. Pfenning, and B. Pientka. Contextual modal type theory. Under consideration for publication in the ACM Transactions on Computation Logic, September 2005.
• 29: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 30: Peter W. O'Hearn , John C. Reynolds , Hongseok Yang, Local Reasoning about Programs that Alter Data Structures, Proceedings of the 15th International Workshop on Computer Science Logic, p.1-19, September 10-13, 2001
• 31: Peter W. O'Hearn , Hongseok Yang , John C. Reynolds, Separation and information hiding, Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.268-280, January 14-16, 2004, Venice, Italy
• 32: Lawrence C. Paulson, A formulation of the simple theory of types (for Isabelle), Proceedings of the International Conference on Computer Logic, p.246-274, December 01, 1988
• 33: S. Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, April 2003.
• 34: Frank Pfenning , Rowan Davies, A judgmental reconstruction of modal logic, Mathematical Structures in Computer Science, v.11 n.4, p.511-540, August 2001 [doi>10.1017/S0960129501003322]
• 35: Benjamin C. Pierce , David N. Turner, Local type inference, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.1-44, Jan. 2000 [doi>10.1145/345099.345100]
• 36: John C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures, Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, p.55-74, July 22-25, 2002
• 37: Zhong Shao , Valery Trifonov , Bratin Saha , Nikolaos Papaspyrou, A type system for certified binaries, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.1, p.1-45, January 2005 [doi>10.1145/1053468.1053469]
• 38: Frederick Smith , David Walker , J. Gregory Morrisett, Alias Types, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.366-381, April 02, 2000
• 39: SRI International and DSTO. The HOL System: Description. University of Cambridge Computer Laboratory, July 1991.
• 40: Philip Wadler, The marriage of effects and monads, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.63-74, September 26-29, 1998, Baltimore, Maryland, United States
• 41: K. Watkins, I. Cervesato, F. Pfenning, and D. Walker. A concurrent logical framework: The propositional fragment. In S. Berardi, M. Coppo, and F. Damiani, editors, Types for Proofs and Programs, volume 3085 of Lecture Notes in Computer Science, pages 355--377. Springer, 2004.
• 42: H. Xi. Applied Type System (extended abstract). In TYPES'03, pages 394--408. Springer-Verlag LNCS 3085, 2004.
• 43: Hongwei Xi , Chiyan Chen , Gang Chen, Guarded recursive datatype constructors, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.224-235, January 15-17, 2003, New Orleans, Louisiana, USA
• 44: D. Zhu and H. Xi. Safe programming with pointers through stateful views. In Practical Aspects of Declarative Languages, PADL'05, volume 3350 of Lecture Notes in Computer Science, pages 83--97, Long Beach, California, January 2005. Springer.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Verification

Keywords:
hoare logic, separation logic, type theory