{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,4]],"date-time":"2022-04-04T15:23:48Z","timestamp":1649085828037},"reference-count":29,"publisher":"Elsevier BV","issue":"7","license":[{"start":{"date-parts":[[2003,9,1]],"date-time":"2003-09-01T00:00:00Z","timestamp":1062374400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2013,7,29]],"date-time":"2013-07-29T00:00:00Z","timestamp":1375056000000},"content-version":"vor","delay-in-days":3619,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/3.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electronic Notes in Theoretical Computer Science"],"published-print":{"date-parts":[[2003,9]]},"DOI":"10.1016\/s1571-0661(04)80756-4","type":"journal-article","created":{"date-parts":[[2004,9,29]],"date-time":"2004-09-29T16:47:47Z","timestamp":1096476467000},"page":"30-49","source":"Crossref","is-referenced-by-count":0,"title":["Automath and Pure Type Systems"],"prefix":"10.1016","volume":"85","author":[{"given":"Fairouz","family":"Kamareddine","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Twan","family":"Laan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rob","family":"Nederpelt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB1","series-title":"Handbook of Logic in Computer Science","first-page":"117","article-title":"\u03bb-calculi with types","author":"Barendregt","year":"1992"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB2","unstructured":"L.S. van Benthem Jutting. Checking Landau's \u201cGrundlagen\u201d in the Automath system. PhD thesis, Eindhoven University of Technology, 1977. Published as Mathematical Centre Tracts nr. 83, (Amsterdam 1979)."},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB3","doi-asserted-by":"crossref","unstructured":"L.S. van Benthem Jutting. Description of AUT-68. Technical Report 12, Eindhoven University of Technology, 1981. Also in [24], pp. 251\u2013273.","DOI":"10.1016\/S0049-237X(08)70207-6"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB4","unstructured":"S. Berardi. Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt's cube. Technical report, Dept. of Computer Science, Carnegie-Mellon University and Dipartimento Matematica, Universita di Torino, 1988."},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB5","unstructured":"N.G. de Bruijn. AUTOMATH, a language for mathematics. Technical Report 68-WSK-05, T.H.-Reports, Eindhoven University of Technology, 1968."},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB6","doi-asserted-by":"crossref","unstructured":"N.G. de Bruijn. The mathematical language AUTOMATH, its usage and some of its extensions. In M. Laudet, D. Lacombe, and M. Schuetzenberger, editors, Symposium on Automatic Demonstration, pages 29\u201361, IRIA, Versailles, 1968. Springer Verlag, Berlin, 1970. Lecture Notes in Mathematics 125; also in [24].","DOI":"10.1007\/BFb0060623"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB7","unstructured":"N.G. de Bruijn. The Mathematical Vernacular, a language for mathematics with typed sets. In P. Dybjer et al., editors, Proceedings of the Workshop on Programming Languages. Marstrand, Sweden, 1987. Reprinted in [24]."},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB8","doi-asserted-by":"crossref","unstructured":"N.G. de Bruijn. Reflections on Automath. Eindhoven University of Technology, 1990. Also in [24], pages 201\u2013228.","DOI":"10.1016\/S0049-237X(08)70205-2"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB9","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","article-title":"A formulation of the simple theory of types","volume":"5","author":"Church","year":"1940","journal-title":"The Journal of Symbolic Logic"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB10","series-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB11","series-title":"Studies in Logic and the Foundations of Mathematics","article-title":"Combinatory Logic I","author":"Curry","year":"1958"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB12","unstructured":"D.T. van Daalen. The Language Theory of Automath. PhD thesis, Eindhoven University of Technology, 1980."},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB13","unstructured":"G. Dowek et al. The Coq Proof Assistant Version 5.6, Users Guide. Technical Report 134, INRIA, Le Chesney, 1991."},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB14","unstructured":"G. Frege. Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Nebert, Halle, 1879. Also in [16], pages 1\u201382."},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB15","unstructured":"J.H. Geuvers. Logics and Type Systems. PhD thesis, Catholic University of Nijmegen, 1993."},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB16","series-title":"From Frege to G\u00f6del: A Source Book in Mathematical Logic","first-page":"1879","year":"1967"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB17","unstructured":"W.A. Howard. The formulas-as-types notion of construction. In [25], pages 479\u2013490, 1980."},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB18","doi-asserted-by":"crossref","first-page":"27","DOI":"10.1016\/S0168-0072(98)00019-0","article-title":"On \u03c0-conversion in the \u03bb-cube and the combination with abbreviations","volume":"97","author":"Kamareddine","year":"1999","journal-title":"Annals of Pure and Applied Logics"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB19","doi-asserted-by":"crossref","unstructured":"F. Kamareddine, L. Laan, and R.P. Nederpelt. Refining the Barendregt cube using parameters. Fifth International Symposium on Functional and Logic Programming, FLOPS 2001, LNCS 2024:375\u2013389, 2001.","DOI":"10.1007\/3-540-44716-4_24"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB20","doi-asserted-by":"crossref","first-page":"65","DOI":"10.1016\/S1567-8326(02)00016-4","article-title":"Revisiting the notion of function","volume":"54","author":"Kamareddine","year":"2003","journal-title":"Algebraic and Logic Programming"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB21","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/0304-3975(95)00101-8","article-title":"A useful \u03bb-notation","volume":"155","author":"Kamareddine","year":"1996","journal-title":"Theoretical Computer Science"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB22","unstructured":"T. Laan. The Evolution of Type Theory in Logic and Mathematics. PhD thesis, Eindhoven University of Technology, 1997."},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB23","series-title":"Grundlagen der Analysis","author":"Landau","year":"1930"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB24","volume":"133","year":"1994"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB25","series-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","year":"1980"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB26","doi-asserted-by":"crossref","unstructured":"P. Severi and E. Poll. Pure type systems with definitions. In A. Nerode and Yu.V. Matiyasevich, editors, Proceedings of LFCS'94 (LNCS 813), pages 316\u2013328, New York, 1994. LFCS'94, St. Petersburg, Russia, Springer.","DOI":"10.1007\/3-540-58140-5_30"},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB27","unstructured":"J. Terlouw. Een nadere bewijstheoretische analyse van GSTT's. Technical report, Department of Computer Science, University of Nijmegen, 1989."},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB28","unstructured":"A.N. Whitehead and B. Russell. Principia Mathematica, volume I, II, III. Cambridge University Press, 1910, 1912, 19131, 1925, 1925, 19272."},{"key":"10.1016\/S1571-0661(04)80756-4_NEWBIB29","unstructured":"J. Zucker. Formalization of classical mathematics in Automath. In Colloque International de Logique, Clermont-Ferrand, pages 135\u2013145, Paris, CNRS, 1977. Colloques Internationaux du Centre National de la Recherche Scientifique, 249."}],"container-title":["Electronic Notes in Theoretical Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104807564?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S1571066104807564?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2020,4,3]],"date-time":"2020-04-03T07:14:32Z","timestamp":1585898072000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S1571066104807564"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,9]]},"references-count":29,"journal-issue":{"issue":"7","published-print":{"date-parts":[[2003,9]]}},"alternative-id":["S1571066104807564"],"URL":"https:\/\/doi.org\/10.1016\/s1571-0661(04)80756-4","relation":{},"ISSN":["1571-0661"],"issn-type":[{"value":"1571-0661","type":"print"}],"subject":[],"published":{"date-parts":[[2003,9]]}}}