{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:13:05Z","timestamp":1763467985146},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_3","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"9-24","source":"Crossref","is-referenced-by-count":18,"title":["A Certified Denotational Abstract Interpreter"],"prefix":"10.1007","author":[{"given":"David","family":"Cachera","sequence":"first","affiliation":[]},{"given":"David","family":"Pichardie","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"115","DOI":"10.1007\/978-3-642-03359-9_10","volume-title":"Proc. of TPHOLs \u201909","author":"N. Benton","year":"2009","unstructured":"Benton, N., Kennedy, A., Varming, C.: Some domain theory and denotational semantics in Coq. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 115\u2013130. Springer, Heidelberg (2009)"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-642-03153-3_4","volume-title":"Language Engineering and Rigorous Software Development","author":"Y. Bertot","year":"2009","unstructured":"Bertot, Y.: Structural abstract interpretation, a formal study in Coq. In: Bove, A., Barbosa, L.S., Pardo, A., Pinto, J.S. (eds.) ALFA. LNCS, vol.\u00a05520, pp. 153\u2013194. Springer, Heidelberg (2009)"},{"issue":"3","key":"3_CR3","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S. Blazy","year":"2009","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reasoning\u00a043(3), 263\u2013288 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR4","unstructured":"Cousot, P.: Visiting Professor at the MIT Aeronautics and Astronautics Department, Course 16.399: Abstract Interpretation"},{"key":"3_CR5","series-title":"NATO ASI Series F","volume-title":"Calculational System Design","author":"P. Cousot","year":"1999","unstructured":"Cousot, P.: The calculational design of a generic abstract interpreter. In: Broy, M., Steinbr\u00fcggen, R. (eds.) Calculational System Design. NATO ASI Series F. IOS Press, Amsterdam (1999)"},{"key":"3_CR6","first-page":"238","volume-title":"Proc. of POPL\u201977","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. of POPL\u201977, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"21","DOI":"10.1007\/978-3-540-31987-0_3","volume-title":"Programming Languages and Systems","author":"P. Cousot","year":"2005","unstructured":"Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The ASTR\u00c9E analyser. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"3_CR8","first-page":"387","volume-title":"Current Trends in Hardware Verfication and Automatic Theorem Proving","author":"M.J.C. Gordon","year":"1988","unstructured":"Gordon, M.J.C.: Mechanizing programming logics in higher-order logic. In: Current Trends in Hardware Verfication and Automatic Theorem Proving, pp. 387\u2013439. Springer, Heidelberg (1988)"},{"key":"3_CR9","unstructured":"Leroy, X.: Mechanized semantics, with applications to program proof and compiler verification, lecture given at the, Marktoberdorf summer school (2009)"},{"key":"3_CR10","first-page":"42","volume-title":"Proc. of POPL\u201906","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: Proc. of POPL\u201906, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"3_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-540-24725-8_2","volume-title":"Programming Languages and Systems","author":"A. Min\u00e9","year":"2004","unstructured":"Min\u00e9, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol.\u00a02986, pp. 3\u201317. Springer, Heidelberg (2004)"},{"key":"3_CR12","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/s001650050009","volume":"10","author":"T. Nipkow","year":"1998","unstructured":"Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics textbook. Formal Aspects of Computing\u00a010, 171\u2013186 (1998)","journal-title":"Formal Aspects of Computing"},{"key":"3_CR13","unstructured":"Pichardie, D.: Interpr\u00e9tation abstraite en logique intuitionniste\u00a0: extraction d\u2019analyseurs Java certifi\u00e9s. PhD thesis, Universit\u00e9 Rennes\u00a01 (2005) (in french)"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Pichardie, D.: Building certified static analysers by modular construction of well-founded lattices. In: Proc. of FICS\u201908. ENTCS, vol.\u00a0212, pp. 225\u2013239 (2008)","DOI":"10.1016\/j.entcs.2008.04.064"},{"key":"3_CR15","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.jlap.2004.03.009","volume":"60-61","author":"G.D. Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming\u00a060-61, 17\u2013139 (2004)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst.\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275501"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:17:24Z","timestamp":1619785044000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}