{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T23:00:28Z","timestamp":1776553228895,"version":"3.51.2"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2022,1,11]],"date-time":"2022-01-11T00:00:00Z","timestamp":1641859200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["J 4386"],"award-info":[{"award-number":["J 4386"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2022,1,17]]},"DOI":"10.1145\/3497775.3503683","type":"proceedings-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T05:20:48Z","timestamp":1641964848000},"page":"225-238","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Safe, fast, concurrent proof checking for the lambda-pi calculus modulo rewriting"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1634-9525","authenticated-orcid":false,"given":"Michael","family":"F\u00e4rber","sequence":"first","affiliation":[{"name":"University of Innsbruck, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:JARS.0000021013.61329.58"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/s12046-009-0003-3"},{"key":"e_1_3_2_1_4_1","unstructured":"Ali Assaf Guillaume Burel Rapha\u00ebl Cauderlier David Delahaye Gilles Dowek Catherine Dubois Fr\u00e9d\u00e9ric Gilbert Pierre Halmagrand Olivier Hermant and Ronan Saillard. [n.d.]. Dedukti: a Logical Framework based on the \u03bb \u03a0 -Calculus Modulo Theory. http:\/\/www.lsv.ens-cachan.fr\/~dowek\/Publi\/expressing.pdf  Ali Assaf Guillaume Burel Rapha\u00ebl Cauderlier David Delahaye Gilles Dowek Catherine Dubois Fr\u00e9d\u00e9ric Gilbert Pierre Halmagrand Olivier Hermant and Ronan Saillard. [n.d.]. Dedukti: a Logical Framework based on the \u03bb \u03a0 -Calculus Modulo Theory. http:\/\/www.lsv.ens-cachan.fr\/~dowek\/Publi\/expressing.pdf"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2005.1650"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39320-4_29"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_4"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_3"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09533-z"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/4596"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24312-2_14"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-25979-4_5"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_9"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-29026-9_2"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.5729640"},{"key":"e_1_3_2_1_17_1","first-page":"1382","article-title":"Formal Proof\u2014The Four-Color Theorem","volume":"55","author":"Gonthier Georges","year":"2008","unstructured":"Georges Gonthier . 2008 . Formal Proof\u2014The Four-Color Theorem . Notices of the American Mathematical Society , 55 (2008), 1382 \u2013 1393 . http:\/\/www.ams.org\/notices\/200811\/tx081101382p.pdf Georges Gonthier. 2008. Formal Proof\u2014The Four-Color Theorem. Notices of the American Mathematical Society, 55 (2008), 1382\u20131393. http:\/\/www.ams.org\/notices\/200811\/tx081101382p.pdf","journal-title":"Notices of the American Mathematical Society"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/fmp.2017.1"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_4"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.35"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676724.2693176"},{"key":"e_1_3_2_1_24_1","volume-title":"Wheeler","author":"Megill Norman D.","year":"2019","unstructured":"Norman D. Megill and David A . Wheeler . 2019 . Metamath : A Computer Language for Mathematical Proofs. Lulu Press , Morrisville, North Carolina. http:\/\/us.metamath.org\/downloads\/metamath.pdf Norman D. Megill and David A. Wheeler. 2019. Metamath: A Computer Language for Mathematical Proofs. Lulu Press, Morrisville, North Carolina. http:\/\/us.metamath.org\/downloads\/metamath.pdf"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0055144"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_31"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0163-3"},{"key":"e_1_3_2_1_30_1","volume-title":"Harley Eades, Corey Oliver, and Ruoyu Zhang.","author":"Stump Aaron","year":"2012","unstructured":"Aaron Stump , Andrew Reynolds , Cesare Tinelli , Austin Laugesen , Harley Eades, Corey Oliver, and Ruoyu Zhang. 2012 . LFSC for SMT Proofs: Work in Progress. In Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012. Proceedings, David Pichardie and Tjark Weber (Eds.) (CEUR Workshop Proceedings , Vol. 878). CEUR-WS.org, 21\u2013 27 . http:\/\/ceur-ws.org\/Vol-878\/paper1.pdf Aaron Stump, Andrew Reynolds, Cesare Tinelli, Austin Laugesen, Harley Eades, Corey Oliver, and Ruoyu Zhang. 2012. LFSC for SMT Proofs: Work in Progress. In Second International Workshop on Proof Exchange for Theorem Proving, PxTP 2012, Manchester, UK, June 30, 2012. Proceedings, David Pichardie and Tjark Weber (Eds.) (CEUR Workshop Proceedings, Vol. 878). CEUR-WS.org, 21\u201327. http:\/\/ceur-ws.org\/Vol-878\/paper1.pdf"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.274.5"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61464-8_71"},{"key":"e_1_3_2_1_33_1","volume-title":"Parallel Proof Checking in Isabelle\/Isar. In The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS)","author":"Wenzel Makarius","year":"2009","unstructured":"Makarius Wenzel . 2009 . Parallel Proof Checking in Isabelle\/Isar. In The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS) . Munich , August 2009, Gabriel Dos Reis and Laurent Th\u00e9ry (Eds.). ACM Digital library. Makarius Wenzel. 2009. Parallel Proof Checking in Isabelle\/Isar. In The ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS). Munich, August 2009, Gabriel Dos Reis and Laurent Th\u00e9ry (Eds.). ACM Digital library."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39634-2_30"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_7"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1021983302516"}],"event":{"name":"CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Philadelphia PA USA","acronym":"CPP '22","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3497775.3503683","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3497775.3503683","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:49:25Z","timestamp":1750193365000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3497775.3503683"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,11]]},"references-count":32,"alternative-id":["10.1145\/3497775.3503683","10.1145\/3497775"],"URL":"https:\/\/doi.org\/10.1145\/3497775.3503683","relation":{},"subject":[],"published":{"date-parts":[[2022,1,11]]},"assertion":[{"value":"2022-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}