{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T14:31:47Z","timestamp":1742913107027,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031433689"},{"type":"electronic","value":"9783031433696"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T00:00:00Z","timestamp":1694563200000},"content-version":"vor","delay-in-days":255,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>When a proof system checks a formal proof, we can say that its kernel <jats:italic>asserts<\/jats:italic> that the formula is a theorem in a particular logic. We describe a general framework in which such assertions can be made globally available so that any other proof assistant willing to trust the assertion\u2019s creator can use that assertion without rechecking any associated formal proof. This framework, called DAMF, is heterogeneous and allows each participant to decide which tools and operators they are willing to trust in order to accept external assertions. This framework can also be integrated into existing proof systems by making minor changes to the input and output subsystems of the prover. DAMF achieves a high level of distributivity using such off-the-shelf technologies as IPFS, IPLD, and public key cryptography. We illustrate the framework by describing an implemented tool for validating and publishing assertion objects and a modified version of the Abella theorem prover that can use and publish such assertions.<\/jats:p>","DOI":"10.1007\/978-3-031-43369-6_10","type":"book-chapter","created":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:32:18Z","timestamp":1694701938000},"page":"176-194","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Reasoning Using Distributed Assertions"],"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":[[2023,9,13]]},"reference":[{"key":"10_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-540-70525-3_9","volume-title":"Deontic Logic in Computer Science","author":"M Abadi","year":"2008","unstructured":"Abadi, M.: Variations in access control logic. In: van der Meyden, R., van der Torre, L. (eds.) DEON 2008. LNCS (LNAI), vol. 5076, pp. 96\u2013109. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70525-3_9"},{"key":"10_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000170","volume":"29","author":"A Abel","year":"2019","unstructured":"Abel, A., et al.: POPLMark reloaded: mechanizing proofs by logical relations. J. Funct. Program. 29, e19 (2019). https:\/\/doi.org\/10.1017\/S0956796819000170","journal-title":"J. Funct. Program."},{"key":"10_CR3","unstructured":"Al Wardani, F., Chaudhuri, K., Miller, D.: Distributing and trusting proof checking: a preliminary report. Technical report, Inria Saclay (2022). https:\/\/hal.inria.fr\/hal-03909741"},{"key":"10_CR4","unstructured":"Al Wardani, F., Chaudhuri, K., Miller, D.: Formal reasoning using distributed assertions. Technical report. HAL-04167922, Inria (2023). https:\/\/inria.hal.science\/hal-04167922"},{"key":"10_CR5","unstructured":"ANSSI, F.N.C.A.: Requirements on the use of Coq in the context of common criteria evaluations. URL (2021). v1.1"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-25379-9_12","volume-title":"Certified Programs and Proofs","author":"M Armand","year":"2011","unstructured":"Armand, M., Faure, G., Gr\u00e9goire, B., Keller, C., Th\u00e9ry, L., Werner, B.: A modular integration of SAT\/SMT solvers to Coq through proof witnesses. In: Jouannaud, J.-P., Shao, Z. (eds.) CPP 2011. LNCS, vol. 7086, pp. 135\u2013150. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_12"},{"issue":"1\u20133","key":"10_CR7","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1023\/A:1022907629104","volume":"38","author":"A Asperti","year":"2003","unstructured":"Asperti, A., Padovani, L., Coen, C.S., Guidi, F., Schena, I.: Mathematical knowledge management in HELM. Ann. Math. Artif. Intell. 38(1\u20133), 27\u201346 (2003)","journal-title":"Ann. Math. Artif. Intell."},{"key":"10_CR8","unstructured":"Assaf, A., et al.: Dedukti: a logical framework based on the $$\\lambda {\\Pi }$$-calculus modulo theory (2016). http:\/\/www.lsv.ens-cachan.fr\/dowek\/Publi\/expressing.pdf"},{"key":"10_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/11541868_4","volume-title":"Theorem Proving in Higher Order Logics","author":"BE Aydemir","year":"2005","unstructured":"Aydemir, B.E., et al.: Mechanized metatheory for the masses: the PoplMark challenge. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 50\u201365. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11541868_4"},{"issue":"2","key":"10_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.6092\/issn.1972-5787\/4650","volume":"7","author":"D Baelde","year":"2014","unstructured":"Baelde, D., Chaudhuri, K., Gacek, A., Miller, D., Nadathur, G., Tiu, A., Wang, Y.: Abella: a system for reasoning about relational specifications. J. Formaliz. Reason. 7(2), 1\u201389 (2014). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4650","journal-title":"J. Formaliz. Reason."},{"issue":"1835","key":"10_CR11","first-page":"2351","volume":"363","author":"H Barendregt","year":"2005","unstructured":"Barendregt, H., Wiedijk, F.: The challenge of computer mathematics. Trans. A R. Soc. 363(1835), 2351\u20132375 (2005)","journal-title":"Trans. A R. Soc."},{"issue":"3","key":"10_CR12","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1023\/A:1015761529444","volume":"28","author":"H Barendregt","year":"2002","unstructured":"Barendregt, H., Barendsen, E.: Autarkic computations in formal proofs. J. Autom. Reason. 28(3), 321\u2013336 (2002). https:\/\/doi.org\/10.1023\/A:1015761529444","journal-title":"J. Autom. Reason."},{"key":"10_CR13","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":"10_CR14","unstructured":"Berners-Lee, T.: Semantic Web road map. Technical report, W3C Design Issues (1998). http:\/\/www.w3.org\/DesignIssues\/Semantic.html"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Berners-Lee, T., Hendler, J., Lassila, O.: The semantic web. Scientific American Magazine (May 2001)","DOI":"10.1038\/scientificamerican0501-34"},{"key":"10_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-14808-8_3","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"K Chaudhuri","year":"2010","unstructured":"Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA + proof system: building a heterogeneous verification platform. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, p. 44. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14808-8_3"},{"key":"10_CR17","unstructured":"Chaudhuri, K., G\u00e9rard, U., Miller, D.: Computation-as-deduction in Abella: work in progress. In: 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice. Oxford, United Kingdom, July 2018. https:\/\/hal.inria.fr\/hal-01806154"},{"issue":"3","key":"10_CR18","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/s10817-016-9380-6","volume":"59","author":"Z Chihani","year":"2016","unstructured":"Chihani, Z., Miller, D., Renaud, F.: A semantic framework for proof evidence. J. Autom. Reason. 59(3), 287\u2013330 (2016). https:\/\/doi.org\/10.1007\/s10817-016-9380-6","journal-title":"J. Autom. Reason."},{"key":"10_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/978-3-540-27818-4_24","volume-title":"Mathematical Knowledge Management","author":"CS Coen","year":"2004","unstructured":"Coen, C.S.: Mathematical libraries as proof assistant environments. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 332\u2013346. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27818-4_24"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-642-35873-9_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Cruanes","year":"2013","unstructured":"Cruanes, S., Hamon, G., Owre, S., Shankar, N.: Tool integration with the evidential tool bus. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 275\u2013294. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35873-9_18"},{"key":"10_CR21","unstructured":"Dowek, G., Thir\u00e9, F.: Logipedia: a multi-system encyclopedia of formal proofs. http:\/\/www.lsv.fr\/dowek\/Publi\/logipedia.pdf (2019)"},{"issue":"4","key":"10_CR22","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10817-015-9327-3","volume":"55","author":"AP Felty","year":"2015","unstructured":"Felty, A.P., Momigliano, A., Pientka, B.: The next 700 challenge problems for reasoning with higher-order abstract syntax representations. J. Autom. Reason. 55(4), 307\u2013372 (2015). https:\/\/doi.org\/10.1007\/s10817-015-9327-3","journal-title":"J. Autom. Reason."},{"key":"10_CR23","doi-asserted-by":"publisher","first-page":"1507","DOI":"10.1017\/S0960129517000093","volume":"28","author":"AP Felty","year":"2017","unstructured":"Felty, A.P., Momigliano, A., Pientka, B.: Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions. Math. Struct. Comput. Sci. 28, 1507\u20131540 (2017). https:\/\/doi.org\/10.1017\/S0960129517000093","journal-title":"Math. Struct. Comput. Sci."},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/11691372_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Fontaine","year":"2006","unstructured":"Fontaine, P., Marion, J.-Y., Merz, S., Nieto, L.P., Tiu, A.: Expressiveness + automation + soundness: towards combining SMT solvers and interactive proof assistants. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 167\u2013181. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11691372_11"},{"issue":"1","key":"10_CR26","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1016\/j.ic.2010.09.004","volume":"209","author":"A Gacek","year":"2011","unstructured":"Gacek, A., Miller, D., Nadathur, G.: Nominal abstraction. Inf. Comput. 209(1), 48\u201373 (2011). https:\/\/doi.org\/10.1016\/j.ic.2010.09.004","journal-title":"Inf. Comput."},{"key":"10_CR27","unstructured":"Harrison, J.: The HOL Light tutorial (2017). https:\/\/www.cl.cam.ac.uk\/jrh13\/hol-light\/tutorial.pdf"},{"key":"10_CR28","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"10_CR29","unstructured":"Logipedia in a nutshell (2022). http:\/\/logipedia.inria.fr\/about\/about.php"},{"issue":"4","key":"10_CR30","doi-asserted-by":"publisher","first-page":"749","DOI":"10.1145\/1094622.1094628","volume":"6","author":"D Miller","year":"2005","unstructured":"Miller, D., Tiu, A.: A proof theory for generic judgments. ACM Trans. Comput. Log. 6(4), 749\u2013783 (2005). https:\/\/doi.org\/10.1145\/1094622.1094628","journal-title":"ACM Trans. Comput. Log."},{"issue":"8","key":"10_CR31","doi-asserted-by":"publisher","first-page":"1309","DOI":"10.1017\/S0960129518000415","volume":"29","author":"A Momigliano","year":"2019","unstructured":"Momigliano, A., Pientka, B., Thibodeau, D.: A case study in programming coinductive proofs: Howe\u2019s method. Math. Struct. Comput. Sci. 29(8), 1309\u20131343 (2019). https:\/\/doi.org\/10.1017\/S0960129518000415","journal-title":"Math. Struct. Comput. Sci."},{"key":"10_CR32","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Proofs and refutations, and Z3. In: Rudnicki, P., Sutcliffe, G., Konev, B., Schmidt, R.A., Schulz, S. (eds.) Proceedings of the Combined KEAPPA - IWIL Workshops. CEUR Workshop Proceedings, vol. 418, pp. 123\u2013132. CEUR-WS.org (2008). http:\/\/ceur-ws.org\/Vol-418\/paper10.pdf"},{"key":"10_CR33","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/3-540-48660-7_14","volume-title":"Automated Deduction \u2014 CADE-16","author":"F Pfenning","year":"1999","unstructured":"Pfenning, F., Sch\u00fcrmann, C.: System description: Twelf \u2014 a meta-logical framework for deductive systems. In: CADE 1999. LNCS (LNAI), vol. 1632, pp. 202\u2013206. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48660-7_14"},{"issue":"2","key":"10_CR34","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1016\/S0890-5401(03)00138-X","volume":"186","author":"AM Pitts","year":"2003","unstructured":"Pitts, A.M.: Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), 165\u2013193 (2003)","journal-title":"Inf. Comput."},{"issue":"1","key":"10_CR35","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s11787-015-0132-x","volume":"10","author":"F Rabe","year":"2016","unstructured":"Rabe, F.: The future of logic: foundation-independence. Log. Univers. 10(1), 1\u201320 (2016)","journal-title":"Log. Univers."},{"issue":"6","key":"10_CR36","doi-asserted-by":"publisher","first-page":"1753","DOI":"10.1093\/logcom\/exu079","volume":"27","author":"F Rabe","year":"2017","unstructured":"Rabe, F.: How to identify, translate and combine logics? J. Log. Comput. 27(6), 1753\u20131798 (2017)","journal-title":"J. Log. Comput."},{"key":"10_CR37","unstructured":"Rabe, F.: The MMT Language and System (2022). https:\/\/uniformal.github.io\/"},{"key":"10_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/11576280_3","volume-title":"Formal Methods and Software Engineering","author":"J Rushby","year":"2005","unstructured":"Rushby, J.: An evidential tool bus. In: Lau, K.-K., Banach, R. (eds.) ICFEM 2005. LNCS, vol. 3785, pp. 36\u201336. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11576280_3"},{"issue":"5","key":"10_CR39","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1007\/s10817-019-09540-0","volume":"64","author":"M Sozeau","year":"2020","unstructured":"Sozeau, M., et al.: 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."},{"issue":"4","key":"10_CR40","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/s10817-009-9143-8","volume":"43","author":"G Sutcliffe","year":"2009","unstructured":"Sutcliffe, G.: The TPTP problem library and associated infrastructure: the FOF and CNF parts, v3.5.0. J. Autom. Reason. 43(4), 337\u2013362 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9143-8","journal-title":"J. Autom. Reason."},{"key":"10_CR41","unstructured":"Tiu, A.: On the role of names in reasoning about $$\\lambda $$-tree syntax specifications. In: Abel, A., Urban, C. (eds.) International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), pp. 32\u201346 (2008)"},{"key":"10_CR42","unstructured":"The Twelf project (2016). http:\/\/twelf.org\/"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-43369-6_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,14]],"date-time":"2023-09-14T14:33:56Z","timestamp":1694702036000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-43369-6_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031433689","9783031433696"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-43369-6_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"13 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FroCoS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Frontiers of Combining Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 September 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 September 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"frocos2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/frocos2023.github.io\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}