{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,20]],"date-time":"2026-05-20T22:21:43Z","timestamp":1779315703315,"version":"3.51.4"},"reference-count":28,"publisher":"Elsevier BV","issue":"3","license":[{"start":{"date-parts":[[1989,12,1]],"date-time":"1989-12-01T00:00:00Z","timestamp":628473600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":8629,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Information and Computation"],"published-print":{"date-parts":[[1989,12]]},"DOI":"10.1016\/0890-5401(89)90040-0","type":"journal-article","created":{"date-parts":[[2004,12,2]],"date-time":"2004-12-02T00:24:20Z","timestamp":1101947060000},"page":"265-359","source":"Crossref","is-referenced-by-count":17,"title":["Reasoning about procedures as parameters in the language L4"],"prefix":"10.1016","volume":"83","author":[{"given":"Steven M.","family":"German","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joseph Y.","family":"Halpern","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/0890-5401(89)90040-0_BIB1","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/357146.357150","article-title":"Ten years of Hoare's logic, A survey\u2014Part I","volume":"3","author":"Apt","year":"1981","journal-title":"ACM Toplas"},{"key":"10.1016\/0890-5401(89)90040-0_BIB2","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/322108.322121","article-title":"Programming language constructs for which it is impossible to obtain good Hoare-like axioms","volume":"26","author":"Clarke","year":"1979","journal-title":"J. Assoc. Comput. Mach."},{"key":"10.1016\/0890-5401(89)90040-0_BIB3_1","article-title":"The characterization problem for Hoare logics","volume":"312","author":"Clarke","year":"1984"},{"key":"10.1016\/0890-5401(89)90040-0_BIB3_2","unstructured":"in \u201cMathematical Logic and Programming Languages\u201d (C. A. R. Hoare and J. C. Shepherdson, Eds.), International Series in Computer Science, Prentice-Hall, Englewood Cliffs, NJ."},{"key":"10.1016\/0890-5401(89)90040-0_BIB4","doi-asserted-by":"crossref","first-page":"612","DOI":"10.1145\/2402.322394","article-title":"Effective axiomatizations of Hoare logics","volume":"30","author":"Clarke","year":"1983","journal-title":"J. Assoc. Comput. Mach."},{"issue":"No. 1","key":"10.1016\/0890-5401(89)90040-0_BIB5","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","article-title":"Soundness and completeness of an axiom system for program verification","volume":"7","author":"Cook","year":"1978","journal-title":"SIAM J. Comput."},{"key":"10.1016\/0890-5401(89)90040-0_BIB6_1","author":"Damm","year":"1983","journal-title":"A Sound and Relatively\u2217 Complete Hoare-Logic for a Language with Higher Type Procedures"},{"key":"10.1016\/0890-5401(89)90040-0_BIB6_2","doi-asserted-by":"crossref","unstructured":"Acta Inform. 20, 59\u2013101.","DOI":"10.1016\/0379-0738(82)90117-7"},{"key":"10.1016\/0890-5401(89)90040-0_BIB7","author":"Enderton","year":"1972"},{"key":"10.1016\/0890-5401(89)90040-0_BIB8","series-title":"Proceedings, Conference on Logics of Programs","first-page":"206","article-title":"Reasoning about procedures as parameters","volume":"Vol. 164","author":"German","year":"1983"},{"key":"10.1016\/0890-5401(89)90040-0_BIB9","series-title":"Proceedings, Symposium on Logic in Computer Science","first-page":"11","article-title":"True relative completeness of an axiom system for the language L4","author":"German","year":"1986"},{"key":"10.1016\/0890-5401(89)90040-0_BIB10","series-title":"True relative completeness of an axiom system for the language L4; with full details of proofs, privately circulated","author":"German","year":"1986"},{"key":"10.1016\/0890-5401(89)90040-0_BIB11","author":"German","year":"1983","journal-title":"On the Power of the Hypothesis of Expressiveness"},{"key":"10.1016\/0890-5401(89)90040-0_BIB12","series-title":"Proceedings, Conference on Logics of Programs","first-page":"106","article-title":"A Hoare calculus for functions defined by recursion on higher types","volume":"Vol. 193","author":"Goerdt","year":"1985"},{"key":"10.1016\/0890-5401(89)90040-0_BIB13","author":"Gorelick","year":"1975"},{"key":"10.1016\/0890-5401(89)90040-0_BIB14","series-title":"Proceedings, Eleventh Annual ACM Symposium on Principles of Programming Languages","first-page":"29","article-title":"On relative completeness in programming logics","volume":"66","author":"Grabowski","year":"1984"},{"key":"10.1016\/0890-5401(89)90040-0_BIB15","series-title":"Proceedings, Conference on Logics of Programs","first-page":"118","article-title":"On the relative incompleteness of logics for total correctness","volume":"Vol. 193","author":"Grabowski","year":"1985"},{"key":"10.1016\/0890-5401(89)90040-0_BIB16","series-title":"Proceedings, Eleventh Annual ACM Symposium on Principles of Programming Languages","first-page":"262","article-title":"A good Hoare axiom system for an Algol-like language","author":"Halpern","year":"1984"},{"key":"10.1016\/0890-5401(89)90040-0_BIB17","series-title":"Proceedings, Eleventh Annual ACM Symposium on Principles of Programming Languages","first-page":"245","article-title":"The semantics of local storage, or what makes the free-list free?","author":"Halpern","year":"1984"},{"key":"10.1016\/0890-5401(89)90040-0_BIB18","author":"Josko","year":"1983","journal-title":"On Expressive Interpretations of Hoare-Logic for a Language with Higher-Type Procedures"},{"key":"10.1016\/0890-5401(89)90040-0_BIB19","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1007\/BF00625282","article-title":"On termination problems for finitely interpreted ALGOL-like programs","volume":"18","author":"Langmaack","year":"1982","journal-title":"Acta Inform."},{"key":"10.1016\/0890-5401(89)90040-0_BIB20","series-title":"Proceedings, 18th IEEE Symposium on Foundations of Computer Science","first-page":"1","article-title":"A necessary and sufficient condition for the existence of Hoare logics","author":"Lipton","year":"1977"},{"key":"10.1016\/0890-5401(89)90040-0_BIB21","series-title":"Proceedings, 15th ACM Symposium on Theory of Computing","first-page":"320","article-title":"A characterization of Hoare's logic for programs with Pascal-like procedures","author":"Olderog","year":"1981"},{"key":"10.1016\/0890-5401(89)90040-0_BIB22_1","author":"Olderog","year":"1981"},{"key":"10.1016\/0890-5401(89)90040-0_BIB22_2","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0304-3975(84)90066-5","volume":"30","author":"Olderog","year":"1984","journal-title":"Theoret. Comput. Sci."},{"key":"10.1016\/0890-5401(89)90040-0_BIB23","series-title":"Proceedings, Conference on Logics of Programs","first-page":"320","article-title":"A partial correctness logic for procedures","volume":"Vol. 193","author":"Sieber","year":"1985"},{"key":"10.1016\/0890-5401(89)90040-0_BIB24","series-title":"Proceedings, Conference on Logics of Programs","first-page":"474","article-title":"From denotational to operational semantics for Algol-like languages: An overview","volume":"Vol. 164","author":"Trakhtenbrot","year":"1983"},{"key":"10.1016\/0890-5401(89)90040-0_BIB25","first-page":"212","article-title":"A necessary and sufficient condition in order that a Herbrand interpretation is expressive relative to recursive programs","volume":"56","author":"Urzyczyn","year":"1983"}],"container-title":["Information and Computation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0890540189900400?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:0890540189900400?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,4]],"date-time":"2020-04-04T12:49:37Z","timestamp":1586004577000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/0890540189900400"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1989,12]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1989,12]]}},"alternative-id":["0890540189900400"],"URL":"https:\/\/doi.org\/10.1016\/0890-5401(89)90040-0","relation":{},"ISSN":["0890-5401"],"issn-type":[{"value":"0890-5401","type":"print"}],"subject":[],"published":{"date-parts":[[1989,12]]}}}