{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:55:41Z","timestamp":1725663341329},"publisher-location":"Berlin, Heidelberg","reference-count":40,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540128960"},{"type":"electronic","value":"9783540387756"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1984]]},"DOI":"10.1007\/3-540-12896-4_382","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T17:57:27Z","timestamp":1330192647000},"page":"474-500","source":"Crossref","is-referenced-by-count":11,"title":["From denotational to operational and axiomatic semantics for ALGOL-like languages: An overview"],"prefix":"10.1007","author":[{"given":"B. A.","family":"Trakhtenbrot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joseph Y.","family":"Halpern","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Albert R.","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"32_CR1","unstructured":"K. R. Apt, Equivalence of operational semantics for a fragment of Pascal, in Formal Descriptions of Programming Language Concepts, E. J. Neuhold, ed., North Holland, 1978."},{"key":"32_CR2","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"K. R. Apt","year":"1981","unstructured":"K. R. Apt, Ten years of Hoare's logic: a survey \u2014 part I, ACM Trans. Programming Languages and Systems 3, 1981, 431\u2013483.","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"32_CR3","first-page":"101","volume":"159","author":"K. R. Apt","year":"1983","unstructured":"K. R. Apt, Ten years of Hoare's logic, a survey, part II: nondeterminism, Foundations of Computer Science IV, Mathematical Center Tracts, 159, Mathematisch Centrum, Amsterdam, 1983, 101\u2013132.","journal-title":"Foundations of Computer Science IV, Mathematical Center Tracts"},{"key":"32_CR4","unstructured":"H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, Studies in Logic 103, North Holland, 1981."},{"key":"32_CR5","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1007\/BF00264535","volume":"15","author":"R. Cartwright","year":"1981","unstructured":"R. Cartwright and D. Oppen, The logic of aliasing, Acta Informatica 15, 1981, 365\u2013384.","journal-title":"Acta Informatica"},{"key":"32_CR6","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"E. M. Clarke","year":"1979","unstructured":"E. M. Clarke, Programming language constructs for which it is impossible to obtain good Hoare-like axioms, J.ACM 26, 1979, 129\u2013147.","journal-title":"J.ACM"},{"key":"32_CR7","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"S. A. Cook","year":"1978","unstructured":"S. A. Cook, Soudness and completeness of an axiom system for program verification, SIAM J. Computing 7, 1978, 70\u201390.","journal-title":"SIAM J. Computing"},{"key":"32_CR8","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0304-3975(82)90009-3","volume":"20","author":"W. Damm","year":"1982","unstructured":"W. Damm, The IO-and OI-hierarchies, Theoretical Computer Science 20, 1982, 95\u2013207.","journal-title":"Theoretical Computer Science"},{"key":"32_CR9","unstructured":"W. Damm and E. Fehr, A schematological approach to the procedure concept of Algol-like languages, Proc. 5ieme colloque sur les arbres en algebre et en programmation, Lille, 1980, 130\u2013134."},{"key":"32_CR10","doi-asserted-by":"crossref","unstructured":"W. Damm and B. Josko, A sound and relatively* complete Hoare-logic for a language with higher type procedures, Lehrstuhl fur Informatik II, RWTH Aachen, Bericht No. 77, 1982, 94pp.","DOI":"10.1007\/BF00264295"},{"key":"32_CR11","unstructured":"J. De Bakker, Mathematical Theory of Program Correctness, Prentice-Hall International, 1980, 505pp."},{"key":"32_CR12","doi-asserted-by":"crossref","unstructured":"J. De Bakker, J. W. Klop, and J.-J.Ch. Meyer, Correctness of programs with function procedures, Logics of Programs, D. Kozen, ed., Lecture Notes in Computer Science 131, Springer, 1982, 94\u2013112.","DOI":"10.1007\/BFb0025776"},{"key":"32_CR13","doi-asserted-by":"crossref","unstructured":"S. German, E. Clarke, and J. Halpern, Reasoning about procedures as parameters, 1983, this volume.","DOI":"10.1007\/3-540-12896-4_365"},{"key":"32_CR14","unstructured":"I. Guessarian, Survey on some classes of interpretations and some their applications, Laboratoire Informatique Theorique et Programmation, 82-46, Univ. Paris 7, 1982."},{"key":"32_CR15","unstructured":"G. A. Gorelick, A complete axiom system for proving assertions about recursive and non-recursive programs, University of Toronto, Computer Science Dept. TR-75, 1975."},{"key":"32_CR16","doi-asserted-by":"crossref","unstructured":"J. Y. Halpern, A good Hoare axiom system for an Algol-like language, 1983, to appear.","DOI":"10.1145\/800017.800538"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"D. Harel, A. Pnueli, and J. Stavi, A complete axiomatic system for proving deductions about recursive programs, Proc. 9th ACM Symp. Theory of Computing, 1977, 249\u2013260.","DOI":"10.1145\/800105.803415"},{"key":"32_CR18","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. R. Hoare","year":"1969","unstructured":"C. A. R. Hoare, An axiomatic basis for computer programming, Comm. ACM, 12, 1969, 576\u2013580.","journal-title":"Comm. ACM"},{"key":"32_CR19","doi-asserted-by":"crossref","unstructured":"T. M. V. Janssen and P. van Emde Boas, On the proper treatment of referencing, dereferencing and assignment, 4th Int'l. Coll. Automata, Languages, and Programming, Lecture Notes in Computer Science 52, Springer, 1977, 282\u2013300.","DOI":"10.1007\/3-540-08342-1_22"},{"key":"32_CR20","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1145\/363744.363749","volume":"8","author":"P. J. Landin","year":"1965","unstructured":"P. J. Landin, A correspondence between Algol 60 and Church's lambda notation, Comm. ACM 8, 1965, 89\u2013101 and 158\u2013165.","journal-title":"Comm. ACM"},{"key":"32_CR21","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1007\/BF00289503","volume":"2","author":"H. Langmaack","year":"1973","unstructured":"H. Langmaack, On procedures as open subroutines, Acta Informatica 2, 1973, 311\u2013333.","journal-title":"Acta Informatica"},{"key":"32_CR22","doi-asserted-by":"crossref","unstructured":"H. Langmaack and E. R. Olderog, Present-day Hoare-like systems, 7th Int'l. Coll. Automata, Languages, and Programming, Lecture Notes in Computer Science 85, Springer, 1980, 363\u2013373.","DOI":"10.1007\/3-540-10003-2_84"},{"key":"32_CR23","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1007\/BF00264494","volume":"16","author":"Z. Manna","year":"1981","unstructured":"Z. Manna and R. Waldinger, Problematic features of programming languages: a situational-calculus approach, Acta Informatica 16, 1981, 371\u2013426.","journal-title":"Acta Informatica"},{"key":"32_CR24","first-page":"509","volume":"26","author":"J. Meseguer","year":"1978","unstructured":"J. Meseguer, Completions, factorizations and colimits of \u03c9-posets, Coll. Math. Soc. Janos Bolyai 26. Math. Logic in Computer Science, Salgotarjan, Hungary, 1978, 509\u2013545.","journal-title":"Coll. Math. Soc. Janos Bolyai"},{"key":"32_CR25","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1016\/S0019-9958(82)80087-9","volume":"52","author":"A. R. Meyer","year":"1982","unstructured":"A. R. Meyer, What is a model of the \u03bb-calculus? Information and Control 52, 1982, 87\u2013122.","journal-title":"Information and Control"},{"key":"32_CR26","first-page":"337","volume-title":"Revised as: Termination assertions for recursive programs: completeness and axiomatic definability, MIT\/LCS\/TM-214","author":"A. R. Meyer","year":"1982","unstructured":"A. R. Meyer and J. C. Mitchell, Axiomatic definability and completeness for recursive programs, 9th ACM Symposium on Principles of Programming Languages, 1982, 337\u2013346. Revised as: Termination assertions for recursive programs: completeness and axiomatic definability, MIT\/LCS\/TM-214, MIT, Cambridge, Massachusetts, March, 1982; to appear Information and Control, 1982."},{"key":"32_CR27","unstructured":"R. E. Milne and C. Strachey, A Theory of Programming Language Semantics, 2 Vols., Chapman and Hall, 1976."},{"key":"32_CR28","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1093\/comjnl\/5.4.349","volume":"5","author":"P. Naur","year":"1963","unstructured":"P. Naur et al., Revised report on the algorithmic language Algol 60, Computer J. 5, 1963, 349\u2013367.","journal-title":"Computer J."},{"key":"32_CR29","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/BF00261258","volume":"16","author":"E. R. Olderog","year":"1981","unstructured":"E. R. Olderog, Sound and complete Hoare-like calculi based on copy rules, Acta Informatica 16, 1981, 161\u2013197.","journal-title":"Acta Informatica"},{"key":"32_CR30","doi-asserted-by":"crossref","unstructured":"E. R. Olderog, A characterization of Hoare's logic for programs with Pascal-like procedures, Proc. 15th ACM Symp. Theory of Computing, 1983a, 320\u2013329.","DOI":"10.1145\/800061.808761"},{"key":"32_CR31","doi-asserted-by":"crossref","unstructured":"E. R. Olderog, Hoare's logic for program with procedures \u2014 what has been accomplished?, Proc. Logics of Programs, Carnegie-Mellon Univ., Pittsburgh, 1983, to appear, Lecture Notes in Computer Science, Springer, 1983b.","DOI":"10.1007\/3-540-12896-4_375"},{"key":"32_CR32","doi-asserted-by":"crossref","unstructured":"F. J. Oles, Type algebras, functor categories, and block structure, Computer Science Dept., Aarhus Univ. DAIMI PB-156, Denmark, Jan. 1983.","DOI":"10.7146\/dpb.v12i156.7430"},{"key":"32_CR33","doi-asserted-by":"crossref","unstructured":"G. D. Plotkin, A Powerdomain for countable non-determinism, 9th Int'l. Coll. Automata, Languages, and Programming, Lecture Notes in Computer Science 140, Springer, 1982, 412\u2013428.","DOI":"10.1007\/BFb0012788"},{"key":"32_CR34","unstructured":"J. C. Reynolds, The essence of Algol, International Symposium on Algorithmic Languages, de Bakker and van Vliet, eds., North Holland, 1981a, 345\u2013372."},{"key":"32_CR35","unstructured":"J. C. Reynolds, The Craft of Programming, Prentice Hall International Series in Computer Science, 1981b, 434pp."},{"key":"32_CR36","unstructured":"J. C. Reynolds, Idealized Algol and its specification logic, Syracuse University, Technical Report 1-81, 1981c."},{"key":"32_CR37","doi-asserted-by":"crossref","unstructured":"R. L. Schwartz, An axiomatic treatment of Algol 68 Routines, 6th Int'l. Coll. Automata, Languages and Programming, Lecture Notes in Computer Science 71, Springer, 1979, 530\u2013545.","DOI":"10.1007\/3-540-09510-1_43"},{"key":"32_CR38","doi-asserted-by":"crossref","unstructured":"D. S. Scott, Domains for Denotational Semantics, 9th Int'l. Conf. Automata, Languages, and Programming, Lecture Notes in Computer Science 140, Springer, 1982, 577\u2013613; to appear, Information and Control.","DOI":"10.1007\/BFb0012801"},{"key":"32_CR39","volume-title":"Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory","author":"J. E. Stoy","year":"1977","unstructured":"J. E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, Massachusetts, 1977."},{"key":"32_CR40","doi-asserted-by":"crossref","unstructured":"B. A. Trakhtenbrot, On relaxation rules in algorithmic logic, Mathematical Foundations of Computer Science 1979, (J. Becvar, ed.), Lecture Notes in Computer Science 74, Springer, 1979, 453\u2013462.","DOI":"10.1007\/3-540-09526-8_45"}],"container-title":["Lecture Notes in Computer Science","Logics of Programs"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-12896-4_382.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,31]],"date-time":"2021-12-31T01:26:29Z","timestamp":1640913989000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-12896-4_382"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1984]]},"ISBN":["9783540128960","9783540387756"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/3-540-12896-4_382","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1984]]}}}