{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:44:47Z","timestamp":1743140687301,"version":"3.40.3"},"publisher-location":"Cham","reference-count":43,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031666728"},{"type":"electronic","value":"9783031666735"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-66673-5_9","type":"book-chapter","created":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:04:18Z","timestamp":1725451458000},"page":"162-183","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["About Trust and\u00a0Proof: An Experimental Framework for\u00a0Heterogeneous Verification"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1520-7090","authenticated-orcid":false,"given":"Farah","family":"Al Wardani","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2938-547X","authenticated-orcid":false,"given":"Kaustuv","family":"Chaudhuri","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0274-4954","authenticated-orcid":false,"given":"Dale","family":"Miller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,4]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M.: Variations in access control logic. In: van\u00a0der Meyden, R., van\u00a0der Torre, L.W.N. (eds.) DEON 2008. LNCS, vol.\u00a05076, pp. 96\u2013109. Springer, Cham (2008). https:\/\/doi.org\/10.1007\/978-3-540-70525-3_9","DOI":"10.1007\/978-3-540-70525-3_9"},{"key":"9_CR2","unstructured":"Abella in your browser (2015). https:\/\/abella-prover.org\/tutorial\/try"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Al Wardani, F., Chaudhuri, K., Miller, D.: The distributed assertions website, May 2024. Archived version. https:\/\/doi.org\/10.5281\/zenodo.11163505","DOI":"10.5281\/zenodo.11163505"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Al Wardani, F., Chaudhuri, K., Miller, D.: Formal reasoning using distributed assertions. In: Sattler, U., Suda, M. (eds.) FroCoS 2023. LNAI, vol. 14279, pp. 176\u2013194. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-43369-6_10","DOI":"10.1007\/978-3-031-43369-6_10"},{"key":"9_CR5","first-page":"11","volume":"61","author":"R Ap\u00e9ry","year":"1979","unstructured":"Ap\u00e9ry, R.: Irrationalit\u00e9 de $$\\zeta 2$$ et $$\\zeta 3$$. Journ\u00e9es Arithm\u00e9tiques de Luminy, Ast\u00e9risque 61, 11\u201313 (1979)","journal-title":"Journ\u00e9es Arithm\u00e9tiques de Luminy, Ast\u00e9risque"},{"key":"9_CR6","unstructured":"Assaf, A., et al.: Dedukti: a logical framework based on the $$\\lambda {\\Pi }$$-calculus modulo theory (2016). https:\/\/theses.hal.science\/INRIA-SACLAY-2015\/hal-04281492v1"},{"issue":"2","key":"9_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.6092\/issn.1972-5787\/4650","volume":"7","author":"D Baelde","year":"2014","unstructured":"Baelde, D., et al.: Abella: a system for reasoning about relational specifications. J. Formalized Reason. 7(2), 1\u201389 (2014). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650","journal-title":"J. Formalized Reason."},{"key":"9_CR8","doi-asserted-by":"publisher","unstructured":"Benet, J.: IPFS-content addressed, versioned, P2P file system (2014). https:\/\/doi.org\/10.48550\/arxiv.1407.3561","DOI":"10.48550\/arxiv.1407.3561"},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Berners-Lee, T., Hendler, J., Lassila, O.: The semantic web. In: Linking the World\u2019s Information, pp. 91\u2013103. ACM (2023). https:\/\/doi.org\/10.1145\/3591366.3591376","DOI":"10.1145\/3591366.3591376"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004).https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"9_CR11","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press (1979)"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symbolic Logic 5, 56\u201368 (1940). https:\/\/doi.org\/10.2307\/2266170","DOI":"10.2307\/2266170"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 118\u2013135. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_7","DOI":"10.1007\/978-3-662-54577-5_7"},{"key":"9_CR14","unstructured":"Debian\u2019s SecureApt. https:\/\/wiki.debian.org\/SecureApt"},{"key":"9_CR15","doi-asserted-by":"publisher","unstructured":"Dowek, G., Thir\u00e9, F.: Logipedia: a multi-system encyclopedia of formal proofs. Technical report. abs\/2305.00064, ArXiV (2023). https:\/\/doi.org\/10.48550\/ARXIV.2305.00064","DOI":"10.48550\/ARXIV.2305.00064"},{"key":"9_CR16","doi-asserted-by":"publisher","unstructured":"Dunchev, C., Guidi, F., Coen, C.S., Tassi, E.: ELPI: fast, embeddable, $$\\lambda $$Prolog interpreter. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2020. LNCS, vol.\u00a09450, pp. 460\u2013468. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-662-48899-7_32","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Dwork, C., Roth, A.: The algorithmic foundations of differential privacy. Found. Trends Theor. Comput. Sci. 9(3-4), 211\u2013407 (2014). https:\/\/doi.org\/10.1561\/0400000042","DOI":"10.1561\/0400000042"},{"key":"9_CR18","unstructured":"GeoGebra for teaching and learning math. https:\/\/www.geogebra.org\/"},{"key":"9_CR19","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","volume":"45","author":"JY Girard","year":"1986","unstructured":"Girard, J.Y.: The system F of variable types: fifteen years later. Theoret. Comput. Sci. 45, 159\u2013192 (1986). https:\/\/doi.org\/10.1016\/0304-3975(86)90044-7","journal-title":"Theoret. Comput. Sci."},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Gordon, M.J., Milner, A.J., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation. LNCS, vol.\u00a078. Springer, Heidelberg (1979). https:\/\/doi.org\/10.1007\/3-540-09724-4","DOI":"10.1007\/3-540-09724-4"},{"key":"9_CR21","unstructured":"Gordon, M.: HOL: A machine oriented formulation of higher-order logic. Technical report,\u00a068, University of Cambridge, July 1985. https:\/\/www.cl.cam.ac.uk\/techreports\/UCAM-CL-TR-68.pdf"},{"key":"9_CR22","doi-asserted-by":"publisher","unstructured":"Heule, Jr. M., Hunt, W.A., Wetzler, N.: Trimming while checking clausal proofs. In: Formal Methods in Computer-Aided Design, FMCAD 2013, pp. 181\u2013188. IEEE (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679408","DOI":"10.1109\/FMCAD.2013.6679408"},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H.: Schur number five. In: McIlraith, S.A., Weinberger, K.Q. (eds.) Proceedings of the Thirty-Second Conference on Artificial Intelligence (AAAI 2018), pp. 6598\u20136606. AAAI Press (2018). https:\/\/doi.org\/10.1609\/AAAI.V32I1.12209","DOI":"10.1609\/AAAI.V32I1.12209"},{"key":"9_CR24","doi-asserted-by":"publisher","unstructured":"Jones, C.B.: VDM proof obligations and their justification. In: Bj\u00f8rner, D., Jones, C.B., Mac an Airchinnigh, M., Neuhold, E.J. (eds.) VDM 1987. LNCS, vol.\u00a0252, pp. 260\u2013286. Springer, Cham (1987). https:\/\/doi.org\/10.1007\/3-540-17654-3_15","DOI":"10.1007\/3-540-17654-3_15"},{"key":"9_CR25","doi-asserted-by":"publisher","unstructured":"Jourdan, J.H., Pottier, F., Leroy, X.: Validating LR(1) parsers. In: Seidl, H. (ed.) ESOP 2012, vol. 7211, pp. 397\u2013416. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28869-2_20","DOI":"10.1007\/978-3-642-28869-2_20"},{"key":"9_CR26","doi-asserted-by":"publisher","unstructured":"Konev, B., Lisitsa, A.: Computer-aided proof of Erd\u00f6s discrepancy properties. Artif. Intell. 224, 103\u2013118 (2015). https:\/\/doi.org\/10.1016\/j.artint.2015.03.004","DOI":"10.1016\/j.artint.2015.03.004"},{"key":"9_CR27","unstructured":"Lafont, A.: A diagram editor to mechanise categorical proofs. In: JFLA 2024: Journ\u00e9es Francophones des Langages Applicatifs. Saint-Jacut-de-la-Mer, France, January 2024. https:\/\/hal.science\/hal-04407118"},{"key":"9_CR28","unstructured":"The Lean Reference Manual. https:\/\/leanprover.github.io\/reference\/"},{"key":"9_CR29","doi-asserted-by":"publisher","unstructured":"Mahboubi, A., Sibut-Pinote, T.: A formal proof of the irrationality of $$\\zeta (3)$$. Log. Methods Comput. Sci. 17(1), 1\u201325 (2021). https:\/\/doi.org\/10.23638\/LMCS-17(1:16)2021","DOI":"10.23638\/LMCS-17(1:16)2021"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Miller, D., Nadathur, G.: Programming with Higher-Order Logic. Cambridge University Press (2012). https:\/\/doi.org\/10.1017\/CBO9781139021326","DOI":"10.1017\/CBO9781139021326"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"M\u00fcller, D., Rabe, F., Coen, C.S.: The Coq library as a theory graph. In: Kaliszyk, C., Brady, E., Kohlhase, A., Sacerdoti Coen, C. (eds.) CICM 2019. LNCS, vol. 11617, pp. 171\u2013186. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-23250-4_12","DOI":"10.1007\/978-3-030-23250-4_12"},{"key":"9_CR32","doi-asserted-by":"publisher","unstructured":"Necula, G.C.: Proof-carrying code. In: 24th Symposium on Principles of Programming Languages, vol. 97, pp. 106\u2013119. ACM, Paris, France (1997). https:\/\/doi.org\/10.1145\/263699.263712","DOI":"10.1145\/263699.263712"},{"key":"9_CR33","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL\u2014A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"9_CR34","unstructured":"Nystrom, et al.: UEFI networking and pre-OS security. Intel Technol. J. UEFI Today Boostrapping Continuum 15(1), 80\u2013101 (2011)"},{"key":"9_CR35","doi-asserted-by":"publisher","unstructured":"Owre, S., Rushby, J.M., , Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217","DOI":"10.1007\/3-540-55602-8_217"},{"key":"9_CR36","unstructured":"Paul, C., Matthews, M.: The Russian \u201cFirehose of Falsehood\u201d propaganda model. Rand Corporation 2(7), 1\u201310 (2016). https:\/\/www.rand.org\/pubs\/perspectives\/PE198.html"},{"key":"9_CR37","doi-asserted-by":"publisher","unstructured":"Paulson, L.C.: Isabelle: A Generic Theorem Prover. LNCS, vol. 828. Springer, Cham (1994). https:\/\/doi.org\/10.1007\/BFb0030541","DOI":"10.1007\/BFb0030541"},{"key":"9_CR38","doi-asserted-by":"crossref","unstructured":"Pollack, R.: How to believe a machine-checked proof. In: Sambin, G., Smith, J. (eds.) Twenty Five Years of Constructive Type Theory. Oxford University Press (1998)","DOI":"10.1093\/oso\/9780198501275.003.0013"},{"key":"9_CR39","doi-asserted-by":"publisher","unstructured":"van\u00a0der Poorten, A.: A proof that Euler missed .... In: Berggren, L., Borwein, J., Borwein, P. (eds.) Pi: A Source Book, pp. 439\u2013447. Springer, New York (2000). https:\/\/doi.org\/10.1007\/978-1-4757-3240-5_49","DOI":"10.1007\/978-1-4757-3240-5_49"},{"key":"9_CR40","unstructured":"Portoraro, F.: Automated reasoning. In: Zalta, E.N., Nodelman, U. (eds.) The Stanford Encyclopedia of Philosophy. Spring (2024). https:\/\/plato.stanford.edu\/archives\/spr2024\/entries\/reasoning-automated\/"},{"key":"9_CR41","unstructured":"Qi, X., Gacek, A., Holte, S., Nadathur, G., Snow, Z.: The Teyjus system \u2013 version 2 (2015). https:\/\/teyjus.cs.umn.edu\/"},{"key":"9_CR42","doi-asserted-by":"publisher","unstructured":"Rabe, F.: The future of logic: foundation-independence. Logica Universalis 10(1), 1\u201320 (2016). https:\/\/doi.org\/10.1007\/s11787-015-0132-x","DOI":"10.1007\/s11787-015-0132-x"},{"key":"9_CR43","doi-asserted-by":"publisher","unstructured":"The mathlib Community: The Lean mathematical library. In: CPP 2020: International\u00a0Conference on Certified Programs and Proofs, pp. 367\u2013381. ACM, January 2020. https:\/\/doi.org\/10.1145\/3372885.3373824","DOI":"10.1145\/3372885.3373824"}],"container-title":["Lecture Notes in Computer Science","The Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66673-5_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T12:08:35Z","timestamp":1725451715000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66673-5_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031666728","9783031666735"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66673-5_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"4 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}