{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T08:22:40Z","timestamp":1775463760367,"version":"3.50.1"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1981,6,1]],"date-time":"1981-06-01T00:00:00Z","timestamp":360201600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[1981,6]]},"DOI":"10.1007\/bf00289260","type":"journal-article","created":{"date-parts":[[2004,10,5]],"date-time":"2004-10-05T03:39:42Z","timestamp":1096947582000},"page":"193-207","source":"Crossref","is-referenced-by-count":3,"title":["Axiomatic data type specifications: A first order theory of linear lists"],"prefix":"10.1007","volume":"15","author":[{"given":"Daniel J.","family":"Moore","sequence":"first","affiliation":[]},{"given":"Bruce","family":"Russell","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"CR1","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1016\/S0022-0000(75)80056-0","volume":"11","author":"J.W. deBakker","year":"1975","unstructured":"deBakker, J.W., Meertens, L.G.L.T.: On the completeness of the inductive assertion method. J. Comput. System Sci. 11, 323?357 (1975)","journal-title":"J. Comput. System Sci."},{"key":"CR2","unstructured":"Cartwright, R. Jr.: A practical formal semantic definition and verification system for TYPED LISP. Stanford Artificial Intelligence Laboratory Memo AIM-296, December 1976"},{"key":"CR3","volume-title":"Model theory. Studies in logic and the foundations of mathematics","author":"C.C. Chang","year":"1973","unstructured":"Chang, C.C., Keisler, H.J.: Model theory. Studies in logic and the foundations of mathematics. (A. Heyting, ed.) Vol. 73, Amsterdam: North-Holland, 1973"},{"key":"CR4","volume-title":"A mathematical introduction to logic","author":"H.B. Enderton","year":"1972","unstructured":"Enderton, H.B.: A mathematical introduction to logic. New York: Academic Press, 1972"},{"key":"CR5","volume-title":"Mathematical aspects of computer science","author":"R.W. Floyd","year":"1976","unstructured":"Floyd, R.W.: Assigning meaning to programs. In: Mathematical aspects of computer science, (J. Schwartz, ed.) Vol. 19, Providence, R.I.: American Mathematical Society 1976"},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"Guttag, J.V., Horowitz, E., Musser, D.R.: Some extensions to algebraic specifications. Information Sciences Institute Report RR-76-50, Marina del Rey, California 1976","DOI":"10.1145\/800022.808312"},{"key":"CR7","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1145\/359605.359618","volume":"20","author":"J.V. Guttag","year":"1977","unstructured":"Guttag, J.V.: Abstract data types and the development of data structures. Communications of the ACM, Vol.20, 396?404 (1977)","journal-title":"Communications of the ACM"},{"key":"CR8","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12, 576?580 (1969)","journal-title":"Communications of the ACM"},{"key":"CR9","volume-title":"Lecture Notes in Mathematics, Vol. 188","author":"C.A.R. Hoare","year":"1971","unstructured":"Hoare, C.A.R.: Procedures and parameters: An axiomatic approach. (E. Engeler ed.) Lecture Notes in Mathematics, Vol. 188, Berlin-Heidelberg-New York: Springer 1971"},{"key":"CR10","volume-title":"Structured programming","author":"C.A.R. Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Notes on data structuring. In: Structured programming. New York: Academic Press 1972"},{"key":"CR11","volume-title":"Introduction to metamathematics","author":"S.C. Kleene","year":"1952","unstructured":"Kleene, S.C.: Introduction to metamathematics. Amsterdam: North-Holland 1952"},{"key":"CR12","volume-title":"Mathematical logic","author":"S.C. Kleene","year":"1967","unstructured":"Kleene, S.C.: Mathematical logic. New York: John Wiley 1967"},{"key":"CR13","volume-title":"Current trends in programming methodology, Vol. 1","author":"B. Liskov","year":"1977","unstructured":"Liskov, B., Zilles, S.: An introduction to formal specifications of data abstractions. In: Current trends in programming methodology, Vol. 1 (R.T. Yeh, ed.), Englewood Cliffs, N.J.: Prentice-Hall, 1977"},{"key":"CR14","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/S0022-0000(69)80009-7","volume":"3","author":"Z. Manna","year":"1969","unstructured":"Manna, Z.: The correctness of programs. J. Comput. System Sci. 3, 119?127 (1969)","journal-title":"J. Comput. System Sci."},{"key":"CR15","volume-title":"Introduction to mathematical logic","author":"E. Mendelson","year":"1964","unstructured":"Mendelson, E.: Introduction to mathematical logic. New York: Van Nostrand 1964"},{"key":"CR16","first-page":"151","volume-title":"Proc. 5th ACM symposium on principles of programming languages, Tucson","author":"D.C. Oppen","year":"1978","unstructured":"Oppen, D.C.: Reasoning about recursively defined data structures. Proc. 5th ACM symposium on principles of programming languages, Tucson, 151?157. New York: ACM 1978"},{"key":"CR17","unstructured":"Soni, D., Moore, D.: The theory of linear lists with head and tail admits elimination of quantifiers. Computer and Information Science Department, The Ohio State University, Technical Report, 1979"},{"key":"CR18","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1145\/359461.359466","volume":"20","author":"B. Wegbreit","year":"1977","unstructured":"Wegbreit, B., Morris, J.H., Jr.:Subgoal induction. Communications of the ACM, 20, 209?222 (1977)","journal-title":"Communications of the ACM"},{"key":"CR19","volume-title":"Current trends in programming methodology, Vol. 4: Data structuring","year":"1978","unstructured":"Yeh, R.T., (ed.): Current trends in programming methodology, Vol. 4: Data structuring. Englewood Cliffs, N.J.: Prentice-Hall, 1978"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00289260.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF00289260\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF00289260","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T08:10:20Z","timestamp":1585901420000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF00289260"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1981,6]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1981,6]]}},"alternative-id":["BF00289260"],"URL":"https:\/\/doi.org\/10.1007\/bf00289260","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[1981,6]]}}}