{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:38:08Z","timestamp":1740109088384,"version":"3.37.3"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,5,1]],"date-time":"2017-05-01T00:00:00Z","timestamp":1493596800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["ProofCert"],"award-info":[{"award-number":["ProofCert"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2017,5]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            In a world where trusting software systems is increasingly important, formal methods and formal proof can help provide some basis for trust. Proof checking can help to reduce the size of the\n            <jats:italic>trusted base<\/jats:italic>\n            since we do not need to trust an entire theorem prover: instead, we only need to trust a (smaller and simpler) proof checker. Many approaches to building proof checkers require embedding within them a full programming language. In most modern proof checkers and theorem provers, that programming language is a functional programming language, often a variant of ML. In fact, aspects of ML (e.g., strong typing, abstract datatypes, and higher-order programming) were designed to make ML a trustworthy \u201cmeta-language\u201d for checking proofs. While there is considerable overlap between logic programming and proof checking (e.g., both benefit from unification, backtracking search, efficient term structures, etc.), the discipline of logic programming has, in fact, played a minor role in the history of proof checking. I will argue that logic programming can have a major role in the future of this important topic.\n          <\/jats:p>","DOI":"10.1007\/s00165-016-0393-z","type":"journal-article","created":{"date-parts":[[2016,9,5]],"date-time":"2016-09-05T05:53:02Z","timestamp":1473054782000},"page":"383-399","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Proof checking and logic programming"],"prefix":"10.1145","volume":"29","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0274-4954","authenticated-orcid":false,"given":"Dale","family":"Miller","sequence":"first","affiliation":[{"name":"Inria Saclay &amp; LIX, \u00c9cole Polytechnique, 1 rue Honor\u00e9 d\u2019Estienne d\u2019Orves, B\u00e2timent Alan Turing, 91120, Palaiseau, France"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_2_1_2_2_2","unstructured":"Assaf A (2015) A framework for defining computational higher-order logics. PhD thesis \u00c9cole Polytechnique"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Baelde D (2012) Least and greatest fixed points in linear logic. ACM Trans Comput Logic 13(1)","DOI":"10.1145\/2071368.2071370"},{"key":"e_1_2_1_2_4_2","unstructured":"Baelde D Chaudhuri K Gacek A Miller D Nadathur G Tiu A Wang Y (2014) Abella: a system for reasoning about relational specifications. J Formal Reas 7(2)"},{"key":"e_1_2_1_2_5_2","first-page":"391","volume-title":"21th conference on automated deduction (CADE). LNAI, vol 4603","author":"Baelde D","year":"2007"},{"volume-title":"A computational logic","year":"1979","author":"Boyer RS","key":"e_1_2_1_2_6_2"},{"key":"e_1_2_1_2_7_2","first-page":"92","volume-title":"International conference on logic for programming and automated reasoning (LPAR), vol 4790","author":"Baelde D","year":"2007"},{"key":"e_1_2_1_2_8_2","first-page":"7","volume-title":"Proceedings first international workshop on focusing. Electronic proceedings in theoretical computer science, vol 197","author":"Blanco R","year":"2015"},{"key":"#cr-split#-e_1_2_1_2_9_2.1","doi-asserted-by":"crossref","unstructured":"Cousineau D Dowek G (2007) Embedding pure type systems in the lambda-Pi-calculus modulo. In: Ronchi Della Rocca S","DOI":"10.1007\/978-3-540-73228-0_9"},{"key":"#cr-split#-e_1_2_1_2_9_2.2","unstructured":"(ed) Typed lambda calculi and applications 8th international conference TLCA 2007 Paris France June 26-28 2007 proceedings vol 4583. LNCS Springer Berlin pp 102-117"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1007\/978-3-319-24312-2_14","volume-title":"Proceedings of the 24th automated reasoning with analytic tableaux and related methods (TABLEAUX), vol 9323","author":"Chihani Z","year":"2015"},{"key":"#cr-split#-e_1_2_1_2_12_2.1","doi-asserted-by":"crossref","unstructured":"Chihaniz MD (2016) Proof certificates for equality reasoning. In: Benevides M Thiemann R","DOI":"10.1016\/j.entcs.2016.06.007"},{"key":"#cr-split#-e_1_2_1_2_12_2.2","unstructured":"(ed) Post-proceedings of LSFA 2015: 10th workshop on logical and semantic frameworks with applications. Natal Brazil vol 323. ENTCS UK"},{"key":"#cr-split#-e_1_2_1_2_13_2.1","doi-asserted-by":"crossref","unstructured":"Chihani Z Miller D Renaud F (2013) Foundational proof certificates in first-order logic. In: Paola Bonacina M","DOI":"10.1007\/978-3-642-38574-2_11"},{"key":"#cr-split#-e_1_2_1_2_13_2.2","unstructured":"(ed) CADE 24: conference on automated deduction 2013 vol 7898. LNAI Berlin pp 162-177"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Chihani Z Miller D Renaud F (2016) A semantic framework for proof evidence. J Autom Reas (Published electronically) . doi:10.1007\/s10817-016-9380-6","DOI":"10.1007\/s10817-016-9380-6"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-007-9091-0"},{"key":"e_1_2_1_2_16_2","unstructured":"The Dedukti system (2013). https:\/\/www.rocq.inria.fr\/deducteam\/Dedukti\/index.html"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Dunchev C Guidi F Coen CS Tassi E (2015) ELPI: fast embeddable \u03bbProlog interpreter. In: Davis M Fehnker A McIver A Voronkov A (eds) Logic for programming artificial intelligence and reasoning\u201420th international conference LPAR-20 2015 Suva Fiji November 24\u201328 2015 proceedings vol 9450. LNCS Springer Berlin pp 460\u2013468","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"e_1_2_1_2_18_2","first-page":"211","volume-title":"Advances in linear logic, vol 222. London mathematical society lecture note series","author":"Danos V","year":"1995"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm037"},{"key":"e_1_2_1_2_20_2","first-page":"68","volume-title":"The collected papers of Gerhard Gentzen","author":"Gentzen G","year":"1935"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001328"},{"key":"e_1_2_1_2_23_2","unstructured":"Girard JY (1992) A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs.stanford.edu"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9218-1"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: a mechanised logic of computation, vol 78","author":"Gordon MJ","year":"1979"},{"key":"e_1_2_1_2_26_2","first-page":"333","volume-title":"8th Asian symposium on computer mathematics, vol 5081","author":"Gonthier G","year":"2007"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"publisher","DOI":"10.4007\/annals.2005.162.1065"},{"key":"e_1_2_1_2_28_2","unstructured":"Herbelin H (1995) S \u00e9quents qu\u2019on calcule: de l\u2019interpr\u00e9tation du calcul des s\u00e9quents comme calcul de lambda-termes et comme calcul de strat\u00e9gies gagnantes. PhD thesis Universit\u00e9 Paris 7"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_2_1_2_30_2","first-page":"11","volume-title":"Proceedings of the fourth workshop on proof exchange for theorem proving. Electronic proceedings in theoretical computer science, vol 186","author":"Heath Q","year":"2015"},{"key":"e_1_2_1_2_31_2","unstructured":"Howe J.M (1998) Proof search issues in some non-classical logics. PhD thesis University of St Andrews. University of St Andrews Research Report CS\/99\/1"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Klein G Elphinstone K Heiser G Andronick J Cock D Derrin P Elkaduwe D Engelhardt K Kolanski R Norrish M Sewell T Tuch H Winwood S (2009) seL4: formal verification of an OS kernel. In: Proceedings of the 22nd symposium on operating systems principles (22nd SOSP\u201909) operating systems review (OSR). ACM SIGOPS Big Sky pp 207\u2013220","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Konev B Lisitsa A (2014) A SAT attack on the Erd\u0151s discrepancy conjecture. In: International conference on theory and applications of satisfiability testing vol 8561. LNCS Springer Berlin pp 219\u2013226","DOI":"10.1007\/978-3-319-09284-3_17"},{"key":"e_1_2_1_2_34_2","unstructured":"Laurent O (2002) Etude de la polarisation en logique. PhD thesis Universit\u00e9 Aix-Marseille II"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"e_1_2_1_2_37_2","unstructured":"Meng J (2015) The integration of higher order interactive proof with first order automatic theorem proving. PhD thesis University of Cambridge Computer Laboratory"},{"volume-title":"Communication and concurrency","year":"1989","author":"Milner R","key":"e_1_2_1_2_38_2"},{"key":"e_1_2_1_2_39_2","first-page":"329","volume-title":"Logic and computer science","author":"Miller D","year":"1990"},{"key":"e_1_2_1_2_40_2","unstructured":"Miller D (2011) ProofCert: broad spectrum proof certificates. An ERC advanced grant funded for the five years 2012\u20132016"},{"key":"e_1_2_1_2_41_2","first-page":"54","volume-title":"CPP: first international conference on certified programs and proofs, vol 7086","author":"Miller D","year":"2011"},{"key":"e_1_2_1_2_42_2","unstructured":"Miller D (2014) Communicating and trusting proofs: the case for broad spectrum proof certificates. In: Schroeder-Heister P Hodges W Heinzmann G Bour PE (eds) Logic methodology and philosophy of science. Proceedings of the fourteenth international congress. College Publications Wenham pp 323\u2013342"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00171-1"},{"key":"e_1_2_1_2_44_2","unstructured":"Marin S Miller D Volpe M (2016) A focused framework for emulating modal proof systems. In: Advances in modal logics (To appear)"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"publisher","DOI":"10.5555\/2331097"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90068-W"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/1094622.1094628"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1007\/978-3-662-48899-7_19","volume-title":"Logic for programming, artificial intelligence, and reasoning (LPAR), vol 9450","author":"Miller D","year":"2015"},{"key":"#cr-split#-e_1_2_1_2_49_2.1","doi-asserted-by":"crossref","unstructured":"Nadathur G Mitchell DJ (1999) System description: Teyjus-a compiler and abstract machine based implementation of \u03bbProlog. In: Ganzinger H","DOI":"10.1007\/3-540-48660-7_25"},{"key":"#cr-split#-e_1_2_1_2_49_2.2","unstructured":"(ed) 16th conf. on automated deduction (CADE) vol 1632. LNAI Springer Trento pp 287-291"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Necula GC Rahul SP (2001) Oracle-based checking of untrusted software. In: Hankin C Schmidt D (eds) 28th ACM symp. on principles of programming languages pp 142\u2013154","DOI":"10.1145\/373243.360216"},{"key":"e_1_2_1_2_51_2","unstructured":"Pereira F (1988) C-Prolog user\u2019s manual version 1.5"},{"key":"#cr-split#-e_1_2_1_2_52_2.1","doi-asserted-by":"crossref","unstructured":"Pfenning F Sch\u00fcrmann C (1999) System description: Twelf-a meta-logical framework for deductive systems. In: Ganzinger H","DOI":"10.1007\/3-540-48660-7_14"},{"key":"#cr-split#-e_1_2_1_2_52_2.2","unstructured":"(ed) 16th conf. on automated deduction (CADE) vol 1632. LNAI Springer Trento pp 202-206"},{"key":"e_1_2_1_2_53_2","first-page":"222","volume-title":"8th symp. on logic in computer science","author":"Schroeder-Heister P","year":"1993"},{"key":"e_1_2_1_2_54_2","unstructured":"Tiu A Nadathur G Miller D (2005) Mixing finite success and finite failure in an automated prover. In: Empirically successful automated reasoning in higher-order logics (ESHOL\u201905) pp 79\u201398"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and applications of satisfiability testing SAT 2014, vol 8561","author":"Wetzler N","year":"2014"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-016-0393-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0393-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-016-0393-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-016-0393-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,7]],"date-time":"2022-01-07T06:56:15Z","timestamp":1641538575000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-016-0393-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5]]},"references-count":60,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,5]]}},"alternative-id":["10.1007\/s00165-016-0393-z"],"URL":"https:\/\/doi.org\/10.1007\/s00165-016-0393-z","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2017,5]]}}}