{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:59Z","timestamp":1772164019491,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":35,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,1]]},"DOI":"10.1145\/3009837.3009862","type":"proceedings-article","created":{"date-parts":[[2016,12,22]],"date-time":"2016-12-22T16:20:29Z","timestamp":1482423629000},"page":"653-665","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Intersection type calculi of bounded dimension"],"prefix":"10.1145","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":[[2017,1]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"The Lambda Calculus. Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics","author":"Barendregt H. P.","year":"1984","unstructured":"H. P. Barendregt . The Lambda Calculus. Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics , 2 nd Edition. Elsevier Science Publishers , 1984 . H. P. Barendregt. The Lambda Calculus. Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics, 2nd Edition. Elsevier Science Publishers, 1984.","edition":"2"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.2307\/2273659"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.5555\/2529641"},{"key":"e_1_3_2_1_4_1","volume-title":"Non-Idempotent Intersection Types and Strong Normalization. Logical Methods in Computer Science, 9(4:3):1 \u2013 46","author":"Bernadet A.","year":"2013","unstructured":"A. Bernadet and S. Graham-Lengrand . Non-Idempotent Intersection Types and Strong Normalization. Logical Methods in Computer Science, 9(4:3):1 \u2013 46 , 2013 . A. Bernadet and S. Graham-Lengrand. Non-Idempotent Intersection Types and Strong Normalization. Logical Methods in Computer Science, 9(4:3):1 \u2013 46, 2013."},{"key":"e_1_3_2_1_5_1","volume-title":"TCS 2014, Proceedings of 8th IFIP TC 1 \/WG 2.2 International Conference on Theoretical Computer Science","author":"Bucciareli A.","year":"2014","unstructured":"A. Bucciareli , D. Kesner , and S. Ronchi Della Rocca. The inhabitation problem for non-idempotent intersection types . In TCS 2014, Proceedings of 8th IFIP TC 1 \/WG 2.2 International Conference on Theoretical Computer Science , Rome, Italy , September 1-3, 2014 . Springer, 2014. A. Bucciareli, D. Kesner, and S. Ronchi Della Rocca. The inhabitation problem for non-idempotent intersection types. In TCS 2014, Proceedings of 8th IFIP TC 1 \/WG 2.2 International Conference on Theoretical Computer Science, Rome, Italy, September 1-3, 2014. Springer, 2014."},{"key":"e_1_3_2_1_6_1","unstructured":"M. W.\n      Bunder\n    .\n  The inhabitation problem for intersection types\n  . J. Harland and P. Manyem editors Computing\n  : The Australasian Theory Symposium volume \n  77\n   of \n  Conferences in Research and Practice in Information Technology Australian Computer Society pages \n  7\n   \u2013 14 2008\n  .   M. W. Bunder. The inhabitation problem for intersection types. J. Harland and P. Manyem editors Computing: The Australasian Theory Symposium volume 77 of Conferences in Research and Practice in Information Technology Australian Computer Society pages 7 \u2013 14 2008."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1141"},{"key":"e_1_3_2_1_9_1","volume-title":"Accademic Press","author":"Coppo M.","year":"1980","unstructured":"M. Coppo , M. Dezani-Ciancaglini , and B. Venneri . Principal Type Schemes and Lambda-Calculus Semantics, pages 480\u2013490 . Accademic Press , London , 1980 . Ed.: R. Hindley and J. Seldin. M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Principal Type Schemes and Lambda-Calculus Semantics, pages 480\u2013490. Accademic Press, London, 1980. Ed.: R. Hindley and J. Seldin."},{"key":"e_1_3_2_1_10_1","first-page":"58","volume-title":"Functional Characters of Solvable Terms. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik","author":"Coppo M.","year":"1981","unstructured":"M. Coppo , M. Dezani-Ciancaglini , and B. Venneri . Functional Characters of Solvable Terms. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik , pages 45\u2013 58 , 1981 . M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional Characters of Solvable Terms. Zeitschrift f\u00fcr mathematische Logik und Grundlagen der Mathematik, pages 45\u201358, 1981."},{"key":"e_1_3_2_1_11_1","volume-title":"FOPARA 2015, Foundational and Practical Aspects of Resource Analysis - 4th International Workshop","author":"De Benedetti E.","year":"2015","unstructured":"E. De Benedetti and S. Ronchi Della Rocca. Call-by-value, elementary time and intersection types . In FOPARA 2015, Foundational and Practical Aspects of Resource Analysis - 4th International Workshop , London, UK , April 11 2015 , Revised Selected Papers, pages 40\u201359. Springer LNCS 9964, 2016. E. De Benedetti and S. Ronchi Della Rocca. Call-by-value, elementary time and intersection types. In FOPARA 2015, Foundational and Practical Aspects of Resource Analysis - 4th International Workshop, London, UK, April 11 2015, Revised Selected Papers, pages 40\u201359. Springer LNCS 9964, 2016."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.12.012"},{"key":"e_1_3_2_1_13_1","volume-title":"Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs \/0905.4251","author":"de Carvalho D.","year":"2009","unstructured":"D. de Carvalho . Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs \/0905.4251 , 2009 . D. de Carvalho. Execution time of lambda-terms via denotational semantics and intersection types. CoRR, abs \/0905.4251, 2009."},{"key":"e_1_3_2_1_14_1","series-title":"LIPIcs","first-page":"258","volume-title":"CSL","author":"D\u00fcdder B.","year":"2012","unstructured":"B. D\u00fcdder , M. Martens , J. Rehof , and P. Urzyczyn . Bounded Combinatory Logic . In CSL 2012 , Proceedings of Computer Science Logic , volume 16 of LIPIcs , pages 243\u2013 258 . Schloss Dagstuhl, 2012. B. D\u00fcdder, M. Martens, J. Rehof, and P. Urzyczyn. Bounded Combinatory Logic. In CSL 2012, Proceedings of Computer Science Logic, volume 16 of LIPIcs, pages 243\u2013258. Schloss Dagstuhl, 2012."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_5"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837629"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1988.5101"},{"key":"e_1_3_2_1_19_1","volume-title":"Cambridge Tracts in Theoretical Computer Science","author":"Hindley J. R.","year":"2008","unstructured":"J. R. Hindley . Basic Simple Type Theory . Cambridge Tracts in Theoretical Computer Science , vol. 42 , Cambridge University Press , 2008 . J. R. Hindley. Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, vol. 42, Cambridge University Press, 2008."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2873052"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292556"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/645892.758319"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1770203.1770221"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/567067.567077"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-0526-5_15"},{"key":"e_1_3_2_1_26_1","volume-title":"Technical Report Memorandum SAI-RM-4, School of Artificial Intelligence","author":"Plotkin G.","year":"1973","unstructured":"G. Plotkin . Lambda definability and logical relations. Technical Report Memorandum SAI-RM-4, School of Artificial Intelligence , University of Edinburgh , 1973 . G. Plotkin. Lambda definability and logical relations. Technical Report Memorandum SAI-RM-4, School of Artificial Intelligence, University of Edinburgh, 1973."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2021953.2021970"},{"key":"e_1_3_2_1_28_1","series-title":"LNCS","first-page":"270","volume-title":"Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday","author":"Rehof J.","unstructured":"J. Rehof and P. Urzyczyn . The Complexity of Inhabitation with Explicit Intersection . In R. L. Constable and A. Silva, editors, Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday , volume 7230 of LNCS , pages 256\u2013 270 . Springer, 2012. J. Rehof and P. Urzyczyn. The Complexity of Inhabitation with Explicit Intersection. In R. L. Constable and A. Silva, editors, Logic and Program Semantics - Essays Dedicated to Dexter Kozen on the Occasion of His 60th Birthday, volume 7230 of LNCS, pages 256\u2013270. Springer, 2012."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02261-6_5"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31585-5_34"},{"key":"e_1_3_2_1_31_1","first-page":"67","volume":"9","author":"Statman R.","year":"1979","unstructured":"R. Statman . Intuitionistic Propositional Logic Is Polynomial-space Complete. Theoretical Computer Science , 9 : 67 \u2013 72 , 1979 . R. Statman. Intuitionistic Propositional Logic Is Polynomial-space Complete. Theoretical Computer Science, 9:67\u201372, 1979.","journal-title":"Intuitionistic Propositional Logic Is Polynomial-space Complete. Theoretical Computer Science"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.2307\/2586625"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02273-9_26"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90297-S"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00073-6"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1922649.1922657"}],"event":{"name":"POPL '17: The 44th Annual ACM SIGPLAN Symposium on Principles of Programming Languages","location":"Paris France","acronym":"POPL '17","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009862","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3009837.3009862","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:36:22Z","timestamp":1750203382000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3009837.3009862"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1]]},"references-count":35,"alternative-id":["10.1145\/3009837.3009862","10.1145\/3009837"],"URL":"https:\/\/doi.org\/10.1145\/3009837.3009862","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/3093333.3009862","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2017,1]]},"assertion":[{"value":"2017-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}