{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T20:01:45Z","timestamp":1781899305065,"version":"3.54.5"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642031526","type":"print"},{"value":"9783642031533","type":"electronic"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009]]},"DOI":"10.1007\/978-3-642-03153-3_4","type":"book-chapter","created":{"date-parts":[[2009,7,27]],"date-time":"2009-07-27T02:11:14Z","timestamp":1248660674000},"page":"153-194","source":"Crossref","is-referenced-by-count":10,"title":["Structural Abstract Interpretation: A Formal Study Using Coq"],"prefix":"10.1007","author":[{"given":"Yves","family":"Bertot","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"B. Aydemir","year":"2005","unstructured":"Aydemir, B., Bohannon, A., Fairbairn, M., Foster, J., Pierce, B., Sewell, P., Vytiniotis, D., Washburn, G., Weirich, S., Zdancewic, S.: Mechanized metatheory for the masses: The POPLmark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol.\u00a03603, pp. 50\u201365. Springer, Heidelberg (2005)"},{"key":"4_CR2","unstructured":"Bertot, Y.: Theorem proving support in programming language semantics. Technical Report 6242, INRIA (2007); to appear in a book in memory of Gilles Kahn"},{"key":"4_CR3","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)"},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11617990_5","volume-title":"Types for Proofs and Programs","author":"Y. Bertot","year":"2006","unstructured":"Bertot, Y., Gr\u00e9goire, B., Leroy, X.: A structured approach to proving compiler optimizations based on dataflow analysis. In: Filli\u00e2tre, J.-C., Paulin-Mohring, C., Werner, B. (eds.) TYPES 2004. LNCS, vol.\u00a03839, pp. 66\u201381. Springer, Heidelberg (2006)"},{"issue":"3","key":"4_CR5","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/j.tcs.2006.08.012","volume":"364","author":"F. Besson","year":"2006","unstructured":"Besson, F., Jensen, T., Pichardie, D.: Proof-carrying code from certified abstract interpretation and fixpoint compression. Theoretical Computer Science\u00a0364(3), 273\u2013291 (2006)","journal-title":"Theoretical Computer Science"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/11813040_31","volume-title":"FM 2006: Formal Methods","author":"S. Blazy","year":"2006","unstructured":"Blazy, S., Dargaye, Z., Leroy, X.: Formal verification of a C compiler front-end. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 460\u2013475. Springer, Heidelberg (2006)"},{"key":"4_CR7","first-page":"238","volume-title":"Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, POPL 1977","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: Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, POPL 1977, pp. 238\u2013252. ACM Press, New York (1977)"},{"key":"4_CR8","doi-asserted-by":"publisher","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., Min\u00e9, A., Mauborgne, L., Monniaux, D., Rival, X.: The ASTRE\u00c9 analyzer. In: Sagiv, M. (ed.) ESOP 2005, vol.\u00a03444, pp. 21\u201330. Springer, Heidelberg (2005)"},{"key":"4_CR9","volume-title":"A discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A discipline of Programming. Prentice Hall, Englewood Cliffs (1976)"},{"key":"4_CR10","first-page":"42","volume-title":"33rd symposium Principles of Programming Languages","author":"X. Leroy","year":"2006","unstructured":"Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: 33rd symposium Principles of Programming Languages, pp. 42\u201354. ACM Press, New York (2006)"},{"key":"4_CR11","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":"4_CR12","doi-asserted-by":"crossref","unstructured":"Pichardie, D.: Building certified static analysers by modular construction of well-founded lattices. In: Proc. of the 1st International Conference on Foundations of Informatics, Computing and Software (FICS 2008). Electronic Notes in Theoretical Computer Science (2008)","DOI":"10.1016\/j.entcs.2008.04.064"},{"key":"4_CR13","unstructured":"The Coq development team. The coq proof assistant (2008), \n                  \n                    http:\/\/coq.inria.fr"}],"container-title":["Lecture Notes in Computer Science","Language Engineering and Rigorous Software Development"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03153-3_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T02:10:54Z","timestamp":1552097454000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03153-3_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642031526","9783642031533"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03153-3_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009]]}}}