{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:15:30Z","timestamp":1725455730701},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540605898"},{"type":"electronic","value":"9783540478027"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0015464","type":"book-chapter","created":{"date-parts":[[2005,11,13]],"date-time":"2005-11-13T06:32:11Z","timestamp":1131863531000},"page":"221-238","source":"Crossref","is-referenced-by-count":1,"title":["Formalization of algebraic specification in the development language Deva"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Santen","sequence":"first","affiliation":[]},{"given":"Florian","family":"Kamm\u00fcller","sequence":"additional","affiliation":[]},{"given":"Stefan","family":"J\u00e4hnichen","sequence":"additional","affiliation":[]},{"given":"Martin","family":"Beyer","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"12_CR1","unstructured":"M. Anlauff. Devil: Devas's interactive laboratory. Tutorial and user manual. Technical Report 93-42, Dept. of Computer Science, Technische Universit\u00e4t Berlin, 1993."},{"key":"12_CR2","doi-asserted-by":"crossref","unstructured":"M. Anlauff, M. Beyer, and T. Santen. Generische Sprachen in Systemen zur formalen Softwareentwicklung. In H. Reichel, editor, Informatik \u2014 Wirtschaft \u2014 Gesellschaft, Informatik aktuell, pages 247\u2013252. Springer Verlag, 1993.","DOI":"10.1007\/978-3-642-78486-6_39"},{"key":"12_CR3","unstructured":"M. Biersack, R. Raschke, and M. Simons. Proof presentation in Deva: The devaweb system. Technical Report 93-39, Dept. of Computer Science, Technische Universit\u00e4t Berlin, December 1993."},{"key":"12_CR4","doi-asserted-by":"crossref","unstructured":"R. S. Bird. An introduction to the theory of lists. In M. Broy, editor, Logic of Programming and Calculi of Discrete Design, pages 5\u201342. Springer, 1987.","DOI":"10.1007\/978-3-642-87374-4_1"},{"key":"12_CR5","unstructured":"M. Broy, C. Facchi, R. Grosu, et al. The Requirement and Design Specification Language SPECTRUM \u2014 An Informal Introduction \u2014 Version 1.0. Technical report, Technische Universit\u00e4t M\u00fcnchen, March 1993."},{"key":"12_CR6","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/0167-6423(86)90004-3","volume":"7","author":"M. Broy","year":"1986","unstructured":"M. Broy, B. M\u00f6ller, P. Pepper, and M. Wirsing. Algebraic implementations preserve program correctness. Science of Computer Programming, 7:35\u201353, 1986.","journal-title":"Science of Computer Programming"},{"key":"12_CR7","unstructured":"R.L. Constable, S.F. Allen, H.M. Bromley, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, 1986."},{"key":"12_CR8","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Thierry Coquand and G\u00e9rard Huet. The calculus of constructions. Information and Computation, 76:95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"12_CR9","unstructured":"N.G. de Bruijn. A survey of the project AUTOMATH. In J.P. Seldin and J.R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 579\u2013606. Academic Press, 1980."},{"key":"12_CR10","unstructured":"Philippe de Groote. Definition et Propi\u00e9t\u00e9s d'un m\u00e9tacalcul de repr\u00e9sentation de th\u00e9ories. PhD thesis, Universit\u00e9 Catholique de Louvain, February 1991."},{"key":"12_CR11","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1016\/S0304-3975(82)80001-7","volume":"20","author":"H. Ehrig","year":"1982","unstructured":"H. Ehrig, H.-J. Kreowski, B. Mahr, and P. Padawitz. Algebraic implementation of abstract data types. Theoretical Computer Science, 20:209\u2013263, 1982.","journal-title":"Theoretical Computer Science"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 1. Springer Verlag, 1985.","DOI":"10.1007\/978-3-642-69962-7"},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"H. Ehrig and B. Mahr. Fundamentals of Algebraic Specification 2. Springer Verlag, 1989.","DOI":"10.1007\/978-3-642-61284-8"},{"issue":"1","key":"12_CR14","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143\u2013184, January 1993.","journal-title":"Journal of the ACM"},{"key":"12_CR15","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"C. A. R. Hoare","year":"1972","unstructured":"C. A. R. Hoare. Proof of correctness of data representations. Acta Informatica, 1:271\u2013281, 1972.","journal-title":"Acta Informatica"},{"key":"12_CR16","doi-asserted-by":"crossref","unstructured":"C.B. Jones. Program specification and verification in VDM. In M. Broy, editor, Logic of Programming and Calculi of Discrete Design, pages 149\u2013184. Springer, 1987.","DOI":"10.1007\/978-3-642-87374-4_7"},{"key":"12_CR17","doi-asserted-by":"crossref","unstructured":"C.B. Jones, K.D. Jones, P.A. Lindsay, and R. Moore. mural: A Formal Development Support System. Springer, 1991.","DOI":"10.1007\/978-1-4471-3180-9"},{"key":"12_CR18","unstructured":"F. Kamm\u00fcller. Konstruktion von Datentypen und struktureller Induktion am Beispiel von Lazy Listen. Studienarbeit, Dept. of Computer Science, Technische Universit\u00e4t Berlin, 1994."},{"issue":"2","key":"12_CR19","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1093\/comjnl\/27.2.97","volume":"27","author":"D. E. Knuth","year":"1984","unstructured":"D. E. Knuth. Literate programming. The Computer Journal, 27(2):97\u2013111, 1984.","journal-title":"The Computer Journal"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Z. Luo. ECC, an extended calculus of constructions. In Proc. of the Fourth Ann. Symp. on Logic in Computer Science, pages 386\u2013395, 1989.","DOI":"10.1109\/LICS.1989.39193"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"R.P. Nederpelt. An approach to theorem proving on the basis of a typed lambda calculus. In W. Bibel and R. Kowalski, editors, 5th Conference on Automated Deduction, LNCS 87, pages 182\u2013194. Springer, 1980.","DOI":"10.1007\/3-540-10009-1_15"},{"key":"12_CR22","unstructured":"E.-R. Olderog, editor. IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET'94). North-Holland, 1994."},{"key":"12_CR23","unstructured":"D. Sannella and M. Wirsing. A kernel language for algebraic specification and implementation. In Proc. 1983 Intl. Conf. on Foundations of Computation Theory, LNCS 158, pages 413\u2013427. Springer Verlag, 1983."},{"key":"12_CR24","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF00283329","volume":"25","author":"D. Sannella","year":"1988","unstructured":"D. Sannella and A. Tarlecki. Toward formal development of programs from algebraic specifications: Implementations revisited. Acta Informatica, 25:233\u2013281, 1988.","journal-title":"Acta Informatica"},{"key":"12_CR25","unstructured":"T. Santen. Formalization of the Spectrum methodology in Deva: Signature and logical calculus. Technical Report 93-04, Dept. of Computer Science, Technische Universit\u00e4t Berlin, 1993."},{"key":"12_CR26","unstructured":"M. Simons, M. Biersack, and R. Raschke. Literate and structured presentation of formal proofs. In Olderog [Old94], pages 61\u201381."},{"key":"12_CR27","unstructured":"J. van Leeuwen, editor. Handbook of Theoretical Computer Science, volume B: Formal Models and Semantics. Elsevier, 1990."},{"issue":"5","key":"12_CR28","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/BF01212485","volume":"5","author":"M. Weber","year":"1993","unstructured":"M. Weber. Definition and basic properties of the Deva meta-calculus. Formal Aspects of Computing, 5(5):391\u2013431, 1993.","journal-title":"Formal Aspects of Computing"},{"key":"12_CR29","doi-asserted-by":"crossref","unstructured":"M. Weber, M. Simons, and C. Lafontaine. The Generic Development Language Deva: Presentation and Case Studies, LNCS 738. Springer, 1993.","DOI":"10.1007\/3-540-57335-6"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"M. Wirsing. Algebraic Specification, chapter 13 of [vLe90], pages 675\u2013788, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50018-4"}],"container-title":["Lecture Notes in Computer Science","KORSO: Methods, Languages, and Tools for the Construction of Correct Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0015464","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,10]],"date-time":"2020-04-10T20:47:12Z","timestamp":1586551632000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0015464"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540605898","9783540478027"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/bfb0015464","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}