{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:53:39Z","timestamp":1770288819817,"version":"3.49.0"},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100008398","name":"Villum Fonden","doi-asserted-by":"publisher","award":["12386, Guarded Homotopy Type Theory"],"award-info":[{"award-number":["12386, Guarded Homotopy Type Theory"]}],"id":[{"id":"10.13039\/100008398","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"publisher","award":["FA9550-15-1-0053"],"award-info":[{"award-number":["FA9550-15-1-0053"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100008394","name":"Natur og Univers, Det Frie Forskningsr\u00e5d","doi-asserted-by":"crossref","award":["ModuRes Sapere Aude Advanced Grant"],"award-info":[{"award-number":["ModuRes Sapere Aude Advanced Grant"]}],"id":[{"id":"10.13039\/100008394","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,7,26]]},"abstract":"<jats:p>Modalities are everywhere in programming and mathematics! Despite this, however, there are still significant technical challenges in formulating a core dependent type theory with modalities. We present a dependent type theory<jats:italic>MLTT<\/jats:italic><jats:sub>\ud83d\udd12<\/jats:sub>supporting the connectives of standard Martin-L\u00f6f Type Theory as well as an<jats:bold>S4<\/jats:bold>-style necessity operator.<jats:italic>MLTT<\/jats:italic><jats:sub>\ud83d\udd12<\/jats:sub>supports a smooth interaction between modal and dependent types and provides a common basis for the use of modalities in programming and in synthetic mathematics. We design and prove the soundness and completeness of a type checking algorithm for<jats:italic>MLTT<\/jats:italic><jats:sub>\ud83d\udd12<\/jats:sub>, using a novel extension of normalization by evaluation. We have also implemented our algorithm in a prototype proof assistant for<jats:italic>MLTT<\/jats:italic><jats:sub>\ud83d\udd12<\/jats:sub>, demonstrating the ease of applying our techniques.<\/jats:p>","DOI":"10.1145\/3341711","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Implementing a modal dependent type theory"],"prefix":"10.1145","volume":"3","author":[{"given":"Daniel","family":"Gratzer","sequence":"first","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jonathan","family":"Sterling","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292555"},{"key":"e_1_2_2_2_1","volume-title":"2009 Workshop on Normalization by Evaluation.","author":"Abel Andreas","year":"2009"},{"key":"e_1_2_2_3_1","unstructured":"Andreas Abel. 2013. Normalization by Evaluation: Dependent Types and Impredicativity. Andreas Abel. 2013. Normalization by Evaluation: Dependent Types and Impredicativity."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.02.025"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_3"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110277"},{"key":"e_1_2_2_7_1","unstructured":"Stuart Frazier Allen. 1987. A non-type-theoretic semantics for type-theoretic language. Stuart Frazier Allen. 1987. A non-type-theoretic semantics for type-theoretic language."},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Thorsten Altenkirch Martin Hofmann and Thomas Streicher. 1995. Categorical reconstruction of a reduction free normalization proof. In Category Theory and Computer Science David Pitt David E. Rydeheard and Peter Johnstone (Eds.). Springer Berlin Heidelberg 182\u2013199. Thorsten Altenkirch Martin Hofmann and Thomas Streicher. 1995. Categorical reconstruction of a reduction free normalization proof. In Category Theory and Computer Science David Pitt David E. Rydeheard and Peter Johnstone (Eds.). Springer Berlin Heidelberg 182\u2013199.","DOI":"10.1007\/3-540-60164-3_27"},{"key":"e_1_2_2_10_1","volume-title":"Licata","author":"Angiuli Carlo","year":"2019"},{"key":"e_1_2_2_11_1","volume-title":"2017 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS). 1\u201312","author":"Bahr P."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1991.151645"},{"key":"e_1_2_2_13_1","volume-title":"Bas Spitters, and Andrea Vezzosi.","author":"Birkedal Lars","year":"2016"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.16"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2018.03.016"},{"key":"e_1_2_2_16_1","volume-title":"Ranald Clouston, Rasmus E. M\u00f8gelberg, and Lars Birkedal.","author":"Bizjak Ale\u0161","year":"2016"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.007"},{"key":"e_1_2_2_18_1","volume-title":"Multi-level Contextual Type Theory. Electronic Proceedings in Theoretical Computer Science 71 (Oct.","author":"Boespflug Mathieu","year":"2011"},{"key":"e_1_2_2_19_1","unstructured":"V. A. J. Borghuis. 1994. Coming to terms with modal logic : on the interpretation of modalities in typed lambda-calculus. V. A. J. Borghuis. 1994. Coming to terms with modal logic : on the interpretation of modalities in typed lambda-calculus."},{"key":"e_1_2_2_20_1","volume-title":"A Contextual Logical Framework","author":"Bock Peter Brottveit"},{"key":"e_1_2_2_21_1","volume-title":"Foundations of Software Science and Computation Structures","author":"Clouston Ranald"},{"key":"e_1_2_2_22_1","volume-title":"Hans Bugge Grathwohl, and Lars Birkedal","author":"Clouston Ranald","year":"2015"},{"key":"e_1_2_2_23_1","volume-title":"Andrew M. Pitts, and Bas Spitters.","author":"Clouston Ranald","year":"2018"},{"key":"e_1_2_2_24_1","unstructured":"The Coq Development Team. 2016. The Coq Proof Assistant Reference Manual. The Coq Development Team. 2016. The Coq Proof Assistant Reference Manual."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(95)00021-6"},{"key":"e_1_2_2_26_1","unstructured":"Thierry Coquand. 2018. Canonicity and normalization for Dependent Type Theory. https:\/\/arxiv.org\/abs\/1810.09367 Thierry Coquand. 2018. Canonicity and normalization for Dependent Type Theory. https:\/\/arxiv.org\/abs\/1810.09367"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/382780.382785"},{"key":"e_1_2_2_28_1","doi-asserted-by":"crossref","unstructured":"Jeff Epstein Andrew Black and Simon Peyton Jones. 2011. Towards Haskell in the cloud. https:\/\/www.microsoft.com\/enus\/research\/publication\/towards-haskell-cloud\/ Jeff Epstein Andrew Black and Simon Peyton Jones. 2011. Towards Haskell in the cloud. https:\/\/www.microsoft.com\/enus\/research\/publication\/towards-haskell-cloud\/","DOI":"10.1145\/2034675.2034690"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/571157.571161"},{"key":"e_1_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Peter Freyd. 1991. Algebraically complete categories. In Category Theory Aurelio Carboni Maria Cristina Pedicchio and Guiseppe Rosolini (Eds.). Springer Berlin Heidelberg 95\u2013104. Peter Freyd. 1991. Algebraically complete categories. In Category Theory Aurelio Carboni Maria Cristina Pedicchio and Guiseppe Rosolini (Eds.). Springer Berlin Heidelberg 95\u2013104.","DOI":"10.1007\/BFb0084215"},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","volume-title":"Treatise on Intuitionistic Type Theory","author":"Granstr\u00f6m Johan G.","DOI":"10.1007\/978-94-007-1736-7"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209148"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006430"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330024"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_26"},{"key":"e_1_2_2_36_1","doi-asserted-by":"crossref","unstructured":"F. William Lawvere. 1992. Categories of Space and of Quantity. In The Space of Mathematics Javier Echeverria Andoni Ibarra and Thomas Mormann (Eds.). De Gruyter 14\u201330. F. William Lawvere. 1992. Categories of Space and of Quantity. In The Space of Mathematics Javier Echeverria Andoni Ibarra and Thomas Mormann (Eds.). De Gruyter 14\u201330.","DOI":"10.1515\/9783110870299.14"},{"key":"e_1_2_2_37_1","volume-title":"Theory and Applications of Categories 19 (June","author":"Lawvere F. William","year":"2007"},{"key":"e_1_2_2_38_1","volume-title":"Internal Universes in Models of Homotopy Type Theory. In 3rd International Conference on Formal Structures for Computation and Deduction, FSCD 2018","author":"Licata Daniel R.","year":"2018"},{"key":"e_1_2_2_39_1","volume-title":"2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (Leibniz International Proceedings in Informatics (LIPIcs)), Dale Miller (Ed.)","volume":"84","author":"Licata Daniel R.","year":"2017"},{"key":"e_1_2_2_40_1","volume-title":"3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) (Leibniz International Proceedings in Informatics (LIPIcs)), H\u00e9l\u00e8ne Kirchner (Ed.)","author":"Mannaa Bassel"},{"key":"e_1_2_2_41_1","volume-title":"Logic Colloquium \u201973","author":"Martin-L\u00f6f Per"},{"key":"e_1_2_2_42_1","unstructured":"Per Martin-L\u00f6f. 1992. Substitution calculus. Notes from a lecture given in G\u00f6teborg. Per Martin-L\u00f6f. 1992. Substitution calculus. Notes from a lecture given in G\u00f6teborg."},{"key":"e_1_2_2_43_1","first-page":"11","article-title":"On the meanings of the logical constants and the justifications of the logical laws","volume":"1","author":"Martin-L\u00f6f Per","year":"1996","journal-title":"Nordic Journal of Philosophical Logic"},{"key":"e_1_2_2_44_1","doi-asserted-by":"crossref","volume-title":"A Computational Interpretation of Modal Proofs","author":"Martini Simone","DOI":"10.1007\/978-94-017-2798-3_12"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006326"},{"key":"e_1_2_2_46_1","volume-title":"Modal Types for Mobile Code","author":"Murphy Tom"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/1018438.1021865"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785683"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_2_53_1","first-page":"255","article-title":"Natural Deduction. A Proof-Theoretical Study","volume":"32","author":"Prawitz Dag","year":"1967","journal-title":"Journal of Symbolic Logic"},{"key":"e_1_2_2_54_1","volume-title":"Article arXiv:1310.7930 (Oct","author":"Schreiber Urs","year":"2013"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.158.8"},{"key":"e_1_2_2_56_1","unstructured":"Peter Schroeder-Heister. 1987. Structural Frameworks with Higher-level Rules: Philosophical Investigations on the Foundations of Formal Reasoning. Habilitation thesis. Peter Schroeder-Heister. 1987. Structural Frameworks with Higher-level Rules: Philosophical Investigations on the Foundations of Formal Reasoning. Habilitation thesis."},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129517000147"},{"key":"e_1_2_2_58_1","volume-title":"Preliminary Proceedings of the APPSEM Workshop on Normalisation by Evaluation, O. Danvy and P. Dybjer (Eds.). Department of Computer Science","author":"Streicher Thomas","year":"1998"},{"key":"e_1_2_2_59_1","unstructured":"The Agda Development Team. 2018. agda-flat. https:\/\/github.com\/agda\/agda\/tree\/flat The Agda Development Team. 2018. agda-flat. https:\/\/github.com\/agda\/agda\/tree\/flat"},{"key":"e_1_2_2_60_1","unstructured":"The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https: \/\/homotopytypetheory.org\/book . The Univalent Foundations Program. 2013. Homotopy Type Theory: Univalent Foundations of Mathematics. https: \/\/homotopytypetheory.org\/book ."},{"key":"e_1_2_2_61_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\/10.1145\/3341711","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341711","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341711","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:24Z","timestamp":1750207404000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341711"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":59,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341711"],"URL":"https:\/\/doi.org\/10.1145\/3341711","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}