{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T10:57:41Z","timestamp":1743073061770,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319035413"},{"type":"electronic","value":"9783319035420"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-03542-0_22","type":"book-chapter","created":{"date-parts":[[2013,12,9]],"date-time":"2013-12-09T16:31:54Z","timestamp":1386606714000},"page":"307-314","source":"Crossref","is-referenced-by-count":2,"title":["The Proof Assistant as an Integrated Development Environment"],"prefix":"10.1007","author":[{"given":"Nick","family":"Benton","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"22_CR1","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Dockins, R., Hobor, A., Beringer, L., Dodds, J., Stewart, G., Blazy, S., Leroy, X.: Program Logics for Certified Compilers. CUP (2014)","DOI":"10.1017\/CBO9781107256552"},{"key":"22_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-642-03359-9_10","volume-title":"Theorem Proving in Higher Order Logics","author":"N. Benton","year":"2009","unstructured":"Benton, N., Kennedy, A., Varming, C.: Some domain theory and denotational semantics in Coq. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 115\u2013130. Springer, Heidelberg (2009)"},{"key":"22_CR3","unstructured":"Bishop, S., Fairbairn, M., Norrish, M., Sewell, P., Smith, M., Wansbrough, K.: TCP, UDP, and Sockets: Rigorous and experimentally-validated behavioural specification. volume 2: The specification. Technical Report 625, University of Cambridge Computer Laboratory (2005)"},{"key":"22_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-14052-5_13","volume-title":"Interactive Theorem Proving","author":"T. Braibant","year":"2010","unstructured":"Braibant, T., Pous, D.: An efficient Coq tactic for deciding Kleene algebras. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 163\u2013178. Springer, Heidelberg (2010)"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: The Bedrock structured programming system: Combining generative metaprogramming and Hoare logic in an extensible program verifier. In: ACM International Conference on Functional Programming, ICFP (2013)","DOI":"10.1145\/2500365.2500592"},{"issue":"10","key":"22_CR6","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/368924.368928","volume":"1","author":"M.E. Conway","year":"1958","unstructured":"Conway, M.E.: Proposal for an UNCOL. Communications of the ACM\u00a01(10), 5\u20138 (1958)","journal-title":"Communications of the ACM"},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"Jensen, J., Benton, N., Kennedy, A.: High-level separation logic for low-level code. In: ACM Symposium on Principles of Programming Languages, POPL (2013)","DOI":"10.1145\/2429069.2429105"},{"key":"22_CR8","doi-asserted-by":"crossref","unstructured":"Kennedy, A., Benton, N., Jensen, J., Dagand, P.: Coq: The world\u2019s best macro assembler? In: International Symposium on Principles and Practice of Declarative Programming, PPDP (2013)","DOI":"10.1145\/2505879.2505897"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: Sel4: Formal verification of an OS kernel. In: 22nd ACM Symposium on Operating Systems Principles, SOSP (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Koprowski, A., Binsztok, H.: TRX: A formally verified parser interpreter. Logical Methods in Computer Science\u00a07(2) (2011)","DOI":"10.2168\/LMCS-7(2:18)2011"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Owens, S.A., Norrish, M.: CakeML: A verified implementation of ML. In: ACM Symposium on Principles of Programming Languages, POPL (2014)","DOI":"10.1145\/2535838.2535841"},{"issue":"7","key":"22_CR12","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. Communications of the ACM\u00a052(7), 107\u2013115 (2009)","journal-title":"Communications of the ACM"},{"key":"22_CR13","doi-asserted-by":"crossref","unstructured":"Malecha, G., Morrisett, G., Shinnar, A., Wisnesky, R.: Toward a verified relational database management system. In: ACM Symposium on Principles of Programming Languages, POPL (2010)","DOI":"10.1145\/1706299.1706329"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Myreen, M.O.: Verified just-in-time compiler on x86. In: ACM Symposium on Principles of Programming Languages, POPL (2010)","DOI":"10.1145\/1706299.1706313"},{"key":"22_CR15","unstructured":"Myreen, M.O., Gordon, M.J.C.: Function extraction. Science of Computer Programming (2010)"},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"Myreen, M.O., Slind, K., Gordon, M.J.C.: Machine-code verification for multiple architectures - an application of decompilation into logic. In: Formal Methods in Computer-Aided Design, FMCAD (2008)","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: Reasoning with the awkward squad. In: ACM International Conference on Functional Programming, ICFP (2008)","DOI":"10.1145\/1411204.1411237"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: ACM Symposium on Principles of Programming Languages, POPL (2006)","DOI":"10.1145\/1111037.1111066"},{"key":"22_CR19","doi-asserted-by":"crossref","unstructured":"Sarkar, S., Sewell, P., Zappa Nardelli, F., Owens, S., Ridge, T., Braibant, T., Myreen, M.O., Alglave, J.: The semantics of x86-cc multiprocessor machine code. In: ACM Symposium on Principles of Programming Languages, POPL (2009)","DOI":"10.1145\/1480881.1480929"},{"key":"22_CR20","doi-asserted-by":"crossref","unstructured":"Strub, P.-Y., Swamy, N., Fournet, C., Chen, J.: Self-certification: Bootstrapping certified typecheckers in F* with Coq. In: ACM Symposium on Principles of Programming Languages, POPL (2012)","DOI":"10.1145\/2103656.2103723"},{"key":"22_CR21","unstructured":"Wisnesky, R., Malecha, G., Morrisett, G.: Certified web services in Ynot. In: International Workshop on Automated Specification and Verification of Web Systems, WWV (2009)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03542-0_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,14]],"date-time":"2023-02-14T09:15:48Z","timestamp":1676366148000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-03542-0_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319035413","9783319035420"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03542-0_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}