{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:28:21Z","timestamp":1725456501563},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540614630"},{"type":"electronic","value":"9783540685951"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0014353","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T09:04:25Z","timestamp":1132736665000},"page":"604-607","source":"Crossref","is-referenced-by-count":1,"title":["The Typelab specification and verification environment"],"prefix":"10.1007","author":[{"given":"F. W.","family":"von Henke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Luther","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Pfeifer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"H.","family":"Rue\u00df","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"D.","family":"Schwier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Strecker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M.","family":"Wagner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"52_CR1","unstructured":"R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"52_CR2","unstructured":"Cristina Comes et al. The Coq Proof Assistant Reference Manual. INRIA Rocquencourt and CNRS-ENS Lyon, 1995."},{"key":"52_CR3","doi-asserted-by":"crossref","unstructured":"J.A. Goguen. Parameterized programming. IEEE Transactions on Software Engineering, SE-10(5), September 1984.","DOI":"10.1109\/TSE.1984.5010277"},{"key":"52_CR4","unstructured":"Zhaohui Luo and Robert Pollack. LEGO Proof Development System: User's Manual. University of Edinburgh, Department of Computer Science, 1992."},{"key":"52_CR5","unstructured":"Zhaohui Luo. Computation and Reasoning. Oxford University Press, 1994."},{"key":"52_CR6","unstructured":"Marko Luther. Wissensbasierte Methoden zur Beweisunterst\u00fctzung in Typentheorie. Master's thesis, Universit\u00e4t Ulm, 1995. Available at URL http:\/\/www.informatik.uni-ulm.de\/ki\/Forschung\/Deduktion\/ml-diplomarbeit.html."},{"key":"52_CR7","doi-asserted-by":"crossref","unstructured":"Lena Magnusson and Bengt Nordstr\u00f6m. The ALF proof editor and its proof engine. In H. Barendregt and T. Nipkow, editors, Types for Proofs and Programs, volume 806 of Springer LNCS, pages 213\u2013237, 1994.","DOI":"10.1007\/3-540-58085-9_78"},{"key":"52_CR8","volume-title":"The PVS Specification Language","author":"S. Owre","year":"1993","unstructured":"S. Owre, N. Shankar, and J.M. Rushby. The PVS Specification Language. Computer Science Lab, SRI International, Menlo Park CA 94025, March 1993."},{"key":"52_CR9","doi-asserted-by":"crossref","unstructured":"[vHDR+95] F.W. von Henke, A. Dold, H. Rue\u00df, D. Schwier, and M. Strecker. Construction and deduction methods for the formal development of software. In KORSO: Methods, Languages, and Tools for the Construction of Correct Software, Springer LNCS 1009. 1995.","DOI":"10.1007\/BFb0015465"},{"key":"52_CR10","unstructured":"Matthias Wagner. Entwicklung und Implementierung eines Beweisers f\u00fcr konstruktive Logik. Master's thesis, Universit\u00e4t Ulm, 1995. Available at URL http:\/\/www.informatik.uni-ulm.de\/ki\/Forschung\/Deduktion\/mw-diplomarbeit.html."},{"key":"52_CR11","doi-asserted-by":"crossref","first-page":"123","DOI":"10.1016\/0304-3975(86)90051-4","volume":"42","author":"M. Wirsing","year":"1986","unstructured":"Martin Wirsing. Structured algebraic specifications: A kernel language. Theoretical Computer Science, 42:123\u2013249, 1986.","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014353","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:46:04Z","timestamp":1586580364000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014353"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614630","9783540685951"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/bfb0014353","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}