{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:23:21Z","timestamp":1725456201987},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540627814"},{"type":"electronic","value":"9783540685173"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0030645","type":"book-chapter","created":{"date-parts":[[2005,12,1]],"date-time":"2005-12-01T06:10:41Z","timestamp":1133417441000},"page":"849-854","source":"Crossref","is-referenced-by-count":1,"title":["TYPELAB: An environment for modular program development"],"prefix":"10.1007","author":[{"given":"F. W.","family":"von Henke","sequence":"first","affiliation":[]},{"given":"M.","family":"Luther","sequence":"additional","affiliation":[]},{"given":"M.","family":"Strecker","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,20]]},"reference":[{"key":"64_CR1","unstructured":"Michel Bidoit. Development of modular specifications by stepwise refinements using the PLUSS specification language. Proc. of the Unified Computation Laboratory, Oxford University Press, 1991."},{"key":"64_CR2","unstructured":"Rod Burstall and James McKinna. Deliverables: a categorical approach to program development in type theory. Technical Report ECS-LFCS-92-242, University of Edinburgh, October 1992."},{"key":"64_CR3","unstructured":"R.L. Constable et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, 1986."},{"key":"64_CR4","volume-title":"The Coq Proof Assistant Reference Manual","author":"C. Cornes","year":"1995","unstructured":"Cristina Cornes et al. The Coq Proof Assistant Reference Manual. INRIA Rocquencourt and CNRS-ENS Lyon, 1995."},{"key":"64_CR5","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/BF00881906","volume":"11","author":"W. M. Farmer","year":"1993","unstructured":"William M. Farmer, Joshua D. Guttman, and F. Javier Thayer. IMPS: An interactive mathematical proof system. J. of Automated Reasoning, 11:213\u2013248, 1993.","journal-title":"J. of Automated Reasoning"},{"key":"64_CR6","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":"64_CR7","unstructured":"Zhaohui Luo and Robert Pollack. LEGO Proof Development System: User's Manual. University of Edinburgh, Department of Computer Science, 1992."},{"key":"64_CR8","unstructured":"Zhaohui Luo. Computation and Reasoning. Oxford University Press, 1994."},{"key":"64_CR9","unstructured":"Marko Luther. Wissensbasierte Methoden zur Beweisunterst\u00fctzung in Type-ntheorie. Master's thesis, Universit\u00e4t Ulm, 1995. Available at URL http:\/\/www.informatik.uni-ulm.de\/ki\/Forschung\/Deduktion \/ml-dipl.html."},{"key":"64_CR10","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":"64_CR11","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":"64_CR12","doi-asserted-by":"crossref","unstructured":"Y. V. Srinivas and R. J\u00fcllig. Specware: Formal support for composing software. Technical Report KES.U.94.5, Kestrel Institute, 1994.","DOI":"10.1007\/3-540-60117-1_22"},{"key":"64_CR13","unstructured":"M. Strecker, M. Luther, and M. Wagner. Structuring and using a knowledge base of mathematical concepts: A type-theoretic approach. In EC AI-96 Workshop on Representation of mathematical knowledge, pages 23\u201326, 1996."},{"key":"64_CR14","unstructured":"Maria Sorea. Integration von Gleichheitsbeweisen in einen typentheoretischen Beweiser. Master's thesis, Universit\u00e4t Ulm, 1996. Forthcoming."},{"key":"64_CR15","doi-asserted-by":"crossref","unstructured":"F.W. von Henke, M. Luther, M. Strecker, and M. Wagner. The TYPELAB specification and verification environment. In M. Nivat M. Wirsing, editor, Proceedings AMAST'96, pages 604\u2013607. Springer LNCS 1101, 1996.","DOI":"10.1007\/BFb0014353"},{"key":"64_CR16","unstructured":"Matthias Wagner. Entwicklung und Implementierung eines Beweisers f\u00fcr konstruktive Logik. Master's thesis, Universit\u00e4t Ulm, 1995. http:\/\/www.informatik.uni-ulm.de\/ki\/Forschung\/Deduktion\/mw-dipl.html."},{"key":"64_CR17","doi-asserted-by":"publisher","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","TAPSOFT '97: Theory and Practice of Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0030645","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,5]],"date-time":"2023-05-05T17:49:37Z","timestamp":1683308977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0030645"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627814","9783540685173"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/bfb0030645","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}