{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T23:06:01Z","timestamp":1779836761472,"version":"3.53.1"},"reference-count":57,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2023,10,2]],"date-time":"2023-10-02T00:00:00Z","timestamp":1696204800000},"content-version":"unspecified","delay-in-days":274,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    We present the Kripke-style modal type theory,\n                    <jats:sc>Mint<\/jats:sc>\n                    , which combines dependent types and the necessity modality. It extends the Kripke-style modal lambda-calculus by Pfenning and Davies to the full Martin-L\u00f6f type theory. As such it encompasses dependently typed variants of system\n                    <jats:italic>K<\/jats:italic>\n                    ,\n                    <jats:italic>T<\/jats:italic>\n                    ,\n                    <jats:italic>K<\/jats:italic>\n                    4, and\n                    <jats:italic>S<\/jats:italic>\n                    4. Further,\n                    <jats:sc>Mint<\/jats:sc>\n                    seamlessly supports a full universe hierarchy, usual inductive types, and large eliminations. In this paper, we give a modular sound and complete normalization-by-evaluation (NbE) proof for\n                    <jats:sc>Mint<\/jats:sc>\n                    based on an untyped domain model, which applies to all four aforementioned modal systems without modification. This NbE proof yields a normalization algorithm for\n                    <jats:sc>Mint,<\/jats:sc>\n                    which can be directly implemented. To further strengthen our results, our models and the NbE proof are fully mechanized in Agda and we extract a Haskell implementation of our NbE algorithm from it.\n                  <\/jats:p>","DOI":"10.1017\/s0956796823000060","type":"journal-article","created":{"date-parts":[[2023,10,2]],"date-time":"2023-10-02T00:59:30Z","timestamp":1696208370000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":7,"title":["Normalization by evaluation for modal dependent type theory"],"prefix":"10.1017","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6710-6262","authenticated-orcid":false,"given":"JASON Z. S.","family":"HU","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6338-2155","authenticated-orcid":false,"given":"JUNYOUNG","family":"JANG","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"BRIGITTE","family":"PIENTKA","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2023,10,2]]},"reference":[{"key":"S0956796823000060_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_14"},{"key":"S0956796823000060_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3373718.3394736"},{"key":"S0956796823000060_ref48","doi-asserted-by":"publisher","DOI":"10.1145\/3571739"},{"key":"S0956796823000060_ref55","doi-asserted-by":"publisher","DOI":"10.1145\/3547649"},{"key":"S0956796823000060_ref56","doi-asserted-by":"crossref","unstructured":"Wieczorek, P. & Biernacki, D. (2018) A Coq formalization of normalization by evaluation for Martin-L\u00f6f type theory. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. New York, NY, USA: Association for Computing Machinery, pp. 266\u2013279.","DOI":"10.1145\/3167091"},{"key":"S0956796823000060_ref53","doi-asserted-by":"crossref","unstructured":"Taha, W. (2000) A sound reduction semantics for untyped CBN multi-stage computation. or, the theory of metaml is non-trivial (extended abstract). In PEPM. ACM, pp. 34\u201343.","DOI":"10.1145\/328691.328697"},{"key":"S0956796823000060_ref45","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328483"},{"key":"S0956796823000060_ref26","doi-asserted-by":"publisher","DOI":"10.1145\/3341711"},{"key":"S0956796823000060_ref43","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"S0956796823000060_ref35","unstructured":"Licata, D. R. , Orton, I. , Pitts, A. M. & Spitters, B. (2018) Internal universes in models of homotopy type theory. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Dagstuhl, Germany. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, pp. 22:1\u201322:17. ISSN: 1868-8969."},{"key":"S0956796823000060_ref57","doi-asserted-by":"publisher","DOI":"10.1145\/3473580"},{"key":"S0956796823000060_ref51","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"S0956796823000060_ref31","article-title":"Normalisation by evaluation for type theory, in type theory","volume":"13","author":"Kaposi","year":"2017","journal-title":"Logical Methods Comput. Sci."},{"key":"S0956796823000060_ref41","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198501275.003.0012"},{"key":"S0956796823000060_ref50","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00418-7"},{"key":"S0956796823000060_ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46678-0_26"},{"key":"S0956796823000060_ref9","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151645"},{"key":"S0956796823000060_ref54","doi-asserted-by":"publisher","DOI":"10.1145\/258993.259019"},{"key":"S0956796823000060_ref4","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888254"},{"key":"S0956796823000060_ref15","doi-asserted-by":"publisher","DOI":"10.1145\/1173706.1173724"},{"key":"S0956796823000060_ref19","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129596002150"},{"key":"S0956796823000060_ref46","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785683"},{"key":"S0956796823000060_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61780-9_66"},{"key":"S0956796823000060_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_35"},{"key":"S0956796823000060_ref34","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19630090502"},{"key":"S0956796823000060_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"S0956796823000060_ref49","doi-asserted-by":"publisher","DOI":"10.1023\/A:1010027404223"},{"key":"S0956796823000060_ref39","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855774"},{"key":"S0956796823000060_ref10","doi-asserted-by":"publisher","DOI":"10.1023\/A:1005291931660"},{"key":"S0956796823000060_ref8","unstructured":"Barras, B. & Werner, B. (1997) Coq in coq."},{"key":"S0956796823000060_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60164-3_27"},{"key":"S0956796823000060_ref44","unstructured":"Pfenning, F. & Wong, H. (1995) On a modal lambda calculus for S4. IN Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, MFPS 1995, Tulane University, New Orleans, LA, USA, March 29\u2013April 1, 1995. Elsevier, pp. 515\u2013534."},{"key":"S0956796823000060_ref47","doi-asserted-by":"publisher","DOI":"10.1145\/3498693"},{"key":"S0956796823000060_ref23","doi-asserted-by":"publisher","DOI":"10.2307\/2586554"},{"key":"S0956796823000060_ref27","doi-asserted-by":"publisher","DOI":"10.1145\/1042038.1042041"},{"key":"S0956796823000060_ref30","doi-asserted-by":"publisher","DOI":"10.1145\/3498700"},{"key":"S0956796823000060_ref52","unstructured":"Sterling, J. (2022) First Steps in Synthetic Tait Computability: The Objective Metatheory of Cubical Type Theory. PhD Thesis. Carnegie Mellon University, USA."},{"key":"S0956796823000060_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-017-2798-3_12"},{"key":"S0956796823000060_ref12","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129519000197"},{"key":"S0956796823000060_ref2","doi-asserted-by":"publisher","DOI":"10.1145\/3158111"},{"key":"S0956796823000060_ref32","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005089"},{"key":"S0956796823000060_ref33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34175-6_4"},{"key":"S0956796823000060_ref1","unstructured":"Abel, A. (2013) Normalization by Evaluation: Dependent Types and Impredicativity. Habilitation Thesis. Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen."},{"key":"S0956796823000060_ref29","unstructured":"Hu, J. Z. S. & Pientka, B. (2022b) An Investigation of Kripke-style Modal Type Theories. Number: arXiv:2206.07823 arXiv:2206.07823 [cs]."},{"key":"S0956796823000060_ref13","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129519000197"},{"key":"S0956796823000060_ref24","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3532398"},{"key":"S0956796823000060_ref11","unstructured":"Bierman, G. M. & de Paiva, V. C. V. (1996) Intuitionistic Necessity Revisited. Technical report. University of Birmingham."},{"key":"S0956796823000060_ref20","first-page":"93","volume-title":"TYPES","author":"Danielsson","year":"2006"},{"key":"S0956796823000060_ref7","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837638"},{"key":"S0956796823000060_ref14","unstructured":"Borghuis, V. A. J. (1994) Coming to Terms with Modal Logic: On the Interpretation of Modalities in Typed Lambda-Calculus. PhD Thesis. Mathematics and Computer Science."},{"key":"S0956796823000060_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.114"},{"key":"S0956796823000060_ref6","unstructured":"Altenkirch, T. & Kaposi, A. (2016a) Normalisation by evaluation for dependent types. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Dagstuhl, Germany. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, pp. 6:1\u20136:16. ISSN: 1868-8969."},{"key":"S0956796823000060_ref37","doi-asserted-by":"publisher","DOI":"10.1016\/S0049-237X(08)71945-1"},{"key":"S0956796823000060_ref42","doi-asserted-by":"publisher","DOI":"10.1145\/581478.581499"},{"key":"S0956796823000060_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_19"},{"key":"S0956796823000060_ref3","doi-asserted-by":"publisher","DOI":"10.1145\/3110277"},{"key":"S0956796823000060_ref28","doi-asserted-by":"publisher","DOI":"10.46298\/entics.10360"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796823000060","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,5,26]],"date-time":"2026-05-26T22:37:00Z","timestamp":1779835020000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796823000060\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"references-count":57,"alternative-id":["S0956796823000060"],"URL":"https:\/\/doi.org\/10.1017\/s0956796823000060","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"\u00a9 The Author(s), 2023. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e7"}}