{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:05Z","timestamp":1780994705804,"version":"3.54.1"},"reference-count":28,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100004359","name":"Vetenskapsr\u00e5det","doi-asserted-by":"publisher","award":["621-2014-4864"],"award-info":[{"award-number":["621-2014-4864"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000921","name":"European Cooperation in Science and Technology","doi-asserted-by":"publisher","award":["CA15123"],"award-info":[{"award-number":["CA15123"]}],"id":[{"id":"10.13039\/501100000921","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":[[2018,1]]},"abstract":"<jats:p>Type theory should be able to handle its own meta-theory, both to justify its foundational claims and to obtain a verified implementation. At the core of a type checker for intensional type theory lies an algorithm to check equality of types, or in other words, to check whether two types are convertible. We have formalized in Agda a practical conversion checking algorithm for a dependent type theory with one universe \u00e0 la Russell, natural numbers, and \u03b7-equality for \u03a0 types. We prove the algorithm correct via a Kripke logical relation parameterized by a suitable notion of equivalence of terms. We then instantiate the parameterized fundamental lemma twice: once to obtain canonicity and injectivity of type formers, and once again to prove the completeness of the algorithm. Our proof relies on inductive-recursive definitions, but not on the uniqueness of identity proofs. Thus, it is valid in variants of intensional Martin-L\u00f6f Type Theory as long as they support induction-recursion, for instance, Extensional, Observational, or Homotopy Type Theory.<\/jats:p>","DOI":"10.1145\/3158111","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":49,"title":["Decidability of conversion for type theory in type theory"],"prefix":"10.1145","volume":"2","author":[{"given":"Andreas","family":"Abel","sequence":"first","affiliation":[{"name":"University of Gothenburg, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Joakim","family":"\u00d6hman","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrea","family":"Vezzosi","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.33"},{"key":"e_1_2_2_2_1","volume-title":"On Decidability of Conversion in Type Theory. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016","author":"Abel Andreas","year":"2016","unstructured":"Andreas Abel , Thierry Coquand , and Bassel Mannaa . 2016 . On Decidability of Conversion in Type Theory. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016 , Novi Sad, Serbia , May 23-26, 2016, Book of Abstracts, Silvia Ghilezan and Jelena Ivetic (Eds.). EasyChair. Andreas Abel, Thierry Coquand, and Bassel Mannaa. 2016. On Decidability of Conversion in Type Theory. In 22nd International Conference on Types for Proofs and Programs, TYPES 2016, Novi Sad, Serbia, May 23-26, 2016, Book of Abstracts, Silvia Ghilezan and Jelena Ivetic (Eds.). EasyChair."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796816000022"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(1:29)2012"},{"key":"e_1_2_2_5_1","unstructured":"AgdaTeam. 2017. The Agda Wiki. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php  AgdaTeam. 2017. The Agda Wiki. http:\/\/wiki.portal.chalmers.se\/agda\/pmwiki.php"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-13(4:1)2017"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/1695"},{"key":"e_1_2_2_9_1","volume-title":"An Algorithm for Testing Conversion in Type Theory","author":"Coquand Thierry","year":"2047","unstructured":"Thierry Coquand . 1991. An Algorithm for Testing Conversion in Type Theory . In Logical Frameworks, G\u00e9rard Huet and Gordon Plotkin (Eds.). Cambridge University Press , 255\u2013279. http:\/\/dl.acm.org\/citation.cfm?id=1 2047 7.120486 Thierry Coquand. 1991. An Algorithm for Testing Conversion in Type Theory. In Logical Frameworks, G\u00e9rard Huet and Gordon Plotkin (Eds.). Cambridge University Press, 255\u2013279. http:\/\/dl.acm.org\/citation.cfm?id=120477.120486"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(88)90005-3"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/1385-7258(72)90034-0"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45504-3_7"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(02)00096-9"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0064870"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7_2"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-11(1:13)2015"},{"key":"e_1_2_2_19_1","unstructured":"Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de Doctorat d\u2019\u00c9tat. Universit\u00e9 de Paris VII.  Jean-Yves Girard. 1972. Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures dans l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de Doctorat d\u2019\u00c9tat. Universit\u00e9 de Paris VII."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45842-5_8"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.240882"},{"key":"e_1_2_2_24_1","unstructured":"INRIA. 2017. The Coq Proof Assistant Reference Manual (version 8.7 ed.). INRIA. http:\/\/coq.inria.fr\/  INRIA. 2017. The Coq Proof Assistant Reference Manual (version 8.7 ed.). INRIA. http:\/\/coq.inria.fr\/"},{"key":"e_1_2_2_25_1","volume-title":"Logic Colloquium \u201873","author":"Martin-L\u00f6f Per","unstructured":"Per Martin-L\u00f6f . 1975. An Intuitionistic Theory of Types: Predicative Part . In Logic Colloquium \u201873 , H. E. Rose and J. C. Shepherdson (Eds.). North-Holland , 73\u2013118. Per Martin-L\u00f6f. 1975. An Intuitionistic Theory of Types: Predicative Part. In Logic Colloquium \u201873, H. E. Rose and J. C. Shepherdson (Eds.). North-Holland, 73\u2013118."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2013.29"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.44"},{"key":"e_1_2_2_28_1","volume-title":"Investigations into Intensional Type Theory. Habilitation thesis","author":"Streicher Thomas","unstructured":"Thomas Streicher . 1993. Investigations into Intensional Type Theory. Habilitation thesis , Ludwig-Maximilians-University Munich . Thomas Streicher. 1993. Investigations into Intensional Type Theory. Habilitation thesis, Ludwig-Maximilians-University Munich."},{"key":"e_1_2_2_29_1","volume-title":"Proceedings of the 1992 Workshop on Types for Proofs and Programs","author":"Werner Benjamin","year":"1992","unstructured":"Benjamin Werner . 1992 . A Normalization Proof for an Impredicative Type System with Large Eliminations over Integers . In Proceedings of the 1992 Workshop on Types for Proofs and Programs , B\u00e5stad, Sweden , June 1992, Bengt Nordstr\u00f6m, Kent Petersson, and Gordon Plotkin (Eds.). 341\u2013357. http:\/\/www.cs.chalmers.se\/Cs\/Research\/Logic\/Types\/proc92.ps Benjamin Werner. 1992. A Normalization Proof for an Impredicative Type System with Large Eliminations over Integers. In Proceedings of the 1992 Workshop on Types for Proofs and Programs, B\u00e5stad, Sweden, June 1992, Bengt Nordstr\u00f6m, Kent Petersson, and Gordon Plotkin (Eds.). 341\u2013357. http:\/\/www.cs.chalmers.se\/Cs\/Research\/Logic\/Types\/proc92.ps"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158111","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158111","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158111"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":28,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158111"],"URL":"https:\/\/doi.org\/10.1145\/3158111","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}