{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:52:50Z","timestamp":1760043170430,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":89,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,4,15]],"date-time":"2024-04-15T00:00:00Z","timestamp":1713139200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-2100015"],"award-info":[{"award-number":["CNS-2100015"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,4,15]]},"DOI":"10.1145\/3643991.3644908","type":"proceedings-article","created":{"date-parts":[[2024,7,2]],"date-time":"2024-07-02T13:05:13Z","timestamp":1719925513000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Thirty-Three Years of Mathematicians and Software Engineers: A Case Study of Domain Expertise and Participation in Proof Assistant Ecosystems"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-8694-3422","authenticated-orcid":false,"given":"Gwenyth","family":"Lincroft","sequence":"first","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-6170-6033","authenticated-orcid":false,"given":"Minsung","family":"Cho","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4397-1635","authenticated-orcid":false,"given":"Katherine","family":"Hough","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-0022-9611","authenticated-orcid":false,"given":"Mahsa","family":"Bazzaz","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1187-9298","authenticated-orcid":false,"given":"Jonathan","family":"Bell","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,7,2]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.3189\/S0022143000022401"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503951"},{"key":"e_1_3_2_1_3_1","volume-title":"FASE 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2--8, 2016, Proceedings 19","author":"Aspinall David","year":"2016","unstructured":"David Aspinall and Cezary Kaliszyk. 2016. Towards formal proof metrics. In Fundamental Approaches to Software Engineering: 19th International Conference, FASE 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2--8, 2016, Proceedings 19. Springer, 325--341."},{"key":"e_1_3_2_1_4_1","first-page":"1","article-title":"Theorem proving in Lean","volume":"3","author":"Avigad Jeremy","year":"2015","unstructured":"Jeremy Avigad, Leonardo de Moura, and Soonho Kong. 2015. Theorem proving in Lean. Release 3, 0 (2015), 1--4.","journal-title":"Release"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2630417.2630418"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(80)90092-4"},{"key":"e_1_3_2_1_7_1","volume-title":"G\u00f6del's God in Isabelle\/HOL. Archive of Formal Proofs 2013","author":"Benzm\u00fcller Christoph","year":"2013","unstructured":"Christoph Benzm\u00fcller and B Woltzenlogel Paleo. 2013. G\u00f6del's God in Isabelle\/HOL. Archive of Formal Proofs 2013 (2013)."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20297-6_25"},{"volume-title":"Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions","author":"Bertot Yves","key":"e_1_3_2_1_9_1","unstructured":"Yves Bertot and Pierre Cast\u00e9ran. 2013. Interactive theorem proving and program development: Coq'Art: the calculus of inductive constructions. Springer Science & Business Media."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-20615-8_1"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473139"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1753235.1753251"},{"key":"e_1_3_2_1_13_1","unstructured":"Buzzard Kevin and Pedramfar Mohammad. 2019. The Natural Number Game. https:\/\/www.ma.imperial.ac.uk\/~buzzard\/xena\/natural_number_game\/."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.77"},{"key":"e_1_3_2_1_15_1","unstructured":"Thomas Claburn. 2021. Realizing this is getting out of hand Coq mulls new name for programming language. https:\/\/www.theregister.com\/2021\/06\/15\/coq_programming_language_change\/."},{"key":"e_1_3_2_1_16_1","volume-title":"Cubical type theory: a constructive interpretation of the univalence axiom. arXiv preprint arXiv:1611.02108","author":"Cohen Cyril","year":"2016","unstructured":"Cyril Cohen, Thierry Coquand, Simon Huber, and Anders M\u00f6rtberg. 2016. Cubical type theory: a constructive interpretation of the univalence axiom. arXiv preprint arXiv:1611.02108 (2016)."},{"key":"e_1_3_2_1_17_1","unstructured":"The Lean Community. 2020. Lean Theorem Prover. https:\/\/github.com\/leanprover\/lean."},{"key":"e_1_3_2_1_18_1","unstructured":"The Lean Community. 2023. Lean 4. https:\/\/github.com\/leanprover\/lean4."},{"key":"e_1_3_2_1_19_1","unstructured":"The Lean Community. 2023. Lean Theorem Prover - Fork. https:\/\/github.com\/leanprover-community\/lean."},{"key":"e_1_3_2_1_20_1","unstructured":"Microsoft Corporation. 2023. Lean. https:\/\/www.microsoft.com\/en-us\/research\/project\/lean\/."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/HICSS.2006.101"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5334\/jors.bt"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/299157.299167"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2018.04.005"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE43902.2021.00098"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0001-5"},{"key":"e_1_3_2_1_27_1","first-page":"653","article-title":"CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels","volume":"16","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels.. In OSDI, Vol. 16. 653--669.","journal-title":"OSDI"},{"key":"e_1_3_2_1_28_1","volume-title":"John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al.","author":"Hales Thomas","year":"2017","unstructured":"Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Hoang Le Truong, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, et al. 2017. A formal proof of the Kepler conjecture. In Forum of mathematics, Pi, Vol. 5. Cambridge University Press, e2."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1093\/reseval\/rvv014"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439922"},{"key":"e_1_3_2_1_31_1","unstructured":"INRIA. 2023. Coq Package Index. https:\/\/coq.inria.fr\/opam\/www\/."},{"key":"e_1_3_2_1_32_1","unstructured":"Inria CNRS. 2023. coq-club - The Coq mailing list. https:\/\/sympa.inria.fr\/sympa\/info\/coq-club."},{"key":"e_1_3_2_1_33_1","unstructured":"Inria CNRS and Contributors. 2021. Early history of Coq. https:\/\/coq.inria.fr\/refman\/history.html."},{"key":"e_1_3_2_1_34_1","unstructured":"Inria CNRS and Contributors. 2021. Install Coq. https:\/\/coq.inria.fr\/download."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2025113.2025127"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.23"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1922649.1922658"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-021-09604-0"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICGSE.2017.11"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.6084\/m9.figshare.24582858.v1"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","unstructured":"Assia Mahboubi and Enrico Tassi. 2022. Mathematical Components. Zenodo. 10.5281\/zenodo.7118596","DOI":"10.5281\/zenodo.7118596"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_1_45_1","unstructured":"The mathlib Community. 2023. Lean mathlib. https:\/\/github.com\/leanprover-community\/mathlib\/."},{"key":"e_1_3_2_1_46_1","unstructured":"The mathlib Community. 2023. Lean mathlib4. https:\/\/github.com\/leanprover-community\/mathlib4\/."},{"key":"e_1_3_2_1_47_1","unstructured":"MathWorks. 2023. Company Overview. https:\/\/www.mathworks.com\/content\/dam\/mathworks\/fact-sheet\/2023-company-factsheet-8-5\u00d711-8282v23.pdf."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/MSR.2019.00069"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/567793.567795"},{"volume-title":"The basic practice of statistics","author":"Moore David S","key":"e_1_3_2_1_50_1","unstructured":"David S Moore and Stephane Kirkland. 2007. The basic practice of statistics. Vol. 2. WH Freeman New York."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/512035.512055"},{"key":"e_1_3_2_1_52_1","volume-title":"A survey on theorem provers in formal methods. arXiv preprint arXiv:1912.03028","author":"Nawaz M Saqib","year":"2019","unstructured":"M Saqib Nawaz, Moin Malik, Yi Li, Meng Sun, and M Lali. 2019. A survey on theorem provers in formal methods. arXiv preprint arXiv:1912.03028 (2019)."},{"volume-title":"A formalization of dynamic epistemic logic. Ph. D. Dissertation. Master's thesis","author":"Neeley Paula","key":"e_1_3_2_1_53_1","unstructured":"Paula Neeley. 2021. A formalization of dynamic epistemic logic. Ph. D. Dissertation. Master's thesis, Carnegie Mellon University."},{"volume-title":"a proof assistant for higher-order logic","author":"Nipkow Tobias","key":"e_1_3_2_1_54_1","unstructured":"Tobias Nipkow, Markus Wenzel, and Lawrence C Paulson. 2002. Isabelle\/HOL: a proof assistant for higher-order logic. Springer."},{"key":"e_1_3_2_1_55_1","volume-title":"Gerosa","author":"Oliva Gustavo A.","year":"2012","unstructured":"Gustavo A. Oliva, Francisco W. Santana, Kleverton C. M. de Oliveira, Cleidson R. B. de Souza, and Marco A. Gerosa. 2012. Characterizing Key Developers: A Case Study with Apache Ant. In Collaboration and Technology, Valeria Herskovic, H. Ulrich Hoppe, Marc Jansen, and J\u00fcrgen Ziegler (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 97--112."},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(86)90015-4"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606557"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2016.68"},{"key":"e_1_3_2_1_59_1","volume-title":"Homotopy type theory: Univalent foundations of mathematics. arXiv preprint arXiv:1308.0729","author":"Foundations Program The Univalent","year":"2013","unstructured":"The Univalent Foundations Program. 2013. Homotopy type theory: Univalent foundations of mathematics. arXiv preprint arXiv:1308.0729 (2013)."},{"key":"e_1_3_2_1_60_1","unstructured":"Python Software Foundation. 2023. The Python Package Index: scipy. https:\/\/pypi.org\/project\/scipy\/."},{"key":"e_1_3_2_1_61_1","doi-asserted-by":"publisher","unstructured":"Ayushi Rastogi and Nachiappan Nagappan. 2016. Forking and the Sustainability of the Developer Community Participation - An Empirical Investigation on Outcomes and Reasons. In 2016 IEEE 23rd International Conference on Software Analysis Evolution and Reengineering (SANER) Vol. 1. 102--111. 10.1109\/SANER.2016.27","DOI":"10.1109\/SANER.2016.27"},{"key":"e_1_3_2_1_62_1","first-page":"1473","article-title":"A mechanically assisted examination of begging the question in Anselm's Ontological Argument","volume":"5","author":"Rushby John","year":"2018","unstructured":"John Rushby. 2018. A mechanically assisted examination of begging the question in Anselm's Ontological Argument. Journal of Applied Logics---IFCoLog Journal of Logics and their Applications 5, 7 (2018), 1473--1497.","journal-title":"Journal of Applied Logics---IFCoLog Journal of Logics and their Applications"},{"key":"e_1_3_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1080\/10586458.2021.1926016"},{"key":"e_1_3_2_1_64_1","unstructured":"Jonas Sch\u00f6pf and Stephanie Widauer. 2018. History of Interactive Theorem Proving. (2018)."},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/253228.253248"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","unstructured":"Ilya Sergey. 2014. Programs and Proofs: Mechanizing Mathematics with Dependent Types. Lecture notes with exercises. 10.5281\/zenodo.4996238","DOI":"10.5281\/zenodo.4996238"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-12-803459-0.00009-1"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2675133.2675215"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2018.110162131"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/RSSE.2012.6233413"},{"key":"e_1_3_2_1_71_1","unstructured":"Nicolas Tabareau and Th\u00e9o Zimmermann. 2024. Roadmap for the Coq Project #069. https:\/\/github.com\/coq\/ceps\/blob\/coq-roadmap\/text\/069-coq-roadmap.md#change-of-name-coq---the-rocq-prover."},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00064"},{"key":"e_1_3_2_1_73_1","unstructured":"The Coq Development Team. 2023. The Coq Proof Assistant. https:\/\/github.com\/coq\/coq."},{"key":"e_1_3_2_1_74_1","unstructured":"The Sage Development Team. 2023. SageMath. https:\/\/github.com\/sagemath\/sage."},{"key":"e_1_3_2_1_75_1","volume-title":"On proof and progress in mathematics. Bulletin of the American mathematical Society 30, 2","author":"Thurston William P","year":"1994","unstructured":"William P Thurston. 1994. On proof and progress in mathematics. Bulletin of the American mathematical Society 30, 2 (1994), 161--177."},{"key":"e_1_3_2_1_76_1","volume-title":"Technische Universitaet Muenchen, and Contributors","author":"University of Cambridge","year":"2022","unstructured":"University of Cambridge, Technische Universitaet Muenchen, and Contributors. 2022. Isabelle. https:\/\/isabelle.in.tum.de\/."},{"key":"e_1_3_2_1_77_1","volume-title":"Technische Universitaet Muenchen, and Contributors","author":"University of Cambridge","year":"2023","unstructured":"University of Cambridge, Technische Universitaet Muenchen, and Contributors. 2023. Archive of Formal Proofs. https:\/\/www.isa-afp.org\/."},{"key":"e_1_3_2_1_78_1","volume-title":"Technische Universitaet Muenchen, and Contributors","author":"University of Cambridge","year":"2023","unstructured":"University of Cambridge, Technische Universitaet Muenchen, and Contributors. 2023. The Archive of Formal Proofs. https:\/\/github.com\/isabelle-prover\/mirror-afp-devel."},{"key":"e_1_3_2_1_79_1","volume-title":"Technische Universitaet Muenchen, and Contributors","author":"University of Cambridge","year":"2023","unstructured":"University of Cambridge, Technische Universitaet Muenchen, and Contributors. 2023. The Isabelle Repository. https:\/\/github.com\/isabelle-prover\/mirror-isabelle."},{"key":"e_1_3_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/1842752.1842781"},{"key":"e_1_3_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_16"},{"key":"e_1_3_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575688"},{"key":"e_1_3_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1038\/s41592-019-0686-2"},{"key":"e_1_3_2_1_84_1","first-page":"11","article-title":"Formal Proof --- Getting Started","volume":"55","author":"Wiedijk Freek","year":"2008","unstructured":"Freek Wiedijk. 2008. Formal Proof --- Getting Started. Notices of the American Mathematical Society 55, 11 (December 2008), 1408--1414.","journal-title":"Notices of the American Mathematical Society"},{"key":"e_1_3_2_1_85_1","unstructured":"Freek Wiedijk. 2023. Formalizing 100 Theorems. https:\/\/www.cs.ru.nl\/~freek\/100\/."},{"key":"e_1_3_2_1_86_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSME.2016.13"},{"key":"e_1_3_2_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_1_89_1","volume-title":"25th International Conference on Software Engineering, 2003. Proceedings. IEEE, 419--429","author":"Ye Yunwen","year":"2003","unstructured":"Yunwen Ye and Kouichi Kishida. 2003. Toward an understanding of the motivation of open source software developers. In 25th International Conference on Software Engineering, 2003. Proceedings. IEEE, 419--429."},{"key":"e_1_3_2_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380412"}],"event":{"name":"MSR '24: 21st International Conference on Mining Software Repositories","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","IEEE CS"],"location":"Lisbon Portugal","acronym":"MSR '24"},"container-title":["Proceedings of the 21st International Conference on Mining Software Repositories"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3643991.3644908","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3643991.3644908","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3643991.3644908","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T23:56:44Z","timestamp":1750291004000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3643991.3644908"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,15]]},"references-count":89,"alternative-id":["10.1145\/3643991.3644908","10.1145\/3643991"],"URL":"https:\/\/doi.org\/10.1145\/3643991.3644908","relation":{},"subject":[],"published":{"date-parts":[[2024,4,15]]},"assertion":[{"value":"2024-07-02","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}