{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:56:10Z","timestamp":1725562570590},"publisher-location":"Berlin, Heidelberg","reference-count":11,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642147050"},{"type":"electronic","value":"9783642147067"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14706-7_3","type":"book-chapter","created":{"date-parts":[[2010,8,11]],"date-time":"2010-08-11T09:14:43Z","timestamp":1281518083000},"page":"32-35","source":"Crossref","is-referenced-by-count":0,"title":["Integrating Types and Specifications for Secure Software Development"],"prefix":"10.1007","author":[{"given":"Greg","family":"Morrisett","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"PLT Scheme, \n                    \n                      http:\/\/www.plt-scheme.org\/"},{"issue":"3","key":"3_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. Leavens","year":"2006","unstructured":"Leavens, G.T., et al.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes\u00a031(3), 1\u201338 (2006)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"3_CR3","unstructured":"The Coq Proof Assistant, \n                    \n                      http:\/\/coq.inria.fr\/"},{"issue":"7","key":"3_CR4","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X. Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Comm. of the ACM.\u00a052(7), 107\u2013115 (2009)","journal-title":"Comm. of the ACM."},{"key":"3_CR5","unstructured":"ACL2, \n                    \n                      http:\/\/userweb.cs.utexas.edu\/~moore\/acl2\/acl2-doc.html"},{"key":"3_CR6","unstructured":"Agda, \n                    \n                      http:\/\/www.cs.chalmers.se\/~catarina\/agda\/"},{"key":"3_CR7","unstructured":"Epigram, \n                    \n                      http:\/\/www.e-pig.org\/"},{"key":"3_CR8","unstructured":"Isabelle, \n                    \n                      http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/"},{"key":"3_CR9","first-page":"62","volume-title":"11th ACM Intl. Conf. on Functional Prog","author":"A. Nanevski","year":"2006","unstructured":"Nanevski, A., et al.: Polymorphism and separation in Hoare Type Theory. In: 11th ACM Intl. Conf. on Functional Prog, pp. 62\u201373. ACM Press, New York (2006)"},{"key":"3_CR10","first-page":"237","volume-title":"37th ACM Symp. on Principles of Prog","author":"G. Malecha","year":"2010","unstructured":"Malecha, G., et al.: Towards a verified relational database management system. In: 37th ACM Symp. on Principles of Prog, pp. 237\u2013248. ACM Press, New York (2010)"},{"key":"3_CR11","first-page":"79","volume-title":"14th ACM Intl. Conf. on Functional Prog","author":"A. Chlipala","year":"2009","unstructured":"Chlipala, A., et al.: Effective interactive proofs for higher-order imperative programs. In: 14th ACM Intl. Conf. on Functional Prog, pp. 79\u201390. ACM Press, New York (2009)"}],"container-title":["Lecture Notes in Computer Science","Computer Network Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14706-7_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:36:34Z","timestamp":1619786194000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14706-7_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642147050","9783642147067"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14706-7_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}