{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:03:35Z","timestamp":1773479015720,"version":"3.50.1"},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2023,8,18]],"date-time":"2023-08-18T00:00:00Z","timestamp":1692316800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,8,18]],"date-time":"2023-08-18T00:00:00Z","timestamp":1692316800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science,Japan","doi-asserted-by":"crossref","award":["KAKENHI 22H00520"],"award-info":[{"award-number":["KAKENHI 22H00520"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,9]]},"DOI":"10.1007\/s10817-023-09671-5","type":"journal-article","created":{"date-parts":[[2023,8,18]],"date-time":"2023-08-18T09:02:05Z","timestamp":1692349325000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Measure Construction by Extension in Dependent Type Theory with Application to Integration"],"prefix":"10.1007","volume":"67","author":[{"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[]},{"given":"Cyril","family":"Cohen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,8,18]]},"reference":[{"key":"9671_CR1","doi-asserted-by":"crossref","unstructured":"Abate, C., Haselwarter, P.G., Rivas, E., Muylder, A. V., Winterhalter, T., Hritcu, C., Maillard, K., Spitters, B.: SSProve: a foundational framework for modular cryptographic proofs in Coq. In: 34th IEEE Computer Security Foundations Symposium (CSF 2021), Dubrovnik, Croatia, June 21\u201325, 2021, pp 1\u201315. IEEE (2021)","DOI":"10.1109\/CSF51468.2021.00048"},{"key":"#cr-split#-9671_CR2.1","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Cohen, C., Kerjean, C., Mahboubi, A., Rouhling, D., Sakaguchi, K.: Competing inheritance paths in dependent type theory: a case study in functional analysis. In: 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June 29-July 6, vol. 12167","DOI":"10.1007\/978-3-030-51054-1_1"},{"key":"#cr-split#-9671_CR2.2","unstructured":"(2) of Lecture Notes in Artifical Intelligence, pp. 3-20. Springer (2020)"},{"issue":"1","key":"9671_CR3","first-page":"43","volume":"11","author":"R Affeldt","year":"2018","unstructured":"Affeldt, R., Cohen, C., Rouhling, D.: Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason. 11(1), 43\u201376 (2018)","journal-title":"J. Formaliz. Reason."},{"key":"9671_CR4","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Cohen, C., Saito, A.: Semantics of probabilistic programs using s-finite kernels in coq. In: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2023) Boston, MA, USA, January 16\u201317, 2023, pp. 3\u201316. ACM (2023)","DOI":"10.1145\/3573105.3575691"},{"key":"9671_CR5","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Garrigue, J., Nowak, D., Saikawa, T.: A trustful monad for axiomatic reasoning with probability and nondeterminism. J. Funct. Program. 31(E17) (2021)","DOI":"10.1017\/S0956796821000137"},{"issue":"3","key":"9671_CR6","first-page":"79","volume":"37","author":"R Affeldt","year":"2020","unstructured":"Affeldt, R., Garrigue, J., Saikawa, T.: Reasoning with conditional probabilities and joint distributions in Coq. Comput. Softw. 37(3), 79\u201395 (2020)","journal-title":"Comput. Softw."},{"key":"9671_CR7","unstructured":"Affeldt, R., Ishiguro, Y.: Formalization of the Lebesgue-Stieltjes measure in MathComp-Analysis. https:\/\/github.com\/math-comp\/analysis\/pull\/677, 2023. Pull request to [42]. Completed in (2022)"},{"key":"9671_CR8","unstructured":"Affeldt, R., Ishiguro, Y.: Formalization of the Radon-Nikod\u00fdm theorem in MathComp-Analysis. https:\/\/github.com\/math-comp\/analysis\/pull\/818, 2023. Pull request to [42]. Completed in (2022)"},{"key":"9671_CR9","doi-asserted-by":"crossref","unstructured":"Bancerek, G., Bylinski, C., Grabowski, A., Kornilowicz, A., Matuszewski, R., Naumowicz, A., Pa\u0327k, K.: The role of the Mizar Mathematical Library for interactive proof development in Mizar. J. Autom. Reason. 61(1\u20134), 9\u201332 (2018)","DOI":"10.1007\/s10817-017-9440-6"},{"key":"9671_CR10","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Gonthier, G., Biha, S. O., Pasca, I.: Canonical big operators. In: 21st International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2008), Montreal, Canada, August 18\u201321, 2008, volume 5170 of Lecture Notes in Computer Science, pp. 86\u2013101. Springer (2008)","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"9671_CR11","unstructured":"Bialas, J.: Properties of Caratheodor\u2019s measure. Technical report (1992). Formalized Mathematics 4"},{"key":"9671_CR12","unstructured":"Bialas, J.: The one-dimensional Lebesgue measure. Technical report (1995). Formalized Mathematics 7"},{"key":"9671_CR13","doi-asserted-by":"crossref","unstructured":"Boldo, S., Cl\u00e9ment, F., Martin, V., Mayero, M., Mouhcine, H.: A Coq formalization of Lebesgue induction principle and Tonelli\u2019s theorem. In: 25th International Symposium on Formal Methods (FM 2023), L\u00fcbeck, Germany, March 6\u201310, 2023, volume 14000 of Lecture Notes in Computer Science, pp 39\u201355. Springer (2023)","DOI":"10.1007\/978-3-031-27481-7_4"},{"issue":"2","key":"9671_CR14","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/s10817-021-09612-0","volume":"66","author":"S Boldo","year":"2021","unstructured":"Boldo, S., Cl\u00e9ment, F., Faissole, F., Martin, V., Mayero, M.: A Coq formalization of Lebesgue Integration of nonnegative functions. J. Autom. Reason. 66(2), 175\u2013213 (2021)","journal-title":"J. Autom. Reason."},{"key":"9671_CR15","unstructured":"Boldo, S., Cl\u00e9ment, F., Leclerc, L.: A Coq formalization of the Bochner integral (2022). arXiv cs.LO arXiv:2201.03242"},{"key":"9671_CR16","unstructured":"Cl\u00e9ment, F., Martin, V.: Lebesgue integration, detailed proofs to be formalized in Coq (2021). arXiv cs.LO arXiv:2101.05678"},{"key":"9671_CR17","unstructured":"Coble, A. R.: Anonymity, information, and machine-assisted proof. PhD thesis, University of Cambridge, King\u2019s College (2010). TR UCAM-CL-TR-785"},{"key":"9671_CR18","unstructured":"Cohen, C.: Formalized algebraic numbers: construction and first-order theory. PhD thesis, \u00c9cole Doctorale de l\u2019\u00c9cole Polytechnique, Laboratoire d\u2019Informatique de l\u2019\u00c9cole Polytechnique (2012)"},{"key":"9671_CR19","unstructured":"Cohen, C., Sakaguchi, K., Tassi, E.: Hierarchy Builder: Algebraic hierarchies made easy in Coq with Elpi (system description). In: 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), June 29\u2013July 6, 2020, Paris, France (Virtual Conference), vol. 167 of LIPIcs, pp. 34:1\u201334:21. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020)"},{"key":"9671_CR20","volume-title":"Implementing mathematics with the Nuprl proof development system","author":"RL Constable","year":"1986","unstructured":"Constable, R.L., Allen, S.F., Bromley, M., Cleaveland, R., Cremer, J.F., Harper, R., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementing mathematics with the Nuprl proof development system. Prentice Hall, Upper Saddle River (1986)"},{"key":"9671_CR21","doi-asserted-by":"crossref","unstructured":"Cruz-Filipe, L.: A constructive formalization of the fundamental theorem of calculus. In: Selected Papers of the Second International Workshop on Types for Proofs and Programs (TYPES 2002), Berg en Dal, The Netherlands, April 24\u201328, 2002, volume 2646 of Lecture Notes in Computer Science, pp. 108\u2013126. Springer (2002)","DOI":"10.1007\/3-540-39185-1_7"},{"key":"9671_CR22","doi-asserted-by":"crossref","unstructured":"Endou, N.: Reconstruction of the one-dimensional Lebesgue measure. Technical report, National Institute of Technology, Gifu College. Formalized Mathematics 28(1), 93\u2013104 (2020)","DOI":"10.2478\/forma-2020-0008"},{"key":"9671_CR23","doi-asserted-by":"crossref","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), Munich, Germany, August 17\u201320, 2009, volume 5674 of Lecture Notes in Computer Science, pp. 327\u2013342. Springer (2009)","DOI":"10.1007\/978-3-642-03359-9_23"},{"key":"9671_CR24","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S. L., Mahboubi, A., O\u2019Connor, R., Biha, S. O., Pasca, I., Rideau, L., Solovyev, A., Tassi, E., Th\u00e9ry, L.: A machine-checked proof of the odd order theorem. In: 4th International Conference on Interactive Theorem Proving (ITP 2013), Rennes, France, July 22\u201326, 2013, volume 7998 of Lecture Notes in Computer Science, pp 163\u2013179. Springer (2013)","DOI":"10.1007\/978-3-642-39634-2_14"},{"issue":"2","key":"9671_CR25","doi-asserted-by":"publisher","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. Reason. 50(2), 173\u2013190 (2013)","journal-title":"J. Autom. Reason."},{"key":"9671_CR26","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: Second International Conference on Interactive Theorem Proving (ITP 2011), Berg en Dal, The Netherlands, August 22\u201325, 2011, volume 6898 of Lecture Notes in Computer Science, pp 135\u2013151. Springer (2011)","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"9671_CR27","unstructured":"Hurd, J.: Formal verification of probabilistic algorithms. PhD thesis, University of Cambridge (2002). UCAM-CL-TR-566"},{"key":"9671_CR28","unstructured":"Ishiguro, Y., Affeldt, R.: A progress report on formalization of measure theory with MathComp-analysis. In: 25th Workshop on Programming and Programming Languages (PPL2023), Nagoya University, March 6\u20138, 2023. Japan Society for Software Science and Technology (2023)"},{"key":"9671_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-5361-0","volume-title":"Probability Theory: A Comprehensive Course","author":"A Klenke","year":"2014","unstructured":"Klenke, A.: Probability Theory: A Comprehensive Course, 2nd edn. Springer, New Year (2014)","edition":"2"},{"key":"9671_CR30","unstructured":"Le projet MILC. Numerical analysis in Coq. https:\/\/depot.lipn.univ-paris13.fr\/mayero\/coq-num-analysis, 2023. Since 2018. See also https:\/\/lipn.univ-paris13.fr\/MILC"},{"key":"9671_CR31","doi-asserted-by":"crossref","unstructured":"Lester, D. R.: Topology in PVS: Continuous mathematics with applications. In: 2nd Workshop on Automated Formal Methods (AFM 2007), pp. 11\u201320. Association for Computing Machinery (2007)","DOI":"10.1145\/1345169.1345171"},{"key":"9671_CR32","unstructured":"Li, D.: Int\u00e9gration et applications\u2014Cours et exercices corrig\u00e9s. Eyrolles (2016)"},{"key":"9671_CR33","unstructured":"Mathematical Components Team. Mathematical Components library. https:\/\/github.com\/math-comp\/math-comp, 2007. Last stable version: 2.0 (2023)"},{"key":"9671_CR34","unstructured":"Megill, N.: Metamath: A Computer Language for Mathematical Proofs. (2019). https:\/\/us.metamath.org\/downloads\/metamath.pdf. With extensive revisions by David A. Wheeler"},{"key":"9671_CR35","doi-asserted-by":"crossref","unstructured":"Mhamdi, T., Hasan, O., Tahar, S.: On the formalization of the Lebesgue integration theory in HOL. In: First International Conference on Interactive Theorem Proving (ITP 2010), Edinburgh, UK, July 11\u201314, 2010, volume 6172 of Lecture Notes in Computer Science, pp. 387\u2013402. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_27"},{"key":"9671_CR36","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J. M., Shankar, N.: PVS: A prototype verification system. In: 11th International Conference on Automated Deduction (CADE-11), Saratoga Springs, NY, USA, June 15\u201318, 1992, vol. 607 of Lecture Notes in Computer Science, pp. 748\u2013752. Springer (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"issue":"9","key":"9671_CR37","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"JM Rushby","year":"1998","unstructured":"Rushby, J.M., Owre, S., Shankar, N.: Subtypes for specifications: predicate subtyping in PVS. IEEE Trans. Softw. Eng. 24(9), 709\u2013720 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9671_CR38","unstructured":"Tassarotti, J., Tristan, J., Palmskog, K.: coq-proba: A probability theory library for the Coq theorem prover. https:\/\/github.com\/jtassarotti\/coq-proba, 2023. Since (2019)"},{"key":"9671_CR39","doi-asserted-by":"crossref","unstructured":"Tassarotti, J., Vajjha, K., Banerjee, A., Tristan, J.: A formal proof of PAC learnability for decision stumps. In: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021), Virtual Event, Denmark, January 17\u201319, 2021, pp. 5\u201317. ACM (2021)","DOI":"10.1145\/3437992.3439917"},{"key":"9671_CR40","unstructured":"The Agda Team. Agda\u2019s documentation v2.6.3, 2023. https:\/\/agda.readthedocs.io\/en\/v2.6.3"},{"key":"9671_CR41","unstructured":"The Coq Development Team. The Coq Proof Assistant Reference Manual. Inria, 2023. https:\/\/coq.inria.fr\/refman\/. Version 8.17.0"},{"key":"9671_CR42","unstructured":"The MathComp-Analysis Team. MathComp-Analysis: Mathematical components compliant analysis library. https:\/\/github.com\/math-comp\/analysis, 2023. Since 2017. Last stable version: 0.6.2. This paper refers to the branch hierarchy-builder"},{"key":"9671_CR43","unstructured":"The mathlib community. Lean mathematical components library. https:\/\/github.com\/leanprover-community\/mathlib 2023. Since (2017)"},{"key":"9671_CR44","unstructured":"The NASALib development team. NASA PVS library of formal developments. Current version: 7.1.1. https:\/\/github.com\/nasa\/pvslib. (2023)"},{"key":"9671_CR45","unstructured":"van Doorn, F.: Formalized Haar measure. In: 12th International Conference on Interactive Theorem Proving (ITP 2021) June 29\u2013July 1, 2021, Rome, Italy (Virtual Conference), volume 193 of LIPIcs, pp. 18:1\u201318:17. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021)"},{"key":"9671_CR46","unstructured":"Wiedijk, F.: Formalizing 100 theorems. http:\/\/www.cs.ru.nl\/~freek\/100 (2023)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09671-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-023-09671-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-023-09671-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,21]],"date-time":"2023-09-21T04:03:20Z","timestamp":1695269000000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-023-09671-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,18]]},"references-count":47,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2023,9]]}},"alternative-id":["9671"],"URL":"https:\/\/doi.org\/10.1007\/s10817-023-09671-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,8,18]]},"assertion":[{"value":"1 February 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 May 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 August 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflict of interest"}}],"article-number":"28"}}