{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:07Z","timestamp":1761611107413,"version":"3.41.0"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,9,1]],"date-time":"2002-09-01T00:00:00Z","timestamp":1030838400000},"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,9]]},"DOI":"10.1023\/a:1021983302516","type":"journal-article","created":{"date-parts":[[2003,3,21]],"date-time":"2003-03-21T23:56:29Z","timestamp":1048290989000},"page":"365-387","source":"Crossref","is-referenced-by-count":9,"title":["A New Implementation of Automath"],"prefix":"10.1007","volume":"29","author":[{"given":"Freek","family":"Wiedijk","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5109773_CR1","unstructured":"Balsters, H.: Lambda calculus extended with segments, Ph.D. thesis, Eindhoven University of Technology, 1986."},{"key":"5109773_CR2","first-page":"117","volume-title":"Handbook of Logic in Computer Science","author":"H. Barendregt","year":"1992","unstructured":"Barendregt, H.: Lambda calculi with types, in S. Abramsky, D. Gabbay and T. Maibaum (eds), Handbook of Logic in Computer Science, Vol. II, Oxford University Press, 1992, pp. 117\u2013309."},{"key":"5109773_CR3","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. de Bruijn","year":"1972","unstructured":"de Bruijn, N.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church\u2013Rosser theorem, Indigationes Math. 34 (1972), 381\u2013392. (C.2) in (Nederpelt et al., 1994).","journal-title":"Indigationes Math"},{"key":"5109773_CR4","first-page":"71","volume-title":"Mathematical Logic and Theoretical Computer Science","author":"N. de Bruijn","year":"1987","unstructured":"de Bruijn, N.: Generalizing Automath by means of a lambda-typed lambda calculus, in D. Kueker, E. Lopez-Escobar and C. Smith (eds), Mathematical Logic and Theoretical Computer Science, Lecture Notes in Pure and Appl. Math. 106, Marcel Dekker, New York, 1987, pp. 71\u201392. (B.7) in (Nederpelt et al., 1994)."},{"key":"5109773_CR5","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1016\/0890-5401(91)90066-B","volume":"91","author":"N. de Bruijn","year":"1991","unstructured":"de Bruijn, N.: Telescopic mappings in typed lambda calculus, Inform. Comput.\n91 (1991), 189\u2013204.","journal-title":"Inform. Comput."},{"key":"5109773_CR6","doi-asserted-by":"crossref","unstructured":"de Groote, P.: Defining \u03bb-typed \u03bb-calculi by axiomatizing the typing relation, Technical Report CRIN 93-R-003, Centre de Recherche en Informatique de Nancy, 1993.","DOI":"10.1007\/3-540-56503-5_9"},{"key":"5109773_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M. Gordon","year":"1979","unstructured":"Gordon, M., Milner, R. and Wadsworth, C.: Edinburgh LCF: A Mechanised Logic of Computation, LNCS 78, Springer-Verlag, Berlin, 1979."},{"key":"5109773_CR8","unstructured":"Harper, R., Honsell, F. and Plotkin, G.: A framework for defining logics, Technical Report ECSLFCS-91-162, Laboratory for Foundations of Computer Science, Department of Computer Science, The University of Edinburgh, 1991."},{"key":"5109773_CR9","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/S0168-0072(98)00019-0","volume":"97","author":"F.R. Bloo","year":"1999","unstructured":"F., Bloo, R. and Nederpelt, R.: On \u041f-conversion in the \u03bb-cube and the combination with abbreviations, Ann. Pure Appl. Logic\n97 (1999), 27\u201345.","journal-title":"Ann. Pure Appl. Logic"},{"key":"5109773_CR10","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1017\/S0956796800001672","volume":"6","author":"F. Kamareddine","year":"1996","unstructured":"Kamareddine, F. and Nederpelt, R.: Canonical typing and \u041f-conversion in the Barendregt cube, J. Funct. Programming\n6 (1996), 245\u2013267.","journal-title":"J. Funct. Programming"},{"key":"5109773_CR11","unstructured":"Landau E.: Grundlagen der Analysis, 4th edn, Chelsea, New York, 1965. First edition 1930."},{"key":"5109773_CR12","unstructured":"Megill, N. D.: Metamath, a computer language for pure mathematics, 1997. <http:\/\/metamath.org\/>. A NEW IMPLEMENTATION OF AUTOMATH 387"},{"key":"5109773_CR13","volume-title":"Selected Papers on Automath","author":"R. Nederpelt","year":"1994","unstructured":"Nederpelt, R., Geuvers, J. and de Vrijer, R.: Selected Papers on Automath, Studies in Logic and the Foundations of Mathematics, Elsevier Science, Amsterdam, 1994."},{"key":"5109773_CR14","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L. and Wenzel, M.: Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic, LNCS 2283, Springer, 2002.","DOI":"10.1007\/3-540-45949-9"},{"key":"5109773_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","author":"L. Paulson","year":"1994","unstructured":"Paulson, L.: Isabelle: A Generic Theorem Prover, LNCS 828, Springer-Verlag, New York, 1994."},{"key":"5109773_CR16","doi-asserted-by":"crossref","unstructured":"Pfenning, F.: The practice of logical frameworks, in H. Kirchner (ed.), Proceedings of the Colloquium on Trees in Algebra and Programming, Link\u00f6ping, Sweden, LNCS 1059, Springer-Verlag, 1996, pp. 119\u2013134. <http:\/\/www.cs.cmu.edu\/~fp\/papers\/caap96.ps.gz>.","DOI":"10.1007\/3-540-61064-2_33"},{"key":"5109773_CR17","unstructured":"The Coq Development Team: The Coq Proof Assistant Reference Manual, 2002. <ftp:\/\/ftp.inria.fr\/INRIA\/coq\/current\/doc\/Reference-Manual-all.ps.gz>."},{"key":"5109773_CR18","unstructured":"van Benthem Jutting, L.: A translation of Landau's \u201cGrundlagen\u201d in AUTOMATH, Technical Report, Eindhoven University of Technology, 1976."},{"key":"5109773_CR19","volume-title":"Mathematical Centre Tracts","author":"L. van Benthem Jutting","year":"1979","unstructured":"van Benthem Jutting, L.: Checking Landau's \u201cGrundlagen\u201d in the Automath System, Mathematical Centre Tracts 83, Mathematisch Centrum, Amsterdam, 1979."},{"key":"5109773_CR20","series-title":"Technical Report","volume-title":"Typing in pure type systems","author":"L. van Benthem Jutting","year":"1990","unstructured":"van Benthem Jutting, L.: Typing in pure type systems, Technical Report, Dept. Computer Science, University of Nijmegen, Nijmegen, 1990."},{"key":"5109773_CR21","doi-asserted-by":"crossref","unstructured":"van Daalen, D.: A description of Automath and some aspects of its language theory, in P. Braffort (ed.), Proceedings of the Symposium APLASM, Vol. 1, Orsay, 1973. (A.3) in (Nederpelt et al., 1994).","DOI":"10.1016\/S0049-237X(08)70201-5"},{"key":"5109773_CR22","unstructured":"van Daalen, D.: The language theory of Automath, Ph.D. thesis, Eindhoven University of Technology, 1980."},{"key":"5109773_CR23","unstructured":"Wiedijk, F.: The De Bruijn factor, 2000. <http:\/\/www.cs.kun.nl\/~freek\/notes\/factor.ps.gz>."},{"key":"5109773_CR24","unstructured":"Wiedijk, F.: The fifteen provers of the world, 2002. <http:\/\/www.cs.kun.nl\/~freek\/comparison.ps.gz>."},{"key":"5109773_CR25","doi-asserted-by":"crossref","unstructured":"Zandleven, I.: A verifying program for Automath, in P. Braffort (ed.), Proceedings of the Symposium APLASM, Vol. I, Orsay, 1973. (E.1) in (Nederpelt et al., 1994).","DOI":"10.1016\/S0049-237X(08)70226-X"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021983302516.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021983302516\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021983302516.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:30:37Z","timestamp":1749123037000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021983302516"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":25,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2002,9]]}},"alternative-id":["5109773"],"URL":"https:\/\/doi.org\/10.1023\/a:1021983302516","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2002,9]]}}}