{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,6]],"date-time":"2025-06-06T04:06:47Z","timestamp":1749182807402,"version":"3.41.0"},"reference-count":13,"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:1021977414812","type":"journal-article","created":{"date-parts":[[2003,3,21]],"date-time":"2003-03-21T23:56:29Z","timestamp":1048290989000},"page":"183-188","source":"Crossref","is-referenced-by-count":0,"title":["Preface: Mechanizing and Automating Mathematics: In honour of N.G. de Bruijn"],"prefix":"10.1007","volume":"29","author":[{"given":"Fairouz","family":"Kamareddine","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"5109764_CR1","unstructured":"van Benthem Jutting, L. S.: A translation of Landau's \u201cGrundlagen\u201d in AUTOMATH, Technical Report, Eindhoven University of Technology, 1976."},{"key":"5109764_CR2","volume-title":"Checking Landau's \u201cGrundlagen\u201d in the Automath system","author":"L. S. van Benthem Jutting","year":"1977","unstructured":"van Benthem Jutting, L. S.: Checking Landau's \u201cGrundlagen\u201d in the Automath system, Ph.D. thesis, Eindhoven University of Technology, 1977. Published as Mathematical Centre Tracts nr. 83 (Amsterdam, Mathematisch Centrum, 1979)."},{"key":"5109764_CR3","unstructured":"de Bruijn, N. G.: AUTOMATH, a language for mathematics, Technical Report 68-WSK-05, T.H.-Reports, Eindhoven University of Technology, 1968."},{"key":"5109764_CR4","doi-asserted-by":"crossref","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, IRIA, Versailles, 1968, pp. 29\u201361. Lecture Notes in Math. 125, Springer-Verlag, Berlin, 1970; also in [12], pp. 73\u2013100.","DOI":"10.1007\/BFb0060623"},{"key":"5109764_CR5","first-page":"201","volume":"12","author":"N. G. de Bruijn","year":"1990","unstructured":"de Bruijn, N. G.: Reflections on Automath, Eindhoven University of Technology, 1990. Also in [12], pp. 201\u2013228.","journal-title":"Reflections on Automath"},{"issue":"5","key":"5109764_CR6","doi-asserted-by":"crossref","first-page":"381","DOI":"10.1016\/1385-7258(72)90034-0","volume":"34","author":"N. G. de Bruijn","year":"1972","unstructured":"de Bruijn, N. G.: Lambda-Calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church\u2013Rosser Theorem, Indag. Mat.\n34(5) (1972), 381\u2013392.","journal-title":"Indag. Mat."},{"issue":"2\/3","key":"5109764_CR7","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, Inform. and Comput.\n76(2\/3) (February\/March 1988), 95\u2013120.","journal-title":"Inform. and Comput."},{"key":"5109764_CR8","volume-title":"Combinatory Logic I","author":"H. B. Curry","year":"1958","unstructured":"Curry, H. B. and Feys, R.: Combinatory Logic I, Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, 1958."},{"key":"5109764_CR9","first-page":"479","volume":"13","author":"W. A. Howard","year":"1980","unstructured":"Howard, W. A.: The formulas-as-types notion of construction, in [13], 1980, pp. 479\u2013490.","journal-title":"The formulas-as-types notion of construction"},{"key":"5109764_CR10","unstructured":"Laan, T.: The evolution of type theory in logic and mathematics, Ph.D. thesis, Eindhoven University of Technology, 1997."},{"key":"5109764_CR11","unstructured":"Landau, E.: Grundlagen der Analysis, Leipzig, 1930."},{"key":"5109764_CR12","unstructured":"Nederpelt, R., Geuvers, J. H. and de Vrijer, R. C.: Selected Papers on Automath, North-Holland, Amsterdam, 1994."},{"volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","year":"1980","key":"5109764_CR13","unstructured":"Seldin, J. P. and Hindley, J. R. (eds), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, New York, 1980."}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021977414812.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1021977414812\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1021977414812.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,5]],"date-time":"2025-06-05T11:30:49Z","timestamp":1749123049000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1021977414812"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,9]]},"references-count":13,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2002,9]]}},"alternative-id":["5109764"],"URL":"https:\/\/doi.org\/10.1023\/a:1021977414812","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2002,9]]}}}