{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:08:30Z","timestamp":1725516510849},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_19","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T12:07:43Z","timestamp":1218542863000},"page":"173-181","source":"Crossref","is-referenced-by-count":2,"title":["Dependent Types, Theorem Proving, and Applications for a Verifying Compiler"],"prefix":"10.1007","author":[{"given":"Yves","family":"Bertot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","doi-asserted-by":"crossref","unstructured":"Augustsson, L.: Cayenne - a language with dependent types. In: International Conference on Functional Programming, pp. 239\u2013250 (1998)","DOI":"10.1145\/291251.289451"},{"issue":"2","key":"19_CR2","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0167-6423(92)90005-V","volume":"19","author":"G. Berry","year":"1992","unstructured":"Berry, G., Gonthier, G.: The esterel synchronous programming language: Design, semantics, implementation. Science of Computer Programming\u00a019(2), 87\u2013152 (1992)","journal-title":"Science of Computer Programming"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-44585-4_3","volume-title":"Computer Aided Verification","author":"Y. Bertot","year":"2001","unstructured":"Bertot, Y.: Formalizing a jvml verifier for initialization in a theorem prover. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 14\u201324. Springer, Heidelberg (2001)"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/11417170_9","volume-title":"Typed Lambda Calculi and Applications","author":"Y. Bertot","year":"2005","unstructured":"Bertot, Y.: Filters on coinductive streams, an application to Eratosthenes\u2019 sieve. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol.\u00a03461, pp. 102\u2013115. Springer, Heidelberg (2005)"},{"key":"19_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development, Coq\u2019Art:the Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development, Coq\u2019Art:the Calculus of Inductive Constructions. Springer, Heidelberg (2004)"},{"issue":"3\u20134","key":"19_CR6","doi-asserted-by":"publisher","first-page":"225","DOI":"10.1023\/A:1021987403425","volume":"22","author":"Y. Bertot","year":"2002","unstructured":"Bertot, Y., Magaud, N., Zimmermann, P.: A proof of GMP square root. Journal of Automated Reasoning\u00a022(3\u20134), 225\u2013252 (2002)","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/3-540-44755-5_13","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Daumas","year":"2001","unstructured":"Daumas, M., Rideau, L., Th\u00e9ry, L.: A generic library of floating-point numbers and its application to exact computing. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 169\u2013184. Springer, Heidelberg (2001)"},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/3-540-44659-1_24","volume-title":"Theorem Proving in Higher Order Logics","author":"P. Letouzey","year":"2000","unstructured":"Letouzey, P., Th\u00e9ry, L.: Formalizing St\u00e5lmarck\u2019s algorithm in Coq. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol.\u00a01869, pp. 387\u2013404. Springer, Heidelberg (2000)"},{"issue":"5-6","key":"19_CR9","doi-asserted-by":"publisher","first-page":"607","DOI":"10.1016\/S0747-7171(06)80007-6","volume":"15","author":"C. Paulin-Mohring","year":"1993","unstructured":"Paulin-Mohring, C., Werner, B.: Synthesis of ML programs in the system Coq. Journal of Symbolic Computation\u00a015(5-6), 607\u2013640 (1993)","journal-title":"Journal of Symbolic Computation"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/3-540-44755-5_24","volume-title":"Theorem Proving in Higher Order Logics","author":"D. Pichardie","year":"2001","unstructured":"Pichardie, D., Bertot, Y.: Formalizing convex hull algorithms. In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol.\u00a02152, pp. 346\u2013361. Springer, Heidelberg (2001)"},{"key":"19_CR11","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1023\/A:1026518331905","volume":"26","author":"L. Th\u00e9ry","year":"2001","unstructured":"Th\u00e9ry, L.: A machine-checked implementation of Buchberger\u2019s algorithm. Journal of Automated Reasoning\u00a026, 107\u2013137 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10930755_20","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Th\u00e9ry","year":"2003","unstructured":"Th\u00e9ry, L.: Proving pearl: Knuth\u2019s algorithm for prime numbers. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, Springer, Heidelberg (2003)"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Xi, H., Pfenning, F.: Dependent types in practical programming. In: Conference Record of POPL 1999: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Antonio, Texas, pp. 214\u2013227 (1999)","DOI":"10.1145\/292540.292560"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T03:42:33Z","timestamp":1557718953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}