{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T13:45:41Z","timestamp":1753883141912,"version":"3.41.2"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","license":[{"start":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T00:00:00Z","timestamp":1748476800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"abstract":"<jats:p>\n            The internal Church thesis (\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi mathvariant=\"sans-serif\">CT<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            ) is a logical principle stating that one can associate to any function\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mrow>\n                  <mml:mi>f<\/mml:mi>\n                  <mml:mspace width=\"0.2em\"\/>\n                  <mml:mo>:<\/mml:mo>\n                  <mml:mspace width=\"0.2em\"\/>\n                  <mml:mi mathvariant=\"double-struck\">N<\/mml:mi>\n                  <mml:mo>\u2192<\/mml:mo>\n                  <mml:mi mathvariant=\"double-struck\">N<\/mml:mi>\n                <\/mml:mrow>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            a concrete code, in some Turing-complete language, that computes\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi>f<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            . While the compatibility of\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi mathvariant=\"sans-serif\">CT<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            in simpler systems has been long known, its compatibility with dependent type theory is still an open question.\n          <\/jats:p>\n          <jats:p>\n            In this paper, we answer this question positively. We define\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mrow>\n                  <mml:mo mathvariant=\"sans-serif\">\u201c<\/mml:mo>\n                  <mml:mi mathvariant=\"sans-serif\">MLTT<\/mml:mi>\n                  <mml:mo mathvariant=\"sans-serif\">\u201d<\/mml:mo>\n                <\/mml:mrow>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            , a type theory extending\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi mathvariant=\"sans-serif\">MLTT<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            with quote operators in which\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mi mathvariant=\"sans-serif\">CT<\/mml:mi>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            is derivable. We furthermore prove that\n            <jats:inline-formula>\n              <mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\" display=\"inline\">\n                <mml:mrow>\n                  <mml:mo mathvariant=\"sans-serif\">\u201c<\/mml:mo>\n                  <mml:mi mathvariant=\"sans-serif\">MLTT<\/mml:mi>\n                  <mml:mo mathvariant=\"sans-serif\">\u201d<\/mml:mo>\n                <\/mml:mrow>\n              <\/mml:math>\n            <\/jats:inline-formula>\n            is consistent, strongly normalizing and enjoys canonicity using a rather standard logical relation model. All the results in this paper have been mechanized in Coq.\n            <jats:xref ref-type=\"fn\">\n              <jats:sup>a<\/jats:sup>\n            <\/jats:xref>\n          <\/jats:p>","DOI":"10.1145\/3715707","type":"journal-article","created":{"date-parts":[[2025,5,29]],"date-time":"2025-05-29T14:18:02Z","timestamp":1748528282000},"update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["\u2018Upon This Quote I Will Build My Church Thesis\u2019"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-8006-6239","authenticated-orcid":false,"given":"Pierre-Marie","family":"P\u00e9drot","sequence":"first","affiliation":[{"name":"INRIA, Nantes, France"}]}],"member":"320","published-online":{"date-parts":[[2025,5,29]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"e_1_3_1_3_2","volume-title":"Proc. 13th ACM SIGPLAN Intern. Conf. on Certified Programs and Proofs,","author":"Adjedj A.","year":"2024","unstructured":"Adjedj, A. et al. Martin-L\u00f6f \u00e0 la Coq. In Proc. 13th ACM SIGPLAN Intern. Conf. on Certified Programs and Proofs,\u00a0Blazy,\u00a0S.,\u00a0Pientka,\u00a0B.,\u00a0Timany,\u00a0A., and\u00a0Traytel,\u00a0D. ACM, (2024)."},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/3661814.3662104"},{"issue":"3","key":"e_1_3_1_5_2","article-title":"The independence of Markov\u2019s principle in type theory","volume":"13","author":"Coquand T.","year":"2017","unstructured":"Coquand, T. and Mannaa, B. The independence of Markov\u2019s principle in type theory. Log. Methods Comput. Sci.\u00a013, 3, (2017).","journal-title":"Log. Methods Comput. Sci."},{"key":"e_1_3_1_6_2","volume-title":"Computability in Constructive Type Theory","author":"Forster Y.","year":"2021","unstructured":"Forster, Y. Computability in Constructive Type Theory. Ph.D. thesis, Saarland University, Germany, (2021)."},{"key":"e_1_3_1_7_2","volume-title":"A Type Theory with Definitional Proof-Irrelevance","author":"Gilbert G.","year":"2019","unstructured":"Gilbert, G. A Type Theory with Definitional Proof-Irrelevance. Ph.D. thesis, Mines ParisTech, France, (2019)."},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"issue":"3","key":"e_1_3_1_9_2","article-title":"Multimodal dependent type theory","volume":"17","author":"Gratzer D.","year":"2021","unstructured":"Gratzer, D., Kavvos, G. A., Nuyts, A., and Birkedal, L. Multimodal dependent type theory. Log. Methods Comput. Sci.\u00a017, 3 (2021).","journal-title":"Log. Methods Comput. Sci."},{"key":"e_1_3_1_10_2","first-page":"156","volume-title":"Typed Lambda Calculi and Applications","author":"Hancock P.","unstructured":"Hancock, P. et al. Small induction recursion. Typed Lambda Calculi and Applications, Springer, Berlin Heidelberg,\u00a0Hasegawa,\u00a0M.\u00a0(ed)\u00a0156\u2013172."},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(09)70129-6"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-018-0612-9"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3498700"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1943-0007371-8"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.2307\/2269016"},{"key":"e_1_3_1_16_2","unstructured":"Margenstern M. L\u2019\u00e9cole constructive de markov. Revue d\u2019histoire des Math\u00e9matiques (1995)."},{"key":"e_1_3_1_17_2","unstructured":"Martin-L\u00f6f P. Intuitionistic Type Theory Volume 1 of Studies in Proof Theory. Bibliopolis (1984)."},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_3_1_19_2","volume-title":"Program Extraction in the Calculus of Constructions","author":"Paulin-Mohring C.","year":"1989","unstructured":"Paulin-Mohring, C. Program Extraction in the Calculus of Constructions. Ph.D. thesis, Paris Diderot University, France, (1989)."},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394740"},{"key":"e_1_3_1_21_2","first-page":"245","volume-title":"Programming Languages and Systems - 27th European Symp. on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software","author":"P\u00e9drot P.","year":"2018","unstructured":"P\u00e9drot, P. and Tabareau, N. Failure is not an option - An exceptional type theory. In Programming Languages and Systems - 27th European Symp. on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, Springer,\u00a0Ahmed,\u00a0A.\u00a0(ed.),\u00a0(2018), 245\u2013271."},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-019-09540-0"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129522000068"},{"key":"e_1_3_1_24_2","volume-title":"Constructivism in Mathematics: An Introduction.","author":"Troelstra A.","year":"1988","unstructured":"Troelstra, A. and Dalen, D. Constructivism in Mathematics: An Introduction.\u00a0North-Holland, (1988)."},{"volume-title":"Homotopy Type Theory: Univalent Foundations of Mathematics","year":"2013","key":"e_1_3_1_25_2","unstructured":"T. Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, (2013); https:\/\/homotopytypetheory.org\/book."},{"key":"e_1_3_1_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0014566"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3715707","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3715707","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:48Z","timestamp":1750295928000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3715707"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,5,29]]},"references-count":25,"alternative-id":["10.1145\/3715707"],"URL":"https:\/\/doi.org\/10.1145\/3715707","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"type":"print","value":"0001-0782"},{"type":"electronic","value":"1557-7317"}],"subject":[],"published":{"date-parts":[[2025,5,29]]},"assertion":[{"value":"2025-05-29","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}],"article-number":"3715707"}}