{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,22]],"date-time":"2025-03-22T04:18:31Z","timestamp":1742617111094,"version":"3.40.2"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540544159"},{"type":"electronic","value":"9783540476177"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1991]]},"DOI":"10.1007\/3-540-54415-1_66","type":"book-chapter","created":{"date-parts":[[2012,2,25]],"date-time":"2012-02-25T22:46:43Z","timestamp":1330210003000},"page":"594-614","source":"Crossref","is-referenced-by-count":1,"title":["First order data types and first order logic"],"prefix":"10.1007","author":[{"given":"Ralf","family":"Treinen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"29_CR1","unstructured":"American National Standards Institute. The Programming Language Ada Reference Manual. LNCS vol. 155. Springer, 1983."},{"key":"29_CR2","unstructured":"J. Bishop. Data Abstraction in Programming Languages. Addison-Wesley, 1986."},{"key":"29_CR3","unstructured":"P. Buhmann. Disunifikation in modularen Termalgebren. Master's thesis, Universit\u00e4t des Saarlandes, 1991. In preparation."},{"key":"29_CR4","first-page":"292","volume":"86","author":"R. M. Burstall","year":"1980","unstructured":"R. M. Burstall and J. A. Goguen. Semantics of CLEAR, a specification language. In D. Bj\u00f6rner, editor, Abstract Softare Specifications, pages 292\u2013332. Springer LNCS, vol. 86, 1980.","journal-title":"LNCS"},{"key":"29_CR5","unstructured":"C. C. Chang and H. J. Keisler. Model Theory. Studies in Logic and the Foundations of Mathematics, vol. 73. North-Holland Publishing Company, third edition, 1990."},{"issue":"34","key":"29_CR6","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1016\/S0747-7171(89)80017-3","volume":"7","author":"H. Comon","year":"1989","unstructured":"H. Comon and P. Lescanne. Equational problems and disunification. Journal of Symbolic Computation, 7(3,4):371\u2013425, 1989.","journal-title":"Journal of Symbolic Computation"},{"key":"29_CR7","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1016\/S0747-7171(87)80022-6","volume":"3","author":"N. Dershowitz","year":"1987","unstructured":"N. Dershowitz. Termination of rewriting. Journal of Symbolic Computation, 3:69\u2013116, 1987.","journal-title":"Journal of Symbolic Computation"},{"key":"29_CR8","doi-asserted-by":"crossref","unstructured":"H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification, vol. 1. EATCS-Monographs on Theoretical Computer Science. Springer-Verlag, 1985.","DOI":"10.1007\/978-3-642-69962-7"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification, vol. 2. EATCS-Monographs on Theoretical Computer Science. Springer-Verlag, 1990.","DOI":"10.1007\/978-3-642-61284-8"},{"key":"29_CR10","unstructured":"H. B. Enderton. Mathematical Introduction to Logic. Academic Press, 1972."},{"key":"29_CR11","doi-asserted-by":"crossref","unstructured":"S. A. Greibach. Theory of Program Structures: Schemes, Semantics, Verification. Lecture Notes in Computer Science, Vol. 35. Springer Verlag, 1975.","DOI":"10.1007\/BFb0023017"},{"key":"29_CR12","unstructured":"I. Guessarian. Algebraic Semantics. Lecture Notes in Computer Science, Vol. 99. Springer Verlag, 1979."},{"key":"29_CR13","unstructured":"R. Harper, D. MacQueen, and R. Milner. Standard ML. Technical Report ECS-LFCS-86-2, Edinburgh University, 1986."},{"key":"29_CR14","doi-asserted-by":"crossref","unstructured":"D. Kozen and J. Tiuryn. Logics of programs. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 14, pages 789\u2013840. Elsevier Science Publishers, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50019-6"},{"key":"29_CR15","first-page":"131","volume":"332","author":"T. Lehmann","year":"1987","unstructured":"T. Lehmann and J. Loeckx. The specification language of OBSCURE. In D. Sannella and A. Tarlecki, editors, 5th Workshop on Specification of Abstract Data Types, pages 131\u2013153. Springer LNCS, vol. 332, 1987.","journal-title":"LNCS"},{"key":"29_CR16","unstructured":"T. Lehmann and J. Loeckx. OBSCURE, a specification language for abstract data types. Technical Report A 19\u201390, Universit\u00e4t des Saarlandes, 1990. Submitted for publication."},{"key":"29_CR17","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1111\/j.1755-2567.1969.tb00356.x","volume":"35","author":"P. Lindstr\u00f6m","year":"1969","unstructured":"P. Lindstr\u00f6m. On extension of elementary logic. Theoria, 35:1\u201311, 1969.","journal-title":"Theoria"},{"key":"29_CR18","unstructured":"B. Liskov and J. Guttag. Abstraction and Specification in Program Development. MIT press, 1986."},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"J. Loeckx. Algorithmic specifications: A constructive specification method for abstract data types. ACM Trans. Prog. Lang. Syst., 9(4), 1987.","DOI":"10.1145\/29873.30399"},{"key":"29_CR20","doi-asserted-by":"crossref","unstructured":"J. Loeckx and K. Sieber. The Foundations of Program Verification. Wiley\/Teubner, 2nd edition, 1987.","DOI":"10.1007\/978-3-322-96753-4"},{"key":"29_CR21","doi-asserted-by":"crossref","first-page":"220","DOI":"10.1016\/S0022-0000(70)80022-8","volume":"4","author":"D. C. Luckham","year":"1970","unstructured":"D. C. Luckham, D. M. R. Park, and M. S. Paterson. On formalized computer programs. J. Comput. Syst. Sci., 4:220\u2013249, 1970.","journal-title":"J. Comput. Syst. Sci."},{"key":"29_CR22","unstructured":"D. MacQueen. Modules for standard ML. In [13], 1986."},{"key":"29_CR23","doi-asserted-by":"crossref","unstructured":"M. J. Maher. Complete axiomatisations of the algebra of finite, rational and infinite trees. In Third Anual Symposium on Logic in Computer Science, pages 348\u2013357, Edinburgh, Scotland, july 1988. IEEE.","DOI":"10.1109\/LICS.1988.5132"},{"key":"29_CR24","doi-asserted-by":"crossref","unstructured":"J. D. Monk. Mathematical Logic. Graduate Texts in Mathematics, vol. 37. Springer, 1976.","DOI":"10.1007\/978-1-4684-9452-5"},{"key":"29_CR25","doi-asserted-by":"crossref","unstructured":"M. Shaw, editor. Alphard: Form and Content. Springer, 1981.","DOI":"10.1007\/978-1-4612-5979-4"},{"key":"29_CR26","first-page":"198","volume":"125","author":"J. Tiuryn","year":"1981","unstructured":"J. Tiuryn. A survey of the logic of effective definitions. In E. Engeler, editor, Proceedings of the Workshop on Logics of Programs, pages 198\u2013245. Springer LNCS, vol. 125, 1981.","journal-title":"LNCS"},{"key":"29_CR27","doi-asserted-by":"crossref","unstructured":"R. Treinen. First order data types and first order logic. Interner Bericht A 01\/91, Universit\u00e4t des Saarlandes, Jan. 1991.","DOI":"10.1007\/3-540-54415-1_66"},{"key":"29_CR28","first-page":"1","volume":"201","author":"D. A. Turner","year":"1985","unstructured":"D. A. Turner. Miranda: A non-strict functional language with polymorphic types. In J.-P. Jouannaud, editor, IFIP International Conference on Functional Programming Languages and Computer Architecture, pages 1\u201316. Springer LNCS, vol. 201, 1985.","journal-title":"LNCS"},{"key":"29_CR29","doi-asserted-by":"crossref","first-page":"332","DOI":"10.1016\/S0022-0000(74)80048-6","volume":"9","author":"J. Vuillemin","year":"1974","unstructured":"J. Vuillemin. Correct and optimal implementations of recursion in a simple programming language. J. Comput. Syst. Sci., 9:332\u2013354, 1974.","journal-title":"J. Comput. Syst. Sci."},{"key":"29_CR30","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF00264293","volume":"20","author":"M. Wirsing","year":"1983","unstructured":"M. Wirsing, P. Pepper, H. Partsch, W. Dosch, and M. Broy. On hierarchies of abstract data types. Acta Informatica, 20:1\u201333, 1983.","journal-title":"Acta Informatica"},{"key":"29_CR31","doi-asserted-by":"crossref","unstructured":"N. Wirth. Programming in MODULA-2. Springer, third edition, 1985.","DOI":"10.1007\/978-3-642-96878-5"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-54415-1_66.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,21]],"date-time":"2025-03-21T21:18:33Z","timestamp":1742591913000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-54415-1_66"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1991]]},"ISBN":["9783540544159","9783540476177"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/3-540-54415-1_66","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1991]]}}}