{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T07:47:11Z","timestamp":1742802431024},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319431437"},{"type":"electronic","value":"9783319431444"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"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":[[2016]]},"DOI":"10.1007\/978-3-319-43144-4_15","type":"book-chapter","created":{"date-parts":[[2016,8,6]],"date-time":"2016-08-06T04:24:16Z","timestamp":1470457456000},"page":"235-251","source":"Crossref","is-referenced-by-count":9,"title":["A Formal Proof of Cauchy\u2019s Residue Theorem"],"prefix":"10.1007","author":[{"given":"Wenda","family":"Li","sequence":"first","affiliation":[]},{"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,8,7]]},"reference":[{"key":"15_CR1","volume-title":"Complex Analysis: An Introduction to the Theory of Analytic Funtions of One Complex Variable","author":"LV Ahlfors","year":"1966","unstructured":"Ahlfors, L.V.: Complex Analysis: An Introduction to the Theory of Analytic Funtions of One Complex Variable. McGraw-Hill, New York (1966)"},{"key":"15_CR2","unstructured":"Avigad, J., H\u00f6lzl, J., Serafin, L.: A formally verified proof of the central limit theorem. CoRR abs\/1405.7012 (2014)"},{"key":"15_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4419-7288-0","volume-title":"Complex Analysis","author":"J Bak","year":"2010","unstructured":"Bak, J., Newman, D.: Complex Analysis. Springer, New York (2010)"},{"key":"15_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-33099-2","volume-title":"Algorithms in Real Algebraic Geometry","author":"S Basu","year":"2006","unstructured":"Basu, S., Pollack, R., Roy, M.F.: Algorithms in Real Algebraic Geometry, vol. 10. Springer, Heidelberg (2006)"},{"issue":"1","key":"15_CR5","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/s11786-014-0181-1","volume":"9","author":"S Boldo","year":"2014","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41\u201362 (2014)","journal-title":"Math. Comput. Sci."},{"key":"15_CR6","unstructured":"Brunel, A.: Non-constructive complex analysis in Coq. In: 18th International Workshop on Types for Proofs and Programs, TYPES 2011, Bergen, Norway, pp. 1\u201315, 8\u201311 September 2011"},{"issue":"1","key":"15_CR7","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1090\/S0002-9939-1981-0589143-8","volume":"81","author":"FD Bruno Brosowski","year":"1981","unstructured":"Bruno Brosowski, F.D.: An elementary proof of the Stone-Weierstrass theorem. Proc. Am. Math. Soc. 81(1), 89\u201392 (1981)","journal-title":"Proc. Am. Math. Soc."},{"key":"15_CR8","volume-title":"Quantifier Elimination and Cylindrical Algebraic Decomposition","author":"B Caviness","year":"2012","unstructured":"Caviness, B., Johnson, J.: Quantifier Elimination and Cylindrical Algebraic Decomposition. Springer, New York (2012)"},{"key":"15_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-6313-5","volume-title":"Functions of One Complex Variable","author":"JB Conway","year":"1978","unstructured":"Conway, J.B.: Functions of One Complex Variable, vol. 11, 2nd edn. Springer, New York (1978)","edition":"2"},{"key":"15_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"88","DOI":"10.1007\/978-3-540-27818-4_7","volume-title":"Mathematical Knowledge Management","author":"L Cruz-Filipe","year":"2004","unstructured":"Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the constructive Coq repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 88\u2013103. Springer, Heidelberg (2004)"},{"key":"15_CR11","unstructured":"Hales, T.C., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., Nguyen, T.Q., Nipkow, T., Obua, S., Pleso, J., Rute, J., Solovyev, A., Ta, A.H.T., Tran, T.N., Trieu, D.T., Urban, J., Vu, K.K., Zumkeller, R.: A formal proof of the Kepler conjecture. arXiv:1501.02155 (2015)"},{"key":"15_CR12","unstructured":"Harrison, J.: Formalizing basic complex analysis. In: Matuszewski, R., Zalewska, A. (eds.) From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, vol. 10(23), pp. 151\u2013165. University of Bia\u0142ystok (2007)"},{"key":"15_CR13","doi-asserted-by":"crossref","first-page":"243","DOI":"10.1007\/s10817-009-9145-6","volume":"43","author":"J Harrison","year":"2009","unstructured":"Harrison, J.: Formalizing an analytic proof of the Prime Number Theorem (dedicated to Mike Gordon on the occasion of his 60th birthday). J. Autom. Reasoning 43, 243\u2013261 (2009)","journal-title":"J. Autom. Reasoning"},{"key":"15_CR14","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J Harrison","year":"2013","unstructured":"Harrison, J.: The HOL light theory of Euclidean space. J. Autom. Reasoning 50, 173\u2013190 (2013)","journal-title":"J. Autom. Reasoning"},{"key":"15_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-59273-7","volume-title":"Complex Analysis","author":"S Lang","year":"1993","unstructured":"Lang, S.: Complex Analysis. Springer, New York (1993)"},{"key":"15_CR16","volume-title":"Complex Analysis","author":"EM Stein","year":"2010","unstructured":"Stein, E.M., Shakarchi, R.: Complex Analysis, vol. 2. Princeton University Press, Princeton (2010)"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-43144-4_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,12]],"date-time":"2019-09-12T07:37:14Z","timestamp":1568273834000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-43144-4_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319431437","9783319431444"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-43144-4_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}