{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T01:02:00Z","timestamp":1767920520335,"version":"3.49.0"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","funder":[{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2327738"],"award-info":[{"award-number":["2327738"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2026,1,8]]},"abstract":"<jats:p>In a dependent type theory with \u03b2-equivalence as its equational theory, the confluence of untyped reduction and termination immediately give us a proof of the decidability of type conversion, where the decision procedure for convertibility simply checks the equality of the \u03b2-normal forms of its inputs. This technique is not available in the presence of surjective pairing (i.e. the \u03b7-law for pairs) because \u03b2\u03b7-reduction is not confluent. In this work, we show that by adopting established syntactic techniques, we can resolve the issue with confluence caused by surjective pairing, and recover a confluence-based proof of decidability of type conversion. Compared to existing proof developments, which rely on semantic tools such as Kripke-style logical relations, our proof modularly composes a minimal semantic proof of untyped normalization and a syntactic proof of decidability. This modularity enables us to explore algorithmic conversion through syntactic methods without modifying the minimal semantic proof. We have fully mechanized our results using the Rocq theorem prover.<\/jats:p>","DOI":"10.1145\/3776672","type":"journal-article","created":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T18:59:43Z","timestamp":1767898783000},"page":"865-894","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach"],"prefix":"10.1145","volume":"10","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-8717-2498","authenticated-orcid":false,"given":"Yiyun","family":"Liu","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6756-9168","authenticated-orcid":false,"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]}],"member":"320","published-online":{"date-parts":[[2026,1,8]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"Andreas Abel. 2013. Normalization by evaluation: Dependent types and impredicativity. Ph. D. Dissertation. Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796819000170"},{"key":"e_1_2_1_3_1","first-page":"345","article-title":"Untyped algorithmic equality for Martin-L\u00f6f\u2019s logical framework with surjective pairs","volume":"77","author":"Abel Andreas","year":"2007","unstructured":"Andreas Abel and Thierry Coquand. 2007. Untyped algorithmic equality for Martin-L\u00f6f\u2019s logical framework with surjective pairs. Fundamenta Informaticae, 77, 4 (2007), 345\u2013395.","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70594-9_4"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.2168\/lmcs-8(1:29)2012"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005770"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636951"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/645891.671415"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_16"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.FSCD.2016.6"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796800020025"},{"key":"e_1_2_1_13_1","volume-title":"Lambda Calculi with Types","author":"Barendregt Henk P.","year":"1985","unstructured":"Henk P. Barendregt. 1993. Lambda Calculi with Types. Oxford University Press, Inc., USA. 117\u2013309. isbn:0198537611"},{"key":"e_1_2_1_14_1","unstructured":"Bruno Barras. 1996. Coq en coq. Ph. D. Dissertation. INRIA."},{"key":"e_1_2_1_15_1","unstructured":"Bruno Barras. 2012. Semantical investigations in intuitionistic set theory and type theories with inductive families. Th\u00e8se l\u2019habilitation \u00e0 diriger des recherches Universit\u00e9 Paris 7 - Denis Diderot."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_26"},{"key":"e_1_2_1_17_1","doi-asserted-by":"crossref","unstructured":"Ulrich Berger Matthias Eberl and Helmut Schwichtenberg. 1998. Normalization by evaluation. Prospects for Hardware Foundations: ESPRIT Working Group 8533 NADA\u2014New Hardware Design Methods Survey Chapters 117\u2013137.","DOI":"10.1007\/3-540-49254-2_4"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129505004822"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_15"},{"key":"e_1_2_1_20_1","volume-title":"An algorithm for testing conversion in type theory. Logical frameworks, 1","author":"Coquand Thierry","year":"1991","unstructured":"Thierry Coquand. 1991. An algorithm for testing conversion in type theory. Logical frameworks, 1 (1991), 255\u2013279."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2019.01.015"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-018-9879-9"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_2_1_24_1","volume-title":"Generating Infrastructural Code for Terms with Binders using MetaCoq and OCaml. Bachelor thesis","author":"Dapprich Adrian","unstructured":"Adrian Dapprich and Andrej Dudenhefner. 2021. Generating Infrastructural Code for Terms with Binders using MetaCoq and OCaml. Bachelor thesis, Saarland University."},{"key":"e_1_2_1_25_1","doi-asserted-by":"crossref","unstructured":"Roberto Di Cosmo and Delia Kesner. 1994. Combining first order algebraic rewriting systems recursion and extensional lambda calculi. In International Colloquium on Automata Languages and Programming. 462\u2013472.","DOI":"10.1007\/3-540-58201-0_90"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7_2"},{"key":"e_1_2_1_27_1","unstructured":"Jan Herman Geuvers. 1993. Logics and type systems. [Sl: sn]."},{"key":"e_1_2_1_28_1","volume-title":"Proofs and types. 7","author":"Girard Jean-Yves","unstructured":"Jean-Yves Girard, Paul Taylor, and Yves Lafont. 1989. Proofs and types. 7, Cambridge University Press, Cambridge."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_26"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581501"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","unstructured":"Martin Hofmann and Martin Hofmann. 1997. Syntax and semantics of dependent types. Extensional Constructs in Intensional Type Theory 13\u201354.","DOI":"10.1007\/978-1-4471-0963-1_2"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796823000060"},{"key":"e_1_2_1_34_1","volume-title":"Antoine Gaulin, and Brigitte Pientka.","author":"Jang Junyoung","year":"2025","unstructured":"Junyoung Jang, Jason ZS Hu, Antoine Gaulin, and Brigitte Pientka. 2025. McTT: Building A Correct-By-Construction Proof Checker For Martin-L\u00f6f Type Theory."},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1017\/S0956796800001301","article-title":"The virtues of eta-expansion","volume":"5","author":"Barry Jay C","year":"1995","unstructured":"C Barry Jay and Neil Ghani. 1995. The virtues of eta-expansion. Journal of functional programming, 5, 2 (1995), 135\u2013154.","journal-title":"Journal of functional programming"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-002-0156-9"},{"key":"e_1_2_1_37_1","volume-title":"Combinatory Reduction Systems. Mathematisch centrum","author":"Klop Jan Willem","unstructured":"Jan Willem Klop. 1980. Combinatory Reduction Systems. Mathematisch centrum, Amsterdam."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90014-X"},{"key":"e_1_2_1_39_1","first-page":"175","volume-title":"Eta-Equivalence in Core Dependent Haskell. Leibniz international proceedings in informatics","author":"Kravchuk-Kirilyuk Anastasiya","year":"2020","unstructured":"Anastasiya Kravchuk-Kirilyuk, Antoine Voizard, and Stephanie Weirich. 2020. Eta-Equivalence in Core Dependent Haskell. Leibniz international proceedings in informatics, 175 (2020)."},{"key":"e_1_2_1_40_1","volume-title":"Workshop on the Implementation of Type Systems (WITS). https:\/\/www. meven. ac\/documents\/22-WITS-abstract. pdf.","author":"Lennon-Bertrand Meven","year":"2022","unstructured":"Meven Lennon-Bertrand. 2022. \u00c0 bas l\u2019\u03b7 \u2014Coq\u2019s troublesome \u03b7 -conversion. The first Workshop on the Implementation of Type Systems (WITS). https:\/\/www. meven. ac\/documents\/22-WITS-abstract. pdf."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2025.27"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632886"},{"key":"e_1_2_1_43_1","volume-title":"Functional Pearl: Short and Mechanized Logical Relation for Dependent Type Theories.","author":"Liu Yiyun","year":"2024","unstructured":"Yiyun Liu, Jonathan Chan, and Stephanie Weirich. 2024. Functional Pearl: Short and Mechanized Logical Relation for Dependent Type Theories."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704843"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","unstructured":"Yiyun Liu and Stephanie Weirich. 2025. Artifact associated with \"Algorithmic Conversion with Surjective Pairing: A Syntactic and Untyped Approach\". https:\/\/doi.org\/10.5281\/zenodo.17343517 10.5281\/zenodo.17343517","DOI":"10.5281\/zenodo.17343517"},{"key":"e_1_2_1_46_1","volume-title":"An extended calculus of constructions. Ph. D. Dissertation","author":"Luo Zhaohui","unstructured":"Zhaohui Luo. 1990. An extended calculus of constructions. Ph. D. Dissertation. University of Edinburgh."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_27"},{"key":"e_1_2_1_48_1","volume-title":"Types for Proofs and Programs","author":"Miquel Alexandre","unstructured":"Alexandre Miquel and Benjamin Werner. 2003. The Not So Simple Proof-Irrelevant Model of CC. In Types for Proofs and Programs, Herman Geuvers and Freek Wiedijk (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 240\u2013258. isbn:978-3-540-39185-2"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796812000044"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3706056"},{"key":"e_1_2_1_51_1","volume-title":"2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201315","author":"Sterling Jonathan","year":"2021","unstructured":"Jonathan Sterling and Carlo Angiuli. 2021. Normalization for cubical type theory. In 2021 36th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201315."},{"key":"e_1_2_1_52_1","volume-title":"Extending the extensional lambda calculus with surjective pairing is conservative. Logical Methods in Computer Science, 2","author":"St\u00f8vring Kristian","year":"2006","unstructured":"Kristian St\u00f8vring. 2006. Extending the extensional lambda calculus with surjective pairing is conservative. Logical Methods in Computer Science, 2 (2006)."},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1057"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","unstructured":"The Rocq Development Team. 2025. The Rocq Prover. https:\/\/doi.org\/10.5281\/zenodo.15149629 10.5281\/zenodo.15149629","DOI":"10.5281\/zenodo.15149629"},{"key":"e_1_2_1_55_1","volume-title":"Belgium","author":"Timany Amin","unstructured":"Amin Timany and Matthieu Sozeau. 2017. Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC). KU Leuven, Belgium ; Inria Paris, 30. https:\/\/inria.hal.science\/hal-01615123"},{"key":"e_1_2_1_56_1","unstructured":"Femke Van Raamsdonk and PG Severi. 1995. On normalisation."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110275"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/3167091"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3776672","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,8]],"date-time":"2026-01-08T19:03:15Z","timestamp":1767898995000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3776672"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,1,8]]},"references-count":58,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2026,1,8]]}},"alternative-id":["10.1145\/3776672"],"URL":"https:\/\/doi.org\/10.1145\/3776672","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026,1,8]]},"assertion":[{"value":"2025-07-10","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-11-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2026-01-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}