Aleksandar Nanevski
Greg Morrisett
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.
- M. Abadi and K.R.M. Leino. A logic of object-oriented programs. In Verification: Theory and Practice, pages 11--41. Springer-Verlag, 2004.]]Google Scholar
- 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.]]Google Scholar
- M. Berger, K. Honda, and N. Yoshida. A logical analysis of aliasing in imperative higher-order functions. In O. Danvy and B.C. Pierce, editors, International Conference on Functional Programming, ICFP'05, pages 280--293, Tallinn, Estonia, September 2005.]] Google ScholarDigital Library
- 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.]]Google Scholar
- L. Birkedal, N. Torp-Smith, and J. C. Reynolds. Local reasoning about a copying garbage collector. In Symposium on Principles of Programming Languages, POPL'04, pages 220--231, Venice, Italy, 2004.]] Google ScholarDigital Library
- L. Birkedal, N. Torp-Smith, and H. Yang. Semantics of separationlogic typing and higher-order frame rules. In Symposium on Logic in Computer Science, LICS'05, pages 260--269, Chicago, Illinois, June 2005.]] Google ScholarDigital Library
- R. Cartwright and D. C. Oppen. Unrestricted procedure calls in Hoare's logic. In Symposium on Principles of Programming Languages, POPL'78, pages 131--140, 1978.]] Google ScholarDigital Library
- A. Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5(2):56--68, Jun 1940.]]Google ScholarCross Ref
- S.A. Cook. Soundness and completeness of an axiom system for program verification. SIAM Journal of Computing, 7(1):70--90, 1978.]]Google ScholarDigital Library
- 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.]]Google Scholar
- D. Evans and D. Larochelle. Improving security using extensible lightweight static analysis. IEEE Software, 19(1):42--51, 2002.]] Google ScholarDigital Library
- C.A.R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576--580, 1969.]] Google ScholarDigital Library
- 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.]]Google Scholar
- K. Honda, N. Yoshida, and M. Berger. An observationally complete program logic for imperative higher-order functions. In Symposium on Logic in Computer Science, LICS'05, pages 270--279, Chicago, Illinois, June 2005.]] Google ScholarDigital Library
- 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.]]Google Scholar
- T. Jim, G. Morrisett, D. Grossman, M. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of C. In USENIX Annual Technical Conference, pages 275--288, Monterey, Canada, June 2002.]] Google ScholarDigital Library
- S.L.P. Jones and P. Wadler. Imperative functional programming. In Symposium on Principles of Programming Languages, POPL'93, pages 71--84, Charleston, South Carolina, 1993.]] Google ScholarDigital Library
- 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.]]Google Scholar
- 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.]]Google Scholar
- Y. Mandelbaum, D. Walker, and R. Harper. An effective theory of type refinements. In International Conference on Functional Programming, ICFP'03, pages 213--226, Uppsala, Sweden, September 2003.]] Google ScholarDigital Library
- 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.]]Google Scholar
- C. McBride. Dependently Typed Functional Programs and their Proofs. PhD thesis, University of Edinburgh, 1999.]]Google Scholar
- J.L. McCarthy. Towards a mathematical science of computation. In IFIP Congress, pages 21--28, 1962.]]Google Scholar
- E. Moggi. Computational lambda-calculus and monads. In Symposium on Logic in Computer Science, LICS'89, pages 14--23, Asilomar, California, 1989.]] Google ScholarDigital Library
- E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55--92, 1991.]] Google ScholarDigital Library
- A. Nanevski and G. Morrisett. Dependent type theory of stateful higher-order functions. Technical Report TR-24-05, Harvard University, December 2005.]]Google Scholar
- 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.]]Google ScholarDigital Library
- A. Nanevski, F. Pfenning, and B. Pientka. Contextual modal type theory. Under consideration for publication in the ACM Transactions on Computation Logic, September 2005.]] Google ScholarDigital Library
- G.C. Necula. Proof-carrying code. In Symposium on Principles of Programming Languages, POPL'97, pages 106--119, Paris, January 1997.]] Google ScholarDigital Library
- P. O'Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In International Workshop on Computer Science Logic, CSL'01, volume 2142 of Lecture Notes in Computer Science, pages 1--19. Springer, 2001.]] Google ScholarDigital Library
- P.W. O'Hearn, H. Yang, and J. C. Reynolds. Separation and information hiding. In Symposium on Principles of Programming Languages, POPL'04, pages 268--280, 2004.]] Google ScholarDigital Library
- L.C. Paulson. A formulation of the simple theory of types (for Isabelle). In International Conference in Computer Logic, COLOG'88, volume 417 of Lecture Notes in Computer Science, pages 246--274. Springer, 2000.]] Google ScholarDigital Library
- S. Peyton Jones, editor. Haskell 98 Language and Libraries: The Revised Report. Cambridge University Press, April 2003.]]Google Scholar
- F. Pfenning and R. Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511--540, 2001.]] Google ScholarDigital Library
- B.C. Pierce and D.N. Turner. Local type inference. ACM Transactions on Programming Languages and Systems, 22(1):1--44, 2000.]] Google ScholarDigital Library
- J.C. Reynolds. Separation logic: A logic for shared mutable data structures. In Symposium on Logic in Computer Science, LICS'02, pages 55--74, 2002.]] Google ScholarDigital Library
- Z. Shao, V. Trifonov, B. Saha, and N. Papaspyrou. A type system for certified binaries. ACM Transactions on Programming Languages and Systems, 27(1):1--45, January 2005.]] Google ScholarDigital Library
- F. Smith, D. Walker, and G. Morrisett. Alias types. In G. Smolka, editor, European Symposium on Programming, ESOP'00, volume 1782 of Lecture Notes in Computer Science, pages 366--381, Berlin, Germany, 2000.]] Google ScholarDigital Library
- SRI International and DSTO. The HOL System: Description. University of Cambridge Computer Laboratory, July 1991.]]Google Scholar
- P. Wadler. The marriage of effects and monads. In International Conference on Functional Programming, ICFP'98, pages 63--74, Baltimore, Maryland, 1998.]] Google ScholarDigital Library
- 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.]]Google Scholar
- H. Xi. Applied Type System (extended abstract). In TYPES'03, pages 394--408. Springer-Verlag LNCS 3085, 2004.]]Google Scholar
- H. Xi, C. Chen, and G. Chen. Guarded recursive datatype constructors. In Symposium on Principles of Programming Languages, POPL'03, pages 224--235, New Orleans, January 2003.]] Google ScholarDigital Library
- 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.]] Google ScholarDigital Library
Index Terms
- Polymorphism and separation in hoare type theory
Recommendations
Polymorphism and separation in hoare type theory
Proceedings of the 2006 ICFP conferenceIn 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 ...
Ynot: dependent types for imperative programs
ICFP '08: Proceedings of the 13th ACM SIGPLAN international conference on Functional programmingWe describe an axiomatic extension to the Coq proof assistant, that supports writing, reasoning about, and extracting higher-order, dependently-typed programs with side-effects. Coq already includes a powerful functional language that supports dependent ...
Structuring the verification of heap-manipulating programs
POPL '10Most systems based on separation logic consider only restricted forms of implication or non-separating conjunction, as full support for these connectives requires a non-trivial notion of variable context, inherited from the logic of bunched implications ...
Comments