{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:56:11Z","timestamp":1776891371775,"version":"3.51.2"},"reference-count":73,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","issue":"5-6","license":[{"start":{"date-parts":[[2008,9,2]],"date-time":"2008-09-02T00:00:00Z","timestamp":1220313600000},"content-version":"unspecified","delay-in-days":1,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2008,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We consider the problem of reconciling a dependently typed functional language with imperative features such as mutable higher-order state, pointer aliasing, and nontermination. We propose Hoare type theory (HTT), which incorporates Hoare-style specifications into types, making it possible to statically track and enforce correct use of side effects.<\/jats:p>\n                  <jats:p>\n                    The main feature of HTT is the Hoare type {\n                    <jats:italic>P<\/jats:italic>\n                    }\n                    <jats:italic>x<\/jats:italic>\n                    :\n                    <jats:italic>A<\/jats:italic>\n                    {\n                    <jats:italic>Q<\/jats:italic>\n                    } specifying computations with precondition\n                    <jats:italic>P<\/jats:italic>\n                    and postcondition\n                    <jats:italic>Q<\/jats:italic>\n                    that return a result of type\n                    <jats:italic>A<\/jats:italic>\n                    . Hoare types can be nested, combined with other types, and abstracted, leading to a smooth integration with higher-order functions and type polymorphism.\n                  <\/jats:p>\n                  <jats:p>We further show that in the presence of type polymorphism, it becomes possible to interpret the Hoare types in the \u201csmall footprint\u201d manner, as advocated by separation logic, whereby specifications tightly describe the state required by the computation.<\/jats:p>\n                  <jats:p>We establish that HTT is sound and compositional, in the sense that separate verifications of individual program components suffice to ensure the correctness of the composite program.<\/jats:p>","DOI":"10.1017\/s0956796808006953","type":"journal-article","created":{"date-parts":[[2008,9,2]],"date-time":"2008-09-02T04:06:07Z","timestamp":1220328367000},"page":"865-911","source":"Crossref","is-referenced-by-count":98,"title":["Hoare type theory, polymorphism and separation"],"prefix":"10.46298","volume":"18","author":[{"given":"ALEKSANDAR","family":"NANEVSKI","sequence":"first","affiliation":[]},{"given":"GREG","family":"MORRISETT","sequence":"additional","affiliation":[]},{"given":"LARS","family":"BIRKEDAL","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,9,2]]},"reference":[{"key":"S0956796808006953_ref32","unstructured":"Hofmann Martin . (July, 1995) Extensional Concepts in Intensional Type Theory. Ph.D. Thesis, Department of Computer Science, University of Edinburgh. Technical Report ECS-LFCS-95-327."},{"key":"S0956796808006953_ref71","first-page":"214","volume-title":"Symposium on Principles of Programming Languages POPL'99","author":"Xi","year":"1999"},{"key":"S0956796808006953_ref55","first-page":"246","volume-title":"International Conference in Computer Logic, COLOG'88","author":"Paulson","year":"1990"},{"key":"S0956796808006953_ref52","doi-asserted-by":"publisher","DOI":"10.1145\/358728.358748"},{"key":"S0956796808006953_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/165180.165214"},{"key":"S0956796808006953_ref62","doi-asserted-by":"publisher","DOI":"10.1145\/1053468.1053469"},{"key":"S0956796808006953_ref58","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"S0956796808006953_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014052"},{"key":"S0956796808006953_ref59","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"S0956796808006953_ref20","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"S0956796808006953_ref22","doi-asserted-by":"publisher","DOI":"10.1109\/52.976940"},{"key":"S0956796808006953_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"S0956796808006953_ref60","volume-title":"International Workshop on Computer Science Logic CSL'06","author":"Reus","year":"2006"},{"key":"S0956796808006953_ref34","first-page":"479","volume-title":"Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Howard","year":"1980"},{"key":"S0956796808006953_ref25","first-page":"7","volume-title":"European Symposium on Programming ESOP'06","author":"Fluet","year":"2006"},{"key":"S0956796808006953_ref67","first-page":"63","volume-title":"International Conference on Functional Programming ICFP'98","author":"Wadler","year":"1998"},{"key":"S0956796808006953_ref63","first-page":"116","volume-title":"International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA'04","author":"Sheard","year":"2004"},{"key":"S0956796808006953_ref49","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_22"},{"key":"S0956796808006953_ref6","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"Barnes","year":"2003"},{"key":"S0956796808006953_ref47","first-page":"14","volume-title":"Symposium on Logic in Computer Science LICS'89","author":"Moggi","year":"1989"},{"key":"S0956796808006953_ref5","first-page":"239","volume-title":"International Conference on Functional Programming ICFP'98","author":"Augustsson","year":"1998"},{"key":"S0956796808006953_ref17","doi-asserted-by":"publisher","DOI":"10.1137\/0207005"},{"key":"S0956796808006953_ref70","first-page":"249","volume-title":"Conference on Programming Language Design and Implementation PLDI'98","author":"Xi","year":"1998"},{"key":"S0956796808006953_ref51","first-page":"106","volume-title":"Symposium on Principles of Programming Languages POPL'97","author":"Necula","year":"1997"},{"key":"S0956796808006953_ref4","first-page":"91","volume-title":"Symposium on Principles of Programming Languages POPL 06","author":"Amtoft","year":"2006"},{"key":"S0956796808006953_ref56","volume-title":"Haskell 98 Language and Libraries: The Revised Report","author":"Peyton","year":"2003"},{"key":"S0956796808006953_ref42","first-page":"213","volume-title":"International Conference on Functional Programming ICFP'03","author":"Mandelbaum","year":"2003"},{"key":"S0956796808006953_ref45","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796803004829"},{"key":"S0956796808006953_ref30","first-page":"48","volume-title":"Symposium on Principles and Practice of Parallel Programming PPOPP'05","author":"Harris","year":"2005"},{"key":"S0956796808006953_ref39","unstructured":"Leino K. Rustan M. , Nelson Greg & Saxe James B. (October, 2000) ESC Java User's Manual. Technical Note 2000-002. Compaq Systems Research Center."},{"key":"S0956796808006953_ref10","first-page":"260","volume-title":"Symposium on Logic in Computer Science LICS'05","author":"Birkedal","year":"2005"},{"key":"S0956796808006953_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5229-1_12"},{"key":"S0956796808006953_ref9","first-page":"220","volume-title":"Symposium on Principles of Programming LanguagesPOPL'04","author":"Birkedal","year":"2004"},{"key":"S0956796808006953_ref18","unstructured":"Detlefs David L. , Leino K. Rustan M. , Nelson Greg & Saxe James B. (December, 1998) Extended Static Checking. Research Report 159, Compaq Systems Research Center."},{"key":"S0956796808006953_ref16","volume-title":"European Symposium on Programming ESOP'07","author":"Condit","year":"2007"},{"key":"S0956796808006953_ref46","first-page":"21","volume-title":"Congress of the International Federation for Information Processing, IFIP'62","author":"McCarthy","year":"1962"},{"key":"S0956796808006953_ref15","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.04.010"},{"key":"S0956796808006953_ref31","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"S0956796808006953_ref65","volume-title":"The HOL System: Description","year":"1991"},{"key":"S0956796808006953_ref66","first-page":"80","volume-title":"International Conference on Verification, Model Checking and Abstract Interpretation VMCAI'06","author":"Tan","year":"2006"},{"key":"S0956796808006953_ref36","first-page":"73","volume-title":"Workshop on Semantics, Program Analysis and Computing Environments for Memory Management SPAC'06","author":"Krishnaswami","year":"2006"},{"key":"S0956796808006953_ref57","first-page":"71","volume-title":"Symposium on Principles of Programming Languages POPL'93","author":"Peyton","year":"1993"},{"key":"S0956796808006953_ref64","first-page":"366","volume-title":"European Symposium on Programming ESOP'00","author":"Smith","year":"2000"},{"key":"S0956796808006953_ref61","first-page":"55","volume-title":"Symposium on Logic in Computer Science LICS'02","author":"Reynolds","year":"2002"},{"key":"S0956796808006953_ref44","unstructured":"McBride Conor . (1999) Dependently Typed Functional Programs and Their Proofs. Ph.D. Thesis, University of Edinburgh. Technical Report ECS-LFCS-00-419."},{"key":"S0956796808006953_ref48","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"S0956796808006953_ref6a","doi-asserted-by":"crossref","unstructured":"Barnett Mike , Leino K. Rustan M. & Schulte Wolfram . (2004) The Spec# programming system: An overview. In International Workshop on Construction and Analysis of Safe, Secure and Interoperable Smart Devices, CASSIS'04. Lecture Notes in Computer Science, Vol. 3362. Springer, Berlin, Germany.","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"S0956796808006953_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-004-0167-4"},{"key":"S0956796808006953_ref69","first-page":"268","volume-title":"International Conference on Functional Programming ICFP'05","author":"Westbrook","year":"2005"},{"key":"S0956796808006953_ref2","first-page":"78","volume-title":"International Conference on Functional Programming, ICFP'05","author":"Ahmed","year":"2005"},{"key":"S0956796808006953_ref12","first-page":"131","volume-title":"Symposium on Principles of Programming Languages POPL'78","author":"Cartwright","year":"1978"},{"key":"S0956796808006953_ref33","first-page":"270","volume-title":"Symposium on Logic in Computer Science LICS'05","author":"Honda","year":"2005"},{"key":"S0956796808006953_ref14","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0956796808006953_ref38","doi-asserted-by":"publisher","DOI":"10.1145\/570886.570888"},{"key":"S0956796808006953_ref41","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198538356.001.0001","volume-title":"Computation and Reasoning: A Type Theory for Computer Science","author":"Luo","year":"1994"},{"key":"S0956796808006953_ref50","first-page":"189","volume-title":"European Symposium on Programming ESOP'07","author":"Nanevski","year":"2007"},{"key":"S0956796808006953_ref29","first-page":"180","volume-title":"Symposium on Principles of Programming Languages POPL'79","author":"Greif","year":"1979"},{"key":"S0956796808006953_ref28","volume-title":"Proofs and Types","author":"Girard","year":"1989"},{"key":"S0956796808006953_ref72","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30557-6_8"},{"key":"S0956796808006953_ref68","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_23"},{"key":"S0956796808006953_ref43","first-page":"11","article-title":"On the meanings of the logical constants and the justifications of the logical laws","volume":"1","author":"Martin-L\u00f6f","year":"1996","journal-title":"Nordic J. Philosophic. Logic"},{"key":"S0956796808006953_ref23","first-page":"173","volume-title":"European Symposium on Programming ESOP'07","author":"Feng","year":"2007"},{"key":"S0956796808006953_ref3","first-page":"303","volume-title":"S ymposium on Logic in Computer Science, LICS01","author":"Altenkirch","year":"2001"},{"key":"S0956796808006953_ref7","first-page":"280","volume-title":"International Conference on Functional Programming ICFP 5","author":"Berger","year":"2005"},{"key":"S0956796808006953_ref24","first-page":"245","volume-title":"Symposium on Principles of Programming Languages POPL'06","author":"Flanagan","year":"2006"},{"key":"S0956796808006953_ref13","first-page":"66","volume-title":"International Conference on Functional Programming ICFP'05","author":"Chen","year":"2005"},{"key":"S0956796808006953_ref54","first-page":"268","volume-title":"Symposium on Principles of Programming Languages POPL'04","author":"O'Hearn","year":"2004"},{"key":"S0956796808006953_ref40","unstructured":"Luo Zhaohui . (1990) An Extended Calculus of Constructions. Ph.D. Thesis, University of Edinburgh. Technical Report ECS-LFCS-90-118."},{"key":"S0956796808006953_ref8","doi-asserted-by":"crossref","unstructured":"Biering B. , Birkedal L. & Torp-Smith N. (July, 2005). BI Hyperdoctrines, Higher-Order Separation Logic, and Abstraction. Technical Report ITU-TR-2005-69. IT University of Copenhagen.","DOI":"10.1007\/978-3-540-31987-0_17"},{"key":"S0956796808006953_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2005.07.001"},{"key":"S0956796808006953_ref53","first-page":"1","volume-title":"International Workshop on Computer Science Logic CSL'01","author":"O'Hearn","year":"2001"},{"key":"S0956796808006953_ref1","first-page":"11","volume-title":"Verification: Theory and Practice","author":"Abadi","year":"2004"},{"key":"S0956796808006953_ref35","first-page":"275","volume-title":"USENIX Annual Technical Conference, USENIX'02","author":"Jim","year":"2002"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796808006953","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:12Z","timestamp":1776889152000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796808006953\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,9]]},"references-count":73,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2008,9]]}},"alternative-id":["S0956796808006953"],"URL":"https:\/\/doi.org\/10.1017\/s0956796808006953","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008,9]]}}}