{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:17:37Z","timestamp":1725484657967},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540434009"},{"type":"electronic","value":"9783540459958"}],"license":[{"start":{"date-parts":[[2002,1,1]],"date-time":"2002-01-01T00:00:00Z","timestamp":1009843200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45995-2_34","type":"book-chapter","created":{"date-parts":[[2007,5,29]],"date-time":"2007-05-29T22:33:34Z","timestamp":1180478014000},"page":"371-385","source":"Crossref","is-referenced-by-count":4,"title":["Parameters in Pure Type Systems"],"prefix":"10.1007","author":[{"given":"Roel","family":"Bloo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fairouz","family":"Kamareddine","sequence":"additional","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":"297","published-online":{"date-parts":[[2002,3,14]]},"reference":[{"key":"34_CR1","unstructured":"H.P. Barendregt. Lambda calculi with types. In [?], pages 117\u2013309. Oxford University Press, 1992."},{"key":"34_CR2","unstructured":"L.S. van Benthem Jutting. Checking Landau\u2019s \u201cGrundlagen\u201d in the Automath system. PhD thesis, Eindhoven University of Technology, 1977. Published as Mathematical Centre Tracts nr. 83 (Amsterdam, Mathematisch Centrum, 1979)."},{"key":"34_CR3","unstructured":"S. Berardi. Towards a mathematical analysis of the Coquand-Huet calculus of constructions and the other systems in Barendregt\u2019s cube. Technical report, Dept. of Computer Science, Carnegie-Mellon University and Dipartimento Matematica, Universita di Torino, 1988."},{"issue":"2","key":"34_CR4","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1006\/inco.1996.0041","volume":"126","author":"R. Bloo","year":"1996","unstructured":"R. Bloo, F. Kamareddine, and R. Nederpelt. The Barendregt Cube with Definitions and Generalised Reduction. Information and Computation, 126(2):123\u2013143, 1996.","journal-title":"Information and Computation"},{"key":"34_CR5","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1023\/A:1008254612284","volume":"7","author":"V.A.J. Borghuis","year":"1998","unstructured":"V.A.J. Borghuis. Modal Pure Type Systems. Journal of Logic, Language, and Information, 7:265\u2013296, 1998.","journal-title":"Journal of Logic, Language, and Information"},{"key":"34_CR6","doi-asserted-by":"crossref","unstructured":"N.G. de Bruijn. Reflections on Automath. Eindhoven University of Technology, 1990. Also in [?], pages 201\u2013228.","DOI":"10.1016\/S0049-237X(08)70205-2"},{"key":"34_CR7","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1940","unstructured":"A. Church. A formulation of the simple theory of types. The Journal of Symbolic Logic, 5:56\u201368, 1940.","journal-title":"The Journal of Symbolic Logic"},{"key":"34_CR8","doi-asserted-by":"crossref","unstructured":"D.T. van Daalen. A description of Automath and some aspects of its language theory. In P. Braffort, editor, Proceedings of the Symposium APLASM, volume I, pages 48\u201377, 1973. Also in [?], pages 101\u2013126.","DOI":"10.1016\/S0049-237X(08)70201-5"},{"key":"34_CR9","unstructured":"J.H. Geuvers, F. Wiedijk, J. Zwanenburg, R. Pollack, and H. Barendregt. Personal communication on the \u201cFundamental Theorem of Algebra\u201d project. FTA web page available at http:\/\/www.cs.kun.nl \/gi\/projects\/fta\/index.html."},{"key":"34_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1007\/3-540-44716-4_24","volume-title":"Refining the Barendregt cube using parameters","author":"F. Kamareddine","year":"2001","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, Lecture Notes in Computer Science:375\u2013389, 2001."},{"key":"34_CR11","unstructured":"T. Laan. The Evolution of Type Theory in Logic and Mathematics. PhD thesis, Eindhoven University of Technology, 1997."},{"key":"34_CR12","unstructured":"T. Laan, R. Bloo, F. Kamareddine, and R. Nederpelt. Parameters in pure type systems. Technical Report 00-18, TUE Computing Science Reports, Eindhoven University of Technology, 2000. Available from http:\/\/www.win.tue.nl \/~bloo\/parameter-report.ps.gz."},{"key":"34_CR13","unstructured":"Twan Laan and Michael Franssen. Parameters for first order logic. Logic and Computation, 2001."},{"key":"34_CR14","unstructured":"Z. Luo. An Extended Calculus of Constructions. PhD thesis, 1990."},{"key":"34_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-58140-5_30","volume-title":"Pure type systems with definitions","author":"P. Severi","year":"1994","unstructured":"P. Severi and E. Poll. Pure type systems with definitions. In A. Nerode and Yu.V. Matiyasevich, editors, Proceedings of LFCS\u201994 (LNCS 813), pages 316\u2013328, New York, 1994. LFCS\u201994, St. Petersburg, Russia, Springer Verlag."},{"key":"34_CR16","unstructured":"J. Terlouw. Een nadere bewijstheoretische analyse van GSTT\u2019s. Technical report, Department of Computer Science, University of Nijmegen, 1989."},{"issue":"2","key":"34_CR17","doi-asserted-by":"publisher","first-page":"339","DOI":"10.2307\/2274219","volume":"50","author":"R. Vrijer de","year":"1985","unstructured":"R. de Vrijer. A direct proof of the finite developments theorem. The Journal of Symbolic Logic, 50(2):339\u2013343, 1985.","journal-title":"The Journal of Symbolic Logic"}],"container-title":["Lecture Notes in Computer Science","LATIN 2002: Theoretical Informatics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45995-2_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T08:30:31Z","timestamp":1556440231000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45995-2_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540434009","9783540459958"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-45995-2_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2002]]}}}