{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:26:50Z","timestamp":1772119610132,"version":"3.50.1"},"reference-count":55,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,8,14]],"date-time":"2024-08-14T00:00:00Z","timestamp":1723593600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,8,14]],"date-time":"2024-08-14T00:00:00Z","timestamp":1723593600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100006919","name":"Massachusetts Institute of Technology","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100006919","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":[[2024,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We address the challenges of scaling verification efforts to match the increasing complexity and size of systems. We propose a research agenda aimed at building a performant proof engine by studying the asymptotic performance of proof engines and redesigning their building blocks. As a case study, we explore equational rewriting and introduce a novel prototype proof engine building block for rewriting in Coq, utilizing proof by reflection for enhanced performance. Our prototype implementation can significantly improve the development of verified compilers, as demonstrated in a case study with the Fiat Cryptography toolchain. The resulting extracted command-line compiler is about 1000\n                    <jats:inline-formula>\n                      <jats:alternatives>\n                        <jats:tex-math>$$\\times $$<\/jats:tex-math>\n                        <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                          <mml:mo>\u00d7<\/mml:mo>\n                        <\/mml:math>\n                      <\/jats:alternatives>\n                    <\/jats:inline-formula>\n                    faster while featuring simpler compiler-specific proofs. This work lays some foundation for scaling verification efforts and contributes to the broader goal of developing a proof engine with good asymptotic performance, ultimately aimed at enabling the verification of larger and more complex systems.\n                  <\/jats:p>","DOI":"10.1007\/s10817-024-09705-6","type":"journal-article","created":{"date-parts":[[2024,8,14]],"date-time":"2024-08-14T12:02:26Z","timestamp":1723636946000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Towards a Scalable Proof Engine: A\u00a0Performant Prototype Rewriting Primitive for Coq"],"prefix":"10.1007","volume":"68","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9427-4891","authenticated-orcid":false,"given":"Jason","family":"Gross","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9854-7500","authenticated-orcid":false,"given":"Andres","family":"Erbsen","sequence":"additional","affiliation":[]},{"given":"Jade","family":"Philipoom","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7617-9180","authenticated-orcid":false,"given":"Rajashree","family":"Agrawal","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,8,14]]},"reference":[{"key":"9705_CR1","doi-asserted-by":"publisher","unstructured":"Aehlig, K., Haftmann, F., Nipkow, T.: A compiled implementation of normalization by evaluation. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) Theorem Proving in Higher Order Logics, pp. 39\u201354. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_8","DOI":"10.1007\/978-3-540-71067-7_8"},{"key":"9705_CR2","doi-asserted-by":"crossref","unstructured":"Aydemir, B., Chargu\u00e9raud, A., Pierce, B.C., Pollack, R., Weirich, S.: Engineering formal metatheory. In: Proc. POPL, pp. 3\u201315 (2008). https:\/\/www.cis.upenn.edu\/~bcpierce\/papers\/binders.pdf","DOI":"10.1145\/1328897.1328443"},{"key":"9705_CR3","volume-title":"A Gift of Fire: Social, Legal, and Ethical Issues for Computing Technology","author":"S Baase","year":"2012","unstructured":"Baase, S., Henry, T.: A Gift of Fire: Social, Legal, and Ethical Issues for Computing Technology, 5th edn. Pearson, London (2012)","edition":"5"},{"key":"9705_CR4","doi-asserted-by":"publisher","unstructured":"Berger, U., Schwichtenberg, H.: An inverse of the evaluation functional for typed $$\\lambda $$-calculus. In: Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp. 203\u2013211 (1991). https:\/\/doi.org\/10.1109\/LICS.1991.151645","DOI":"10.1109\/LICS.1991.151645"},{"key":"9705_CR5","doi-asserted-by":"publisher","unstructured":"Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Altenkirch, T., McBride, C. (eds.) Types for Proofs and Programs, pp. 48\u201362. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-74464-1_4","DOI":"10.1007\/978-3-540-74464-1_4"},{"key":"9705_CR6","doi-asserted-by":"publisher","unstructured":"Boespflug, M., D\u00e9n\u00e8s, M., Gr\u00e9goire, B.: Full reduction at full throttle. In: Proceedings of the First International Conference on Certified Programs and Proofs. CPP\u201911, pp. 362\u2013377. Springer, Berlin, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_26","DOI":"10.1007\/978-3-642-25379-9_26"},{"key":"9705_CR7","unstructured":"Boespflug, M.: Efficient normalization by evaluation. In: Danvy, O. (ed.) Workshop on Normalization by Evaluation, Los Angeles, USA (2009). https:\/\/hal.inria.fr\/inria-00434283"},{"key":"9705_CR8","doi-asserted-by":"publisher","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Abadi, M., Ito, T. (eds.) Theoretical Aspects of Computer Software, pp. 515\u2013529. Springer, New York. https:\/\/doi.org\/10.1007\/BFb0014565","DOI":"10.1007\/BFb0014565"},{"key":"9705_CR9","doi-asserted-by":"publisher","unstructured":"Braibant, T., Pous, D.: Tactics for reasoning modulo AC in Coq. In: Jouannaud, J.-P., Shao, Z. (eds.) Certified Programs and Proofs, pp. 167\u2013182. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_14","DOI":"10.1007\/978-3-642-25379-9_14"},{"key":"9705_CR10","doi-asserted-by":"publisher","unstructured":"Chaieb, A., Nipkow, T.: Verifying and reflecting quantifier elimination for presburger arithmetic. In: Sutcliffe, G., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 367\u2013380. Springer, Berlin (2005). https:\/\/doi.org\/10.1007\/11591191_26","DOI":"10.1007\/11591191_26"},{"key":"9705_CR11","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Parametric higher-order abstract syntax for mechanized semantics. In: ICFP\u201908: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, Victoria, British Columbia, Canada (2008). http:\/\/adam.chlipala.net\/papers\/PhoasICFP08\/","DOI":"10.1145\/1411204.1411226"},{"key":"9705_CR12","doi-asserted-by":"publisher","unstructured":"Claret, G., del Carmen Gonz\u00e1lez\u00a0Huesca, L., R\u00e9gis-Gianas, Y., Ziliani, B.: Lightweight proof by reflection using a posteriori simulation of effectful computation. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) Interactive Theorem Proving, pp. 67\u201383. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_8","DOI":"10.1007\/978-3-642-39634-2_8"},{"key":"9705_CR13","unstructured":"Coulter, M., Bensinger, G.: Alphabet shares dive after google AI Chatbot Bard Flubs Answer in ad, Reuters (2023). Accessed 24 Apr 2023. https:\/\/www.reuters.com\/technology\/google-ai-chatbot-bard-offers-inaccurate-information-company-ad-2023-02-08\/"},{"key":"9705_CR14","doi-asserted-by":"publisher","unstructured":"De\u00a0Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. In: Indagationes Mathematicae (Proceedings), vol. 75, pp. 381\u2013392. Elsevier, Amsterdam (1972). https:\/\/doi.org\/10.1016\/1385-7258(72)90034-0","DOI":"10.1016\/1385-7258(72)90034-0"},{"issue":"2","key":"9705_CR15","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1145\/251880.251992","volume":"22","author":"M Dowson","year":"1997","unstructured":"Dowson, M.: The Ariane 5 software failure. ACM SIGSOFT Softw Eng Notes 22(2), 84 (1997). https:\/\/doi.org\/10.1145\/251880.251992","journal-title":"ACM SIGSOFT Softw Eng Notes"},{"key":"9705_CR16","doi-asserted-by":"publisher","unstructured":"Erbsen, A., Philipoom, J., Gross, J., Sloan, R., Chlipala, A.: Simple high-level code for cryptographic arithmetic\u2014with proofs, without compromises. In: 2019 IEEE Symposium on Security and Privacy (SP), pp. 1202\u20131219. San Francisco, CA, USA (2019). https:\/\/doi.org\/10.1109\/SP.2019.00005. http:\/\/adam.chlipala.net\/papers\/FiatCryptoSP19\/","DOI":"10.1109\/SP.2019.00005"},{"key":"9705_CR17","unstructured":"Gawron, N.: Infamous Software Bugs: FDIV Bug. https:\/\/www.olenick.com\/blog\/articles\/infamous-software-bugs-fdiv-bug"},{"issue":"1","key":"9705_CR18","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: On formally undecidable propositions of Principia Mathematica and related systems I. Monatshefte f\u00fcr Mathematik 38(1), 173\u2013198 (1931). https:\/\/doi.org\/10.1007\/BF01700692","journal-title":"Monatshefte f\u00fcr Mathematik"},{"key":"9705_CR19","doi-asserted-by":"publisher","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming. ICFP \u201902, pp. 235\u2013246. Association for Computing Machinery, New York, NY, USA (2002). https:\/\/doi.org\/10.1145\/581478.581501","DOI":"10.1145\/581478.581501"},{"key":"9705_CR20","doi-asserted-by":"publisher","unstructured":"Gr\u00e9goire, B., Pottier, L., Th\u00e9ry, L.: Proof certificates for algebra and their application to automatic geometry theorem proving. In: Sturm, T., Zengler, C. (eds.) Automated Deduction in Geometry, pp. 42\u201359. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-21046-4_3","DOI":"10.1007\/978-3-642-21046-4_3"},{"key":"9705_CR21","doi-asserted-by":"publisher","unstructured":"Gross, J., Erbsen, A., Philipoom, J., Agrawal, R., Chlipala, A.: Accelerating verified-compiler development with a verified rewriting engine. In: Andronick, J., de Moura, L. (eds.) Proceedings of the 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 237, pp. 17\u201311718. Schloss Dagstuhl\u2014Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2022). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.17. arXiv:2205.00862","DOI":"10.4230\/LIPIcs.ITP.2022.17"},{"key":"9705_CR22","unstructured":"Gross, J.S.: Performance engineering of proof-based software systems at scale. PhD thesis, Massachusetts Institute of Technology (February 2021). https:\/\/dspace.mit.edu\/handle\/1721.1\/130763"},{"key":"9705_CR23","unstructured":"Gross, J.: setoid_rewrite and rewrite_strat Are Cubic in the Number of Binders Even When There Are No Matches $$\\bullet $$ Issue #12524 $$\\bullet $$ Coq\/coq, GitHub issue (2020). Accessed 25 Apr 2023. https:\/\/github.com\/coq\/coq\/issues\/12524"},{"key":"9705_CR24","unstructured":"Haftmann, F., Nipkow, T.: A code generator framework for Isabelle\/HOL. In: Proc. TPHOLs (2007)"},{"key":"9705_CR25","unstructured":"Halfhill, T.R.: The Truth Behind the Pentium Bug. https:\/\/web.archive.org\/web\/20060209005434, http:\/\/www.byte.com\/art\/9503\/sec13\/art1.htm"},{"key":"9705_CR26","unstructured":"Hern, A.: Microsoft scrambles to limit PR damage over abusive AI Bot Tay, The Guardian (2016). Accessed 24 Apr 2023. https:\/\/www.theguardian.com\/technology\/2016\/mar\/24\/microsoft-scrambles-limit-pr-damage-over-abusive-ai-bot-tay"},{"issue":"2","key":"9705_CR27","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/s10990-006-8746-6","volume":"19","author":"J Hickey","year":"2006","unstructured":"Hickey, J., Nogin, A.: Formal compiler construction in a logical framework. Higher-Order Symb. Comput. 19(2), 197\u2013230 (2006). https:\/\/doi.org\/10.1007\/s10990-006-8746-6","journal-title":"Higher-Order Symb. Comput."},{"issue":"1","key":"9705_CR28","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1109\/2.562936","volume":"30","author":"J-M J\u00e9z\u00e9quel","year":"1997","unstructured":"J\u00e9z\u00e9quel, J.-M., Meyer, B.: Design by contract: the lessons of Ariane. Computer 30(1), 129\u2013130 (1997). https:\/\/doi.org\/10.1109\/2.562936","journal-title":"Computer"},{"key":"9705_CR29","unstructured":"Kolomatskaia, A., Shulman, M.: Semi-simplicial types, GitHub repository (2022). Accessed 25 Apr 2023. https:\/\/github.com\/FrozenWinters\/SSTs"},{"key":"9705_CR30","doi-asserted-by":"publisher","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: A verified implementation of ML. In: POPL \u201914: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL \u201914, pp. 179\u2013191. ACM Press, New York, NY, USA (2014). https:\/\/doi.org\/10.1145\/2535838.2535841","DOI":"10.1145\/2535838.2535841"},{"key":"9705_CR31","unstructured":"Lee, P.: Learning from Tay\u2019s Introduction, Official Microsoft Blog (2016). Microsoft. Accessed 24 Apr 2023. https:\/\/blogs.microsoft.com\/blog\/2016\/03\/25\/learning-tays-introduction\/"},{"key":"9705_CR32","unstructured":"Leech, J.P., Klaes, L., Wiener, M., Yamada, Y.: Space FAQ 08\/13\u2014planetary probe history. http:\/\/www.faqs.org\/faqs\/space\/probe\/"},{"issue":"4","key":"9705_CR33","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9155-4","journal-title":"J. Autom. Reason."},{"issue":"7","key":"9705_CR34","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1109\/MC.1993.274940","volume":"26","author":"NG Leveson","year":"1993","unstructured":"Leveson, N.G., Turner, C.S.: An investigation of the Therac-25 accidents. Computer 26(7), 18\u201341 (1993). https:\/\/doi.org\/10.1109\/MC.1993.274940","journal-title":"Computer"},{"key":"9705_CR35","unstructured":"Lloyd, R.: Metric mishap caused loss of NASA orbiter. http:\/\/www.cnn.com\/TECH\/space\/9909\/30\/mars.metric.02\/index.html"},{"issue":"2","key":"9705_CR36","doi-asserted-by":"publisher","first-page":"115","DOI":"10.2307\/2266895","volume":"20","author":"MH L\u00f6b","year":"1955","unstructured":"L\u00f6b, M.H.: Solution of a problem of Leon Henkin. J. Symb. Logic 20(2), 115\u2013118 (1955). https:\/\/doi.org\/10.2307\/2266895","journal-title":"J. Symb. Logic"},{"key":"9705_CR37","unstructured":"Lynch, J.: The worst computer bugs in history: losing \\$460m in 45 minutes. BugSnag Blog. Accessed 25 Apr 2023 (2017). https:\/\/www.bugsnag.com\/blog\/bug-day-460m-loss"},{"key":"9705_CR38","unstructured":"Lynch, J.: The worst computer bugs in history: race conditions in Therac-25. BugSnag Blog. Accessed 25 Apr 2023 (2017). https:\/\/www.bugsnag.com\/blog\/bug-day-race-condition-therac-25"},{"key":"9705_CR39","unstructured":"Lynch, J.: The worst computer bugs in history: rapid unanticipated disassembly of the Mars Climate Orbiter. BugSnag Blog. Accessed 25 Apr 2023 (2017). https:\/\/www.bugsnag.com\/blog\/bug-day-mars-climate-orbiter"},{"key":"9705_CR40","unstructured":"Lynch, J.: The worst computer bugs in history: the Ariane 5 disaster. BugSnag Blog. Accessed 25 Apr 2023 (2017). https:\/\/www.bugsnag.com\/blog\/bug-day-ariane-5-disaster"},{"key":"9705_CR41","doi-asserted-by":"publisher","unstructured":"Malecha, G., Bengtson, J.: Extensible and efficient automation through reflective tactics. In: Thiemann, P. (ed.) Programming Languages and Systems: 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2\u20138, 2016, Proceedings, pp. 532\u2013559. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_21","DOI":"10.1007\/978-3-662-49498-1_21"},{"key":"9705_CR42","unstructured":"Malecha, G.M.: Extensible proof engineering in intensional type theory. PhD thesis, Harvard University (November 2014). http:\/\/gmalecha.github.io\/publication\/2015\/02\/01\/extensible-proof-engineering-in-intensional-type-theory.html"},{"key":"9705_CR43","doi-asserted-by":"crossref","unstructured":"Maranget, L.: Compiling pattern matching to good decision trees. In: Proceedings of the 2008 ACM SIGPLAN Workshop on ML, pp. 35\u201346 (2008). ACM. http:\/\/moscova.inria.fr\/~maranget\/papers\/ml05e-maranget.pdf","DOI":"10.1145\/1411304.1411311"},{"key":"9705_CR44","doi-asserted-by":"publisher","unstructured":"Martin-Dorel, \u00c9., Roux, P.: A reflexive tactic for polynomial positivity using numerical solvers and floating-point computations. In: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs. CPP 2017, pp. 90\u201399. Association for Computing Machinery, New York, NY, USA (2017). https:\/\/doi.org\/10.1145\/3018610.3018622","DOI":"10.1145\/3018610.3018622"},{"key":"9705_CR45","unstructured":"Nicely, T.R.: Pentium FDIV Flaw FAQ. https:\/\/web.archive.org\/web\/20190618044444, http:\/\/www.trnicely.net\/pentbug\/pentbug.html"},{"key":"9705_CR46","unstructured":"Pottier, L.: Connecting Gr\u00f6bner bases programs with Coq to do proofs in algebra, geometry and arithmetics (2010) arXiv:1007.3615"},{"key":"9705_CR47","unstructured":"Pujet, L.: A logical relation for MLTT using indexed inductive types, GitHub repository (2022). Accessed 25 Apr 2023. https:\/\/github.com\/loic-p\/logrel-mltt\/"},{"key":"9705_CR48","doi-asserted-by":"publisher","unstructured":"Schropp, A., Popescu, A.: Nonfree datatypes in Isabelle\/HOL. In: Gonthier, G., Norrish, M. (eds.) Certified Programs and Proofs, pp. 114\u2013130. Springer, New York. https:\/\/doi.org\/10.1007\/978-3-319-03545-1_8","DOI":"10.1007\/978-3-319-03545-1_8"},{"key":"9705_CR49","unstructured":"Shulman, M.: Homotopy type theory should eat itself (but so Far, It\u2019s Too Big to Swallow), Homotopy Type Theory Blog (2014). Accessed 24 Apr 2023. https:\/\/homotopytypetheory.org\/2014\/03\/03\/hott-should-eat-itself\/"},{"key":"9705_CR50","unstructured":"Smith, S., Patwary, M., Norick, B., LeGresley, P., Rajbhandari, S., Casper, J., Liu, Z., Prabhumoye, S., Zerveas, G., Korthikanti, V., Zhang, E., Child, R., Aminabadi, R.Y., Bernauer, J., Song, X., Shoeybi, M., He, Y., Houston, M., Tiwary, S., Catanzaro, B.: Using DeepSpeed and Megatron to train Megatron-Turing NLG 530B, a large-scale generative language model (2022) arXiv:2201.11990"},{"key":"9705_CR51","doi-asserted-by":"publisher","unstructured":"Sozeau, M., Boulier, S., Forster, Y., Tabareau, N., Winterhalter, T.: Coq Coq correct! verification of type checking and erasure for Coq. In: Coq. Proc. ACM Program. Lang. 4(POPL) (2019). https:\/\/doi.org\/10.1145\/3371076","DOI":"10.1145\/3371076"},{"issue":"5","key":"9705_CR52","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1007\/s10817-019-09540-0","volume":"64","author":"M Sozeau","year":"2020","unstructured":"Sozeau, M., Anand, A., Boulier, S., Cohen, C., Forster, Y., Kunze, F., Malecha, G., Tabareau, N., Winterhalter, T.: The MetaCoq project. J. Autom. Reason. 64(5), 947\u2013999 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09540-0","journal-title":"J. Autom. Reason."},{"key":"9705_CR53","unstructured":"Turley, J.: ChatGPT falsely accused me of sexually harassing my students. Can we really trust AI? USA Today. Accessed 1 May 2023 (2023). https:\/\/www.usatoday.com\/story\/opinion\/columnist\/2023\/04\/03\/chatgpt-misinformation-bias-flaws-ai-chatbot\/11571830002\/"},{"key":"9705_CR54","unstructured":"Westbrook, E.: Uniform logical relations. Technical Report TR11-01, Rice University (2011). April 1, 2011. https:\/\/hdl.handle.net\/1911\/96394"},{"key":"9705_CR55","unstructured":"Xiang, C.: \u2018He Would Still Be Here\u2019: man dies by suicide after talking with AI Chatbot, Widow Says, Vice (2023). Accessed 24 Apr 2024. https:\/\/www.vice.com\/en\/article\/pkadgm\/man-dies-by-suicide-after-talking-with-ai-chatbot-widow-says"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09705-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-024-09705-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-024-09705-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T05:10:02Z","timestamp":1725599402000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-024-09705-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,14]]},"references-count":55,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,9]]}},"alternative-id":["9705"],"URL":"https:\/\/doi.org\/10.1007\/s10817-024-09705-6","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-2891864\/v1","asserted-by":"object"}]},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,14]]},"assertion":[{"value":"4 May 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 June 2024","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 August 2024","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"<i>Financial interests<\/i> None. <i>Non-financial interests<\/i> Jason Gross is a member of the Coq development team.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}},{"value":"Not applicable.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical Approval"}},{"value":"Not applicable.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent to Participate"}},{"value":"Not applicable.","order":5,"name":"Ethics","group":{"name":"EthicsHeading","label":"Consent for Publication"}}],"article-number":"19"}}