{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T15:30:32Z","timestamp":1743089432330,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540417392"},{"type":"electronic","value":"9783540447160"}],"license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44716-4_24","type":"book-chapter","created":{"date-parts":[[2007,8,15]],"date-time":"2007-08-15T18:16:34Z","timestamp":1187201794000},"page":"375-389","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Refining the Barendregt Cube using Parameters"],"prefix":"10.1007","author":[{"given":"Fairouz","family":"Kamareddine","sequence":"first","affiliation":[]},{"given":"Twan","family":"Laan","sequence":"additional","affiliation":[]},{"given":"Rob","family":"Nederpelt","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,21]]},"reference":[{"key":"24_CR1","unstructured":"S. Abramsky, Dov M. Gabbay, and T.S.E. Maibaum, editors. Handbook of Logic in Computer Science, Volume 2: Background: Computational Structures. Oxford University Press, 1992."},{"key":"24_CR2","unstructured":"H.P. Barendregt. The Lambda Calculus: its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics 103. North-Holland, Amsterdam, revised edition, 1984."},{"key":"24_CR3","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1017\/S0956796800020025","volume":"1","author":"H.P. Barendregt","year":"1991","unstructured":"H.P. Barendregt. Introduction to generalised type systems. Functional Programming, 1:125\u2013154, 1991.","journal-title":"Functional Programming"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"H.P. Barendregt. Lambda calculi with types. In [1], pages 117\u2013309. Oxford University Press, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"issue":"2","key":"24_CR5","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. P. Nederpelt. The Barendregt Cube with Definitions and Generalised Reduction. Information and Computation, 126 (2):123\u2013143, 1996.","journal-title":"Information and Computation"},{"key":"24_CR6","series-title":"Lecture Notes in Mathematics","first-page":"29","volume-title":"Symposium on Automatic Demonstration","author":"N.G. de Bruijn","year":"1968","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 [18], pages 73-100."},{"key":"24_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":"24_CR8","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"24_CR9","unstructured":"J.H. Geuvers. Logics and Type Systems. PhD thesis, Catholic University of Nijmegen, 1993."},{"key":"24_CR10","unstructured":"J.-Y. Girard. Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dansl\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII, 1972."},{"key":"24_CR11","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A framework for defining logics. In Proceedings Second Symposium on Logic in Computer Science, pages 194\u2013204, Washington D.C., 1987. IEEE."},{"key":"24_CR12","unstructured":"J.R. Hindley and J.P. Seldin. Introduction to Combinators and \u03bb-calculus, volume 1 of London Mathematical Society Student Texts. Cambridge University Press, 1986."},{"key":"24_CR13","unstructured":"W.A. Howard. The formulas-as-types notion of construction. In [21], pages 479\u2013490, 1980."},{"key":"24_CR14","unstructured":"T. Laan. The Evolution of Type Theory in Logic and Mathematics. PhD thesis, Eindhoven University of Technology, 1997."},{"key":"24_CR15","unstructured":"Twan Laan and Michael Franssen. Parameters for first order logic. Logic and Computation, 2001."},{"key":"24_CR16","series-title":"Technical Report CMU-CS-88-131","volume-title":"Constructive natural deduction and its modest interpretation","author":"G. Longo","year":"1988","unstructured":"G. Longo and E. Moggi. Constructive natural deduction and its modest interpretation. Technical Report CMU-CS-88-131, Carnegie Mellono University, Pittsburgh, USA, 1988."},{"key":"24_CR17","volume-title":"Definition of Standard ML","author":"R. Milner","year":"1990","unstructured":"R. Milner, M. Tofte, and R. Harper. Definition of Standard ML. MIT Press, Cambridge (Massachusetts)\/London, 1990."},{"key":"24_CR18","unstructured":"R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer, editors. Selected Papers on Automath. Studies in Logic and the Foundations of Mathematics 133. North-Holland, Amsterdam, 1994."},{"key":"24_CR19","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1016\/0890-5401(92)90028-E","volume":"99","author":"G.R. R. de Lavalette","year":"1991","unstructured":"G.R. Renardel de Lavalette. Strictness analysis via abstract interpretation for recursively defined types. Information and Computation, 99:154\u2013177, 1991.","journal-title":"Information and Computation"},{"key":"24_CR20","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"408","DOI":"10.1007\/3-540-06859-7_148","volume-title":"Towards a theory of type structure","author":"J.C. Reynolds","year":"1974","unstructured":".J.C. Reynolds. Towards a theory of type structure, volume 19 of Lecture Notes in Computer Science, pages 408\u2013425. Springer, 1974."},{"volume-title":"To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","year":"1980","key":"24_CR21","unstructured":"J.P. Seldin and J.R. Hindley, editors. To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, New York, 1980."},{"key":"24_CR22","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"316","DOI":"10.1007\/3-540-58140-5_30","volume-title":"Proceedings of LFCS\u201994","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."}],"container-title":["Lecture Notes in Computer Science","Functional and Logic Programming"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44716-4_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,17]],"date-time":"2024-02-17T11:50:26Z","timestamp":1708170626000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44716-4_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540417392","9783540447160"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-44716-4_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2001]]},"assertion":[{"value":"21 March 2001","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}