{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:03Z","timestamp":1774837803223,"version":"3.50.1"},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2002,4,1]],"date-time":"2002-04-01T00:00:00Z","timestamp":1017619200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,4,1]],"date-time":"2002-04-01T00:00:00Z","timestamp":1017619200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Journal of Automated Reasoning"],"published-print":{"date-parts":[[2002,4]]},"DOI":"10.1023\/a:1015761529444","type":"journal-article","created":{"date-parts":[[2002,12,29]],"date-time":"2002-12-29T00:56:06Z","timestamp":1041123366000},"page":"321-336","source":"Crossref","is-referenced-by-count":43,"title":["Autarkic Computations in Formal Proofs"],"prefix":"10.1007","volume":"28","author":[{"given":"Henk","family":"Barendregt","sequence":"first","affiliation":[]},{"given":"Erik","family":"Barendsen","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"390383_CR1","volume-title":"Images of SMC Research 1996","year":"1996","unstructured":"Aspers, W. A. M., de Bakker, J. W., ten Hagen, P. J. W., Hazewinkel, M., van der Houwen, P. J., and Nieland, H. M. (eds.): Images of SMC Research 1996, Stichting Mathematisch Centrum, Amsterdam, 1996."},{"key":"390383_CR2","doi-asserted-by":"crossref","unstructured":"Barendregt, H. P.: Lambda calculi with types, in S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum (eds.), Handbook of Logic in Computer Science, Vol. 2, Oxford University Press, 1992, pp. 117\u2013309.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"390383_CR3","unstructured":"Barendregt, H. P.: The quest for correctness, in Aspers et al., 1996, pp. 39\u201358."},{"key":"390383_CR4","volume-title":"A Computational Logic","author":"R. S. Boyer","year":"1988","unstructured":"Boyer, R. S. and Moore, J S.: A Computational Logic, Academic Press, New York, 1988."},{"key":"390383_CR5","series-title":"INRIA, Versailles, Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/BFb0060623","volume-title":"Symposium on Automatic Demonstration","author":"N. G. de Bruijn","year":"1970","unstructured":"de Bruijn, N. G.: The mathematical language AUTOMATH, its usage and some of its extensions, in M. Laudet, D. Lacombe, and M. Schuetzenberger (eds.), Symposium on Automatic Demonstration, INRIA, Versailles, Lecture Notes in Comput. Sci. 125, Springer-Verlag, Berlin, 1970, pp. 29\u201361. Also in Nederpelt et al., 1994."},{"key":"390383_CR6","doi-asserted-by":"crossref","unstructured":"de Bruijn, N. G.: Reflections on Automath 1990. Also in Nederpelt et al., 1994, pp. 201\u2013228.","DOI":"10.1016\/S0049-237X(08)70205-2"},{"key":"390383_CR7","series-title":"Lecture Notes in Comput. Sci.","volume-title":"CADE-12","year":"1984","unstructured":"Bundy, A. (ed.): CADE-12, Lecture Notes in Comput. Sci. 814, Springer-Verlag, Berlin, 1984."},{"key":"390383_CR8","doi-asserted-by":"crossref","unstructured":"Cohen, A. M.: Computers: (Ac)counting for mathematical proofs, in Aspers et al., 1996, pp. 15\u201338.","DOI":"10.1016\/S0167-4048(96)00009-0"},{"key":"390383_CR9","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"R. L. Constable","year":"1986","unstructured":"Constable, R. L.: Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, Englewood Cliffs, New Jersey, 1986."},{"key":"390383_CR10","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T. and Huet, G.: The calculus of constructions, Information and Computation\n76 (1988), 95\u2013120. Available at URL: http:\/\/pauillac.inria.fr\/coq\/coq-eng.html.","journal-title":"Information and Computation"},{"key":"390383_CR11","unstructured":"Elbers, H.: Personal communication, 1996."},{"key":"390383_CR12","unstructured":"Luo, Z. and Pollack, R.: The LEGO proof development system: A user's manual, Technical Report ECS-LFCS-92-211, University of Edinburgh, 1992. LEGO system available via URL http:\/\/www.dcs.ed.ac.uk\/packages\/lego\/."},{"key":"390383_CR13","doi-asserted-by":"crossref","DOI":"10.21236\/AD0406138","volume-title":"LISP 1.5 Programmer's Manual","author":"J. McCarthy","year":"1962","unstructured":"McCarthy, J.: LISP 1.5 Programmer's Manual, MIT Press, Cambridge, MA, 1962."},{"key":"390383_CR14","unstructured":"Nederpelt, R. P., Geuvers, J. H., and de Vrijer, R. C. (eds.): Selected Papers on Automath, Studies in Logic 133, North-Holland, Amsterdam, 1994."},{"key":"390383_CR15","unstructured":"Oostdijk, M.: Proof by Calculation, Master's thesis 385, Universitaire School voor Informatica, University of Nijmegen, 1996."},{"key":"390383_CR16","unstructured":"Poincar\u00e9, H.: La Science et l'Hypoth\u00e8se, Flammarion, Paris. 1902."},{"key":"390383_CR17","unstructured":"Ruys, M. P. J.: Studies in Mechanical Verification of Mathematical Proofs, Dissertation, University of Nijmegen, 1999."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015761529444.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1015761529444\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1015761529444.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:34:11Z","timestamp":1749123251000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1015761529444"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,4]]},"references-count":17,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2002,4]]}},"alternative-id":["390383"],"URL":"https:\/\/doi.org\/10.1023\/a:1015761529444","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2002,4]]}}}