{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:05Z","timestamp":1753889765736,"version":"3.41.2"},"reference-count":23,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2006,3,16]],"date-time":"2006-03-16T00:00:00Z","timestamp":1142467200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We answer Klop and de Vrijer's question whether adding surjective-pairing axioms to the extensional lambda calculus yields a conservative extension. The answer is positive. As a byproduct we obtain a \"syntactic\" proof that the extensional lambda calculus with surjective pairing is consistent.<\/jats:p>","DOI":"10.2168\/lmcs-2(2:1)2006","type":"journal-article","created":{"date-parts":[[2006,11,23]],"date-time":"2006-11-23T09:26:57Z","timestamp":1164274017000},"source":"Crossref","is-referenced-by-count":4,"title":["Extending the Extensional Lambda Calculus with Surjective Pairing is Conservative"],"prefix":"10.46298","volume":"Volume 2, Issue 2","author":[{"given":"Kristian","family":"Stoevring","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2006,3,16]]},"reference":[{"key":"10.2168\/LMCS-2(2:1)2006_Barendregt:ZMLGM1974","doi-asserted-by":"crossref","first-page":"289","DOI":"10.1002\/malq.19740201902","volume":"20","author":"Henk Barendregt","year":"1974","journal-title":"Z. Math. Logik Grundlag. Math."},{"key":"10.2168\/LMCS-2(2:1)2006_Barendregt:84","unstructured":"Henk Barendregt.The Lambda Calculus: Its Syntax and Semantics, volume 103 ofStudies in Logic and the Foundation of Mathematics. North-Holland, revised edition, 1984."},{"key":"10.2168\/LMCS-2(2:1)2006_Barendregt:92-foo","doi-asserted-by":"crossref","unstructured":"Henk Barendregt. Lambda calculi with types. In Samson Abramsky, Dov M. Gabbay, and Thomas S. E. Maibaum, editors,Handbook of Logic in Computer Science, Vol. 2, chapter 2, pages 118-309. Oxford University Press, Oxford, 1992.","DOI":"10.1093\/oso\/9780198537618.003.0002"},{"key":"10.2168\/LMCS-2(2:1)2006_Curien-DiCosmo:JFP1996","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001696"},{"key":"10.2168\/LMCS-2(2:1)2006_Curien-Hardin:JFP1994","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000976"},{"key":"10.2168\/LMCS-2(2:1)2006_Dershowitz-al:RTA1991","doi-asserted-by":"crossref","unstructured":"Nachum Dershowitz, Jean-Pierre Jouannaud, and Jan Willem Klop. Open problems in rewriting. In Ronald V. Book, editor,Rewriting Techniques and Applications, 4th International Conference, RTA-91, volume 488 ofLecture Notes in Computer Science, pages 445-456. Springer-Verlag, 1991. The RTA list of open problems is currently maintained at \\texttthttp:\/\/www.lsv.ens-cachan.fr\/rtaloop\/.","DOI":"10.1007\/3-540-53904-2_120"},{"key":"10.2168\/LMCS-2(2:1)2006_Durfee:MSc","doi-asserted-by":"crossref","unstructured":"Glenn Durfee. A model for a list-oriented extension of the lambda calculus. Master's thesis, School of Computer Science, Carnegie Mellon University, 1997.","DOI":"10.21236\/ADA327564"},{"key":"10.2168\/LMCS-2(2:1)2006_Jay-Ghani:JFP95","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800001301"},{"key":"10.2168\/LMCS-2(2:1)2006_Klop:PhD-foo","unstructured":"Jan Willem Klop.Combinatory Reduction Systems. Mathematical Centre Tracts 127. Mathematisch Centrum, Amsterdam, 1980."},{"key":"10.2168\/LMCS-2(2:1)2006_Klop-de-Vrijer:IAC1989","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90014-X"},{"key":"10.2168\/LMCS-2(2:1)2006_Lambek-Scott:86","unstructured":"Joachim Lambek and Philip J. Scott.Introduction to Higher Order Categorical Logic, volume 7 ofCambridge studies in advanced mathematics. Cambridge University Press, 1986."},{"key":"10.2168\/LMCS-2(2:1)2006_Lassen:LICS2006","unstructured":"Soren B. Lassen. Head normal form bisimulation for pairs and the\u03bb\u03bc-calculus. Manuscript, 2006."},{"key":"10.2168\/LMCS-2(2:1)2006_Nipkow:TLCA1993","doi-asserted-by":"crossref","unstructured":"Tobias Nipkow. Orthogonal higher-order rewrite systems are confluent. In Marc Bezem and Jan Friso Groote, editors,Typed Lambda Calculi and Applications, TLCA '93, volume 664 ofLecture Notes in Computer Science, pages 306-317. Springer-Verlag, 1993.","DOI":"10.1007\/BFb0037114"},{"issue":"1","key":"10.2168\/LMCS-2(2:1)2006_van-Oostrom:TCS1997","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1016\/S0304-3975(96)00173-9","volume":"175","author":"Vincent \\SortNoop{Oostrom}van Oostr","year":"1997","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-2(2:1)2006_Pfenning:CR","doi-asserted-by":"crossref","unstructured":"Frank Pfenning. A proof of the Church-Rosser theorem and its representation in a logical framework. Technical Report CMU-CS-92-186, School of Computer Science, Carnegie Mellon University, 1992.","DOI":"10.21236\/ADA256574"},{"key":"10.2168\/LMCS-2(2:1)2006_Pfenning-Schuermann:CADE1999","doi-asserted-by":"crossref","unstructured":"Frank Pfenning and Carsten Sch\u00fcrmann. System description: Twelf - a meta-logical framework for deductive systems. In Harald Ganzinger, editor,Automated Deduction--CADE-16, 16th International Conference on Automated Deduction, volume 1632 ofLecture Notes in Computer Science, pages 202-206. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48660-7_14"},{"key":"10.2168\/LMCS-2(2:1)2006_vanRaamsdonk:PhD","unstructured":"Femke \\SortNoop{Raamsdonk}van Raamsdonk.Confluence and Normalization for higher-order rewriting. PhD thesis, Vrije Universiteit Amsterdam, 1996."},{"key":"10.2168\/LMCS-2(2:1)2006_Revesz:TCS1993","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90212-X"},{"key":"10.2168\/LMCS-2(2:1)2006_Revesz:FI1995","doi-asserted-by":"crossref","first-page":"153","DOI":"10.3233\/FI-1995-22127","volume":"22","author":"Gy\u00f6rgy E. R\u00e9v\u00e9sz","year":"1995","journal-title":"Fundamenta Informaticae"},{"key":"10.2168\/LMCS-2(2:1)2006_Scott:CACM77-2","doi-asserted-by":"publisher","DOI":"10.1145\/359810.359826"},{"key":"10.2168\/LMCS-2(2:1)2006_Scott:Curry1980","unstructured":"Dana S. Scott. Relating theories of the lambda calculus. In J. P. Seldin and J. R. Hindley, editors,To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism, pages 403-450. Academic Press, 1980."},{"key":"10.2168\/LMCS-2(2:1)2006_Takahashi:IaC1995","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1057"},{"key":"10.2168\/LMCS-2(2:1)2006_de-Vrijer:LICS1989","unstructured":"Roel \\SortNoop{Vrijer}de Vrijer. Extending the lambda calculus with surjective pairing is conservative. InProceedings of the Fourth Annual IEEESymposium on Logic in Computer Science, pages 204-215, Pacific Grove, California, June 1989. IEEE Computer Society Press."}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/2249\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/2249\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,8]],"date-time":"2024-02-08T12:40:57Z","timestamp":1707396057000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/2249"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,3,16]]},"references-count":23,"URL":"https:\/\/doi.org\/10.2168\/lmcs-2(2:1)2006","relation":{"is-same-as":[{"id-type":"arxiv","id":"math\/0602544","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.math\/0602544","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2006,3,16]]},"article-number":"2249"}}