{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T17:40:05Z","timestamp":1703958005672},"reference-count":13,"publisher":"Elsevier BV","issue":"1-2","license":[{"start":{"date-parts":[[2002,2,1]],"date-time":"2002-02-01T00:00:00Z","timestamp":1012521600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,17]],"date-time":"2013-07-17T00:00:00Z","timestamp":1374019200000},"content-version":"vor","delay-in-days":4184,"URL":"https:\/\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theoretical Computer Science"],"published-print":{"date-parts":[[2002,2]]},"DOI":"10.1016\/s0304-3975(00)00354-6","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T10:11:15Z","timestamp":1027591875000},"page":"293-314","source":"Crossref","is-referenced-by-count":3,"title":["Proof by computation in the Coq system"],"prefix":"10.1016","volume":"272","author":[{"given":"Martijn","family":"Oostdijk","sequence":"first","affiliation":[]},{"given":"Herman","family":"Geuvers","sequence":"additional","affiliation":[]}],"member":"78","reference":[{"key":"10.1016\/S0304-3975(00)00354-6_BIB1","doi-asserted-by":"crossref","unstructured":"H. Barendregt, Lambda Calculi with Types, in: S. Abramsky, D.M. Gabbay, T.S.E. Maibaum (Eds.), Handbook of Logic in Computer Science, Vol. II, Clarendon Press., Oxford, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"10.1016\/S0304-3975(00)00354-6_BIB2","unstructured":"H. Barendregt, E. Barendsen, Autarkic Computations in Formal Proofs, Computing Science Institute, University of Nijmegen, 1997."},{"key":"10.1016\/S0304-3975(00)00354-6_BIB3","series-title":"Types for Proofs and Programs, TYPES\u201995, LNCS","first-page":"16","article-title":"A Two-Level Approach towards lean Proof-Checking","author":"Barthe","year":"1995"},{"key":"10.1016\/S0304-3975(00)00354-6_BIB4","doi-asserted-by":"crossref","unstructured":"S. Boutin, Using reflection to build efficient and certified decision procedures, in: M. Abadi, T. Ieo (Eds.), LNCS, 1281, Springer, Berlin, 1997.","DOI":"10.1007\/BFb0014565"},{"key":"10.1016\/S0304-3975(00)00354-6_BIB5","doi-asserted-by":"crossref","unstructured":"Th. Coquand, Ch. Paulin-Mohring, Inductively defined types, in: P. Martin-L\u00f6f, G. Mints (Eds.), COLOG-88: Internat. Conf. on Computer Logic, vol. 417, Springer, Berlin, 1990.","DOI":"10.1007\/3-540-52335-9_47"},{"key":"10.1016\/S0304-3975(00)00354-6_BIB6","unstructured":"H.J. Elbers, Connecting informal and formal mathematics, Ph.D. Thesis, Eindhoven University of Technology, 1998."},{"key":"10.1016\/S0304-3975(00)00354-6_BIB7","unstructured":"J. Harrison, Metatheory and reflection in theorem proving: a survey and critique, Technical Report CRC-053, SRI International Cambridge Computer Science Research Centre, 1995."},{"key":"10.1016\/S0304-3975(00)00354-6_BIB8","doi-asserted-by":"crossref","unstructured":"D. Howe, Computational metatheory in Nuprl, in: E. Lusk, R. Overbeek (Eds.), Proc. 9th Internat. Conf. of Automated Deduction, Lecture Notes in Computer Science, vol. 310, Springer, Berlin, 1988,, pp. 238\u2013257.","DOI":"10.1007\/BFb0012835"},{"key":"10.1016\/S0304-3975(00)00354-6_BIB9","unstructured":"G. Huet et al., The Coq Proof Assistant, Reference Manual, Version 6.1, INRIA-Rocquencourt \u2013 CNRS-ENS Lyon, 1997."},{"key":"10.1016\/S0304-3975(00)00354-6_BIB10","unstructured":"M. Huisman, Binary addition in Lego, Technical Report CSI-R9716, Computing Science Institute, University of Nijmegen, 1997."},{"key":"10.1016\/S0304-3975(00)00354-6_BIB11","unstructured":"Z. Luo, R. Pollack, LEGO Proof Development System: User's Manual, Department of Computer Science, University of Edinburgh, 1992 (1993, 1994)."},{"key":"10.1016\/S0304-3975(00)00354-6_BIB12","unstructured":"M. Oostdijk, Proof by calculation, Master's Thesis 385, Universitaire School voor Informatica, University of Nijmegen, 1996."},{"key":"10.1016\/S0304-3975(00)00354-6_BIB13","unstructured":"M. Oostdijk, H. Geuvers, Coq proof development files, 1998, http:\/\/www.win.tue.nl\/martijno\/work\/reflection\/."}],"container-title":["Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500003546?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0304397500003546?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T17:22:38Z","timestamp":1703956958000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0304397500003546"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,2]]},"references-count":13,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2002,2]]}},"alternative-id":["S0304397500003546"],"URL":"https:\/\/doi.org\/10.1016\/s0304-3975(00)00354-6","relation":{},"ISSN":["0304-3975"],"issn-type":[{"value":"0304-3975","type":"print"}],"subject":[],"published":{"date-parts":[[2002,2]]}}}