{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:31:59Z","timestamp":1750221119217,"version":"3.41.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"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":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>We develop an algebraic and algorithmic theory of principality for the recently introduced framework of intersection type calculi with dimensional bound. The theory enables inference of principal type information under dimensional bound, it provides an algebraic and algorithmic theory of approximation of classical principal types in terms of computable bases of abstract vector spaces (more precisely, semimodules), and it shows a systematic connection of dimensional calculi to the theory of approximants. Finite, computable bases are shown to span standard principal typings of a given term for sufficiently high dimension, thereby providing an approximation to standard principality by type inference, and capturing it precisely for sufficiently large dimensional parameter. Subsidiary results include decidability of principal inhabitation for intersection types (given a type does there exist a normal form for which the type is principal?). Remarkably, combining bounded type inference with principal inhabitation allows us to compute approximate normal forms of arbitrary terms without using beta-reduction.<\/jats:p>","DOI":"10.1145\/3290321","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Principality and approximation under dimensional bound"],"prefix":"10.1145","volume":"3","author":[{"given":"Andrej","family":"Dudenhefner","sequence":"first","affiliation":[{"name":"TU Dortmund, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jakob","family":"Rehof","sequence":"additional","affiliation":[{"name":"TU Dortmund, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. 1\u201328","author":"Alpuim Jo\u00e3o","year":"2017","unstructured":"Jo\u00e3o Alpuim , Bruno C. d. S. Oliveira , and Zhiyuan Shi . 2017 . Disjoint Polymorphism. In Programming Languages and Systems -26th European Symposium on Programming , ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. 1\u201328 . Jo\u00e3o Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi. 2017. Disjoint Polymorphism. In Programming Languages and Systems -26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings. 1\u201328."},{"key":"e_1_2_2_2_1","volume-title":"Algebra","author":"Artin Michael","unstructured":"Michael Artin . 2011. Algebra ( 2 nd edition). Pearson Education . Michael Artin. 2011. Algebra (2nd edition). Pearson Education.","edition":"2"},{"key":"e_1_2_2_3_1","volume-title":"The Lambda Calculus. Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics","author":"Barendregt Henk P.","unstructured":"Henk P. Barendregt . 1984. The Lambda Calculus. Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics , 2 nd Edition. Elsevier Science Publishers . Henk P. Barendregt. 1984. The Lambda Calculus. Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, 2nd Edition. Elsevier Science Publishers.","edition":"2"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"volume-title":"Lambda Calculus with Types. Perspectives in Logic","author":"Barendregt Henk P.","key":"e_1_2_2_5_1","unstructured":"Henk P. Barendregt , Wil Dekkers , and Richard Statman . 2013. Lambda Calculus with Types. Perspectives in Logic , Cambridge University Press . Henk P. Barendregt, Wil Dekkers, and Richard Statman. 2013. Lambda Calculus with Types. Perspectives in Logic, Cambridge University Press."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.01.045"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.03.026"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/2594832.2594835"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093883253"},{"volume-title":"ICALP International Colloquium on Automata, Languages, and Programming","author":"Coppo Mario","key":"e_1_2_2_10_1","unstructured":"Mario Coppo , Mariangiola Dezani-Ciancaglini , and Patrick Sall\u00e9 . 1979. Functional characterization of some semantic equalities inside \u03bb-calculus . In ICALP International Colloquium on Automata, Languages, and Programming . Springer LNCS 71. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Patrick Sall\u00e9. 1979. Functional characterization of some semantic equalities inside \u03bb-calculus. In ICALP International Colloquium on Automata, Languages, and Programming. Springer LNCS 71."},{"volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Coppo Mario","key":"e_1_2_2_11_1","unstructured":"Mario Coppo , Mariangiola Dezani-Ciancaglini , and Betti Venneri . 1980. Principal Type Schemes and \u03bb-Calculus Semantics . In R. Hindley and J. Seldin (Eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism . Accademic Press , London , 480\u2013490. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1980. Principal Type Schemes and \u03bb-Calculus Semantics. In R. Hindley and J. Seldin (Eds.), To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Accademic Press, London, 480\u2013490."},{"key":"e_1_2_2_12_1","volume-title":"Functional Characters of Solvable Terms. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik","author":"Coppo Mario","year":"1981","unstructured":"Mario Coppo , Mariangiola Dezani-Ciancaglini , and Betti Venneri . 1981. Functional Characters of Solvable Terms. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik ( 1981 ), 45\u201358. Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1981. Functional Characters of Solvable Terms. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik (1981), 45\u201358."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1141"},{"key":"e_1_2_2_14_1","volume-title":"11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings. 125\u2013139","author":"D\u00fcdder Boris","year":"2013","unstructured":"Boris D\u00fcdder , Moritz Martens , and Jakob Rehof . 2013 . Intersection Type Matching with Subtyping. In Typed Lambda Calculi and Applications , 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings. 125\u2013139 . Boris D\u00fcdder, Moritz Martens, and Jakob Rehof. 2013. Intersection Type Matching with Subtyping. In Typed Lambda Calculi and Applications, 11th International Conference, TLCA 2013, Eindhoven, The Netherlands, June 26-28, 2013. Proceedings. 125\u2013139."},{"key":"e_1_2_2_15_1","volume-title":"The Complexity of Principal Inhabitation. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017","author":"Dudenhefner Andrej","year":"2017","unstructured":"Andrej Dudenhefner and Jakob Rehof . 2017 a. The Complexity of Principal Inhabitation. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017 , September 3-9, 2017, Oxford, UK. 15:1\u201315:14. Andrej Dudenhefner and Jakob Rehof. 2017a. The Complexity of Principal Inhabitation. In 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK. 15:1\u201315:14."},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009862"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005127"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"volume-title":"Semirings and their Applications","author":"Golan Jonathan S.","key":"e_1_2_2_19_1","unstructured":"Jonathan S. Golan . 1999. Semirings and their Applications . Springer . Jonathan S. Golan. 1999. Semirings and their Applications. Springer."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2873052"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/317636.317788"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292556"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.032"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.758319"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567077"},{"key":"e_1_2_2_26_1","volume-title":"The Delta-calculus: syntax and types. CoRR abs\/1803.09660","author":"Liquori Luigi","year":"2018","unstructured":"Luigi Liquori and Claude Stolze . 2018. The Delta-calculus: syntax and types. CoRR abs\/1803.09660 ( 2018 ). arXiv: 1803.09660 http:\/\/arxiv.org\/abs\/1803.09660 Luigi Liquori and Claude Stolze. 2018. The Delta-calculus: syntax and types. CoRR abs\/1803.09660 (2018). arXiv: 1803.09660 http:\/\/arxiv.org\/abs\/1803.09660"},{"volume-title":"Nuttin\u2019. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. 207\u2013233.","author":"McBride Conor","key":"e_1_2_2_27_1","unstructured":"Conor McBride . 2016. I Got Plenty o \u2019 Nuttin\u2019. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. 207\u2013233. Conor McBride. 2016. I Got Plenty o\u2019 Nuttin\u2019. In A List of Successes That Can Change the World - Essays Dedicated to Philip Wadler on the Occasion of His 60th Birthday. 207\u2013233."},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01404107"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1016850.1016871"},{"volume-title":"To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism","author":"Pottinger Garrel","key":"e_1_2_2_30_1","unstructured":"Garrel Pottinger . 1980. A Type Assignment for the Strongly Normalizable Lambda-Terms . In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism , J. Hindley and J. Seldin (Eds.). Academic Press , 561\u2013577. Garrel Pottinger. 1980. A Type Assignment for the Strongly Normalizable Lambda-Terms. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, J. Hindley and J. Seldin (Eds.). Academic Press, 561\u2013577."},{"volume-title":"Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday (LNCS), Robert L","author":"Rehof Jakob","key":"e_1_2_2_31_1","unstructured":"Jakob Rehof and Pawe\u0142 Urzyczyn . 2012. The Complexity of Inhabitation with Explicit Intersection . In Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday (LNCS), Robert L . Constable and Alexandra Silva (Eds.), Vol. 7230 . Springer , 256\u2013270. Jakob Rehof and Pawe\u0142 Urzyczyn. 2012. The Complexity of Inhabitation with Explicit Intersection. In Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday (LNCS), Robert L. Constable and Alexandra Silva (Eds.), Vol. 7230. Springer, 256\u2013270."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(88)90101-6"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90069-5"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2934553"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586625"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/3.6.643"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1922649.1922657"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290321","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290321","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:02:07Z","timestamp":1750208527000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290321"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":37,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290321"],"URL":"https:\/\/doi.org\/10.1145\/3290321","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}