{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:16:16Z","timestamp":1725488176286},"publisher-location":"Berlin, Heidelberg","reference-count":8,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540672616"},{"type":"electronic","value":"9783540464280"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-46428-x_26","type":"book-chapter","created":{"date-parts":[[2007,8,1]],"date-time":"2007-08-01T02:01:06Z","timestamp":1185933666000},"page":"367-370","source":"Crossref","is-referenced-by-count":0,"title":["More About TAS and IsaWin \u2014 Tools for Formal Program Development"],"prefix":"10.1007","author":[{"given":"Christoph","family":"L\u00fcth","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Burkhart","family":"Wolff","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2000,5,19]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"R.-J. Back and J. von Wright. Refinement Calculus. Springer Verlag, 1998.","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"26_CR2","unstructured":"R. Bornat and B. Sufrin. Jape\u2019s quiet interface. In N. Merriam, editor, User Interfaces for Theorem Provers UITP\u2019 96, Technical Report, pages 25\u201334. University of York. Electronic proceedings available at http:\/\/www.cs.york.ac.uk\/~nam\/uitp96\/proceedings.html , 1996."},{"key":"26_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/BFb0030646","volume-title":"TAPSOFT 97\u2019: Theory and Practice of Software Development","author":"Kolyang","year":"1997","unstructured":"Kolyang, C. L\u00fcth, T. Meier, and B. Wolff. TAS and IsaWin: Generic interfaces for transformational program development and theorem proving. In M. Bidoit and M. Dauchet, editors, TAPSOFT 97\u2019: Theory and Practice of Software Development, number 1214 in LNCS, pages 855\u2013859. Springer Verlag, 1997."},{"key":"26_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"1186","DOI":"10.1007\/3-540-48118-4_13","volume-title":"FM\u201999 \u2014 Formal Methods. Proceedings","author":"B. Krieg-Br\u00fcckner","year":"1999","unstructured":"B. Krieg-Br\u00fcckner, J. Peleska, E.-R. Olderog, and A. Baer. The UniForM workbench, a universal development environment for formal methods. In J. M. Wing, J. Woodcock, and J. Davies, editors, FM\u201999 \u2014 Formal Methods. Proceedings, Vol. II, number 1709 in LNCS, pages 1186\u20131205. Springer Verlag, 1999."},{"key":"26_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1007\/978-3-540-49020-3_17","volume-title":"Fundamental Approaches to Software Engineering FASE\u201999. Joint European Conferences on Theory and Practice of Software ETAPS\u201999","author":"C. L\u00fcth","year":"1999","unstructured":"C. L\u00fcth, H. Tej, Kolyang, and B. Krieg-Br\u00fcckner. TAS and IsaWin: Tools for transformational program development and theorem proving. In J.-P. Finance, editor, Fundamental Approaches to Software Engineering FASE\u201999. Joint European Conferences on Theory and Practice of Software ETAPS\u201999, number 1577 in LNCS, pages 239\u2013243. Springer Verlag, 1999."},{"issue":"2","key":"26_CR6","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1017\/S0956796899003421","volume":"9","author":"C. L\u00fcth","year":"1999","unstructured":"C. L\u00fcth and B. Wolff. Functional design and implementation of graphical user interfaces for theorem provers. Journal of Functional Programming, 9(2):167\u2013189, March 1999.","journal-title":"Journal of Functional Programming"},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"T. Mossakowski. CASL \u2014 from semantics to tools. In TACAS 2000 \u2014 Tools and Algorithms for the Construction and Analysis of Systems. Springer Verlag, 2000. To appear in LNCS.","DOI":"10.1007\/3-540-46419-0_8"},{"key":"26_CR8","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle-A Generic Theorem Prover","author":"L. C. Paulson","year":"1994","unstructured":"L. C. Paulson. Isabelle-A Generic Theorem Prover. Number 828 in LNCS. Springer Verlag, 1994."}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-46428-X_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T16:29:24Z","timestamp":1556728164000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-46428-X_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540672616","9783540464280"],"references-count":8,"URL":"https:\/\/doi.org\/10.1007\/3-540-46428-x_26","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}