Abstract
We present a denotational model of impredicative Hoare Type Theory, a very expressive dependent type theory in which one can specify and reason about mutable abstract data types.
The model ensures soundness of the extension of Hoare Type Theory with impredicative polymorphism; makes the connections to separation logic clear, and provides a basis for investigation of further sound extensions of the theory, in particular equations between computations and types.
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
Appel, A., Mellièes, P.-A., Richards, C., Vouillon, J.: A very modal model of a modern, major, general type system. In: POPL 2007 (2007)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, Springer, Heidelberg (2005)
Benton, N., Leperchey, B.: Relational reasoning in a nominal semantics for storage. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 88–101. Springer, Heidelberg (2005)
Berger, M., Honda, K., Yoshida, N.: A logical analysis of aliasing in imperative higher-order functions. In: Danvy, O., Pierce, B.C. (eds.) ICFP 2005, Tallinn, Estonia, September 2005, 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)
Biering, B., Birkedal, L., Torp-Smith, N.: BI hyperdoctrines, Higher-Order Separation Logic, and Abstraction. In: TOPLAS 2007 (to appear, 2007)
Birkedal, L., Møgelberg, R., Petersen, R.: Domain-theoretic models of parametric polymorphism. In: TCS (to appear, 2007)
Birkedal, L., Torp-Smith, N., Yang, H.: Semantics of separation-logic typing and higher-order frame rules for algol-like languages. LMCS 2(5:1), 1–33 (2006)
Birkedal, L., Yang, H.: Relational parametricity and separation logic. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, Springer, Heidelberg (2007)
Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. International Journal on Software Tools for Technology Transfer 7(3), 212–232 (2005)
Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. Compaq Systems Research Center, Research Report 159 (December 1998)
Evans, D., Larochelle, D.: Improving security using extensible lightweight static analysis. IEEE Software 19(1), 42–51 (2002)
Jacobs, B.: Categorical Logic and Type Theory. Studies in Logic and the Foundations of Mathematics, vol. 141. Elsevier, Amsterdam (1999)
Krishnaswami, N.: Separation logic for a higher-order typed language. In: SPACE 2006, pp. 73–82 (2006)
Krishnaswami, N., Aldrich, J., Birkedal, L.: Modular verification of the subject-observer pattern via higher-order separation logic. In: FTfJP (2007)
Morrisett, G., Walker, D., Crary, K., Glew, N.: From System F to typed assembly language. ACM TPLS 21(3), 527–568 (1999)
Nanevski, A., Ahmed, A., Morrisett, G., Birkedal, L.: Abstract Predicates and Mutable ADTs in Hoare Type Theory. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 189–204. Springer, Heidelberg (2007)
Nanevski, A., Morrisett, G., Birkedal, L.: Polymorphism and separation in Hoare Type Theory. In: ICFP 2006, Portland, Oregon, pp. 62–73 (2006)
O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. In: POPL 2004, pp. 268–280 (2004)
Petersen, R., Birkedal, L., Nanevski, A., Morrisett, G.: A realizability model of impredicative hoare type theory. Technical report, IT University of Copenhagen (2007), http://www.itu.dk/people/birkedal/papers/httmodel-tr.pdf
Pym, D.: The Semantics and Proof Theory of the Logic of Bunched Implications. Applied Logics Series, vol. 26. Kluwer, Dordrecht (2002)
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)
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55–74 (2002)
Shinwell, M.: The Fresh Approach: Functional Programming with Names and Binders. PhD thesis, Computer Laboratory, Cambridge University (December 2004)
Shinwell, M.R., Pitts, A.M.: On a monadic semantics for freshness. TCS 342, 28–55 (2005)
Watkins, K., Cervesato, I., Pfenning, F., Walker, D.: A concurrent logical framework: The propositional fragment. In: Filliâtre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol. 3839, pp. 355–377. Springer, Heidelberg (2006)
Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL 1999, San Antonio, pp. 214–227 (1999)
Yoshida, N., Honda, K., Berger, M.: Local state in hoare logic for imperative higher-order functions. In: Seidl, H. (ed.) FOSSACS 2007. LNCS, vol. 4423, Springer, Heidelberg (2007)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Petersen, R.L., Birkedal, L., Nanevski, A., Morrisett, G. (2008). A Realizability Model for Impredicative Hoare Type Theory. In: Drossopoulou, S. (eds) Programming Languages and Systems. ESOP 2008. Lecture Notes in Computer Science, vol 4960. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78739-6_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-78739-6_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78738-9
Online ISBN: 978-3-540-78739-6
eBook Packages: Computer ScienceComputer Science (R0)