{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:54Z","timestamp":1761597054643},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540418641"},{"type":"electronic","value":"9783540453154"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-45315-6_11","type":"book-chapter","created":{"date-parts":[[2007,12,3]],"date-time":"2007-12-03T06:28:39Z","timestamp":1196663319000},"page":"168-183","source":"Crossref","is-referenced-by-count":19,"title":["The Rho Cube"],"prefix":"10.1007","author":[{"given":"Horatiu","family":"Cirstea","sequence":"first","affiliation":[]},{"given":"Claude","family":"Kirchner","sequence":"additional","affiliation":[]},{"given":"Luigi","family":"Liquori","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,3,23]]},"reference":[{"key":"11_CR1","unstructured":"H. Barendregt. Lambda Calculus: its Syntax and Semantics. North Holland, 1984."},{"key":"11_CR2","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1093\/oso\/9780198537618.003.0002","volume":"II","author":"H. Barendregt","year":"1992","unstructured":"H. Barendregt. Lambda Calculi with Types. In Handbook of Logic in Computer Science, volume II, pages 118\u2013310. Oxford University Press, 1992.","journal-title":"Handbook of Logic in Computer Science"},{"key":"11_CR3","unstructured":"S. Berardi. Towards a Mathematical Analysis of Type Dependence in Coquand-Huet Calculus of Constructions and the Other Systems in Barendregt\u2019s Cube. Technical report, Dept. of Computer Science, Carnegie Mellon University, and Dip. di Matematica, Universit\u00e0 di Torino, 1988."},{"key":"11_CR4","unstructured":"S. Berardi. Type Dependence and Constructive Cathematics. PhD thesis, Dipartimento di Matematica, Universit\u00e0 di Torino, 1990."},{"issue":"5","key":"11_CR5","doi-asserted-by":"publisher","first-page":"523","DOI":"10.1016\/S0747-7171(89)80057-4","volume":"8","author":"H.-J. B\u00fcrckert","year":"1989","unstructured":"H.-J. B\u00fcrckert. Matching-A Special Case of Unification? Journal of Symbolic Computation, 8(5):523\u2013536, 1989.","journal-title":"Journal of Symbolic Computation"},{"issue":"2\/3","key":"11_CR6","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(2\/3):95\u2013120, 1988.","journal-title":"Information and Computation"},{"key":"11_CR7","doi-asserted-by":"crossref","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A. Church","year":"1941","unstructured":"A. Church. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, 5:56\u201368, 1941.","journal-title":"Journal of Symbolic Logic"},{"key":"11_CR8","unstructured":"H. Cirstea. Calcul de R\u00e9\u00e9criture: Fondements et Applications. Th\u00e8se de Doctorat d\u2019Universit\u00e9, Universit\u00e9 Henri Poincar\u00e9-Nancy I, 2000."},{"key":"11_CR9","unstructured":"H. Cirstea and C. Kirchner. An Introduction to the Rewriting Calculus. Research Report RR-3818, INRIA, 1999."},{"key":"11_CR10","unstructured":"H. Cirstea and C. Kirchner. Combining Higher-Order and First-Order Computation Using \u03c1-calculus: Towards a Semantics of ELAN. In Frontiers of Combining Systems 2, pages 95\u2013120. Wiley, 1999."},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"H. Cirstea and C. Kirchner. The Typed Rewriting Calculus. In Third International Workshop on Rewriting Logic and Application, 2000.","DOI":"10.1016\/S1571-0661(05)80127-6"},{"key":"11_CR12","unstructured":"H. Cirstea, C. Kirchner, and L. Liquori. Matching Power. Research Report A00-RR-363, LORIA, 2000. Submitted."},{"key":"11_CR13","unstructured":"T. Coquand. Metamathematical Investigations of a Calculus of Constructions. In Logic and Computer Science, pages 91\u2013122. Academic Press, 1991."},{"key":"11_CR14","unstructured":"N. G. de Bruijn. A Survey of the Project AUTOMATH. In J. P. Seldin and J. R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 589\u2013606. Academic Press, 1980."},{"key":"11_CR15","unstructured":"J.Y. Girard. Interpretation Fonctionnelle et-Elimination des Coupures dans l\u2019Arithm\u00e9tique d\u2019Ordre Sup\u00e9rieur. PhD thesis, Universit\u00e9 Paris VII, 1972."},{"key":"11_CR16","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1016\/0304-3975(86)90044-7","volume":"45","author":"J.Y. Girard","year":"1986","unstructured":"J.Y. Girard. The System F of Variable Types, Fifteen Years Later. Theoretical Computer Science, 45:159\u2013192, 1986.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"11_CR17","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1017\/S0956796800020037","volume":"1","author":"H. Geuvers","year":"1991","unstructured":"H. Geuvers and M.J. Nederhof. A Modular Proof of Strong Normalization for the Calculus of Constructions. Journal of Functional Programming, 1(2):155\u2013189, 1991.","journal-title":"Journal of Functional Programming"},{"issue":"1","key":"11_CR18","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1992","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A Framework for Defining Logics. Journal of the ACM, 40(1):143\u2013184, 1992.","journal-title":"Journal of the ACM"},{"key":"11_CR19","unstructured":"J.-M. Hullot. Associative-Commutative Pattern Matching. In Proc. of IJCAI, 1979."},{"key":"11_CR20","unstructured":"J.-P. Jouannaud and C. Kirchner. Solving Equations in Abstract Algebras: A Rule-based Survey of Unification. In Computational Logic. Essays in Honor of Alan Robinson, chapter 8, pages 257\u2013321. The MIT press, 1991."},{"issue":"1-3","key":"11_CR21","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/S0168-0072(98)00019-0","volume":"97","author":"F. Kamareddine","year":"1999","unstructured":"F. Kamareddine, R. Bloo, and R. Nederpelt. On \u03c0-conversion on the \u03bb-cube and the Combination with Abbreviations. Annals of Pure and Applied Logics, 97(1-3):27\u201345, 1999.","journal-title":"Annals of Pure and Applied Logics"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"C. Kirchner and H. Kirchner. Rewriting, Solving, Proving. A preliminary version of a book available at http:\/\/www.loria.fr\/~ckirchne\/rsp.ps.gz , 1999.","DOI":"10.1007\/978-3-642-59851-7_9"},{"key":"11_CR23","doi-asserted-by":"crossref","unstructured":"F. Kamareddine and T. Laan. A Correspondence between Martin-L\u00f6f Type Theory, the Ramified Theory of Types and Pure Type Systems. Journal of Logic, Language and Information, 2001. To appear.","DOI":"10.1023\/A:1011286100450"},{"issue":"2","key":"11_CR24","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1017\/S0956796800001672","volume":"6","author":"F. Kamareddine","year":"1996","unstructured":"F. Kamareddine and R. Nederpelt. Canonical Typing and \u03c0-conversion in the \u03bb-cube. Journal of Functional Programming, 6(2):85\u2013109, 1996.","journal-title":"Journal of Functional Programming"},{"key":"11_CR25","unstructured":"Z. Luo. ECC: An Extended Calculus of Constructions. In Proceedings of LICS, pages 385\u2013395, 1990."},{"key":"11_CR26","unstructured":"P. Martin-L\u00f6f. Intuitionistic Type Theory, volume 1 of Studies in Proof Theory. Bibliopolis, Naples, 1984."},{"key":"11_CR27","unstructured":"S.L. Peyton Jones and E. Meijer. Henk: a Typed Intermediate Language. In Types in Compilation Workshop, 1997."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45315-6_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,20]],"date-time":"2024-02-20T00:00:17Z","timestamp":1708387217000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45315-6_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540418641","9783540453154"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/3-540-45315-6_11","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}