{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,28]],"date-time":"2026-08-28T17:09:16Z","timestamp":1787936956041,"version":"build-2784847793"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/T026960\/1"],"award-info":[{"award-number":["EP\/T026960\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>We combine dependent types with linear type systems that soundly and completely capture polynomial time computation. We explore two systems for capturing polynomial time: one system that disallows construction of iterable data, and one, based on the LFPL system of Martin Hofmann, that controls construction via a payment method. Both of these are extended to full dependent types via Quantitative Type Theory, allowing for arbitrary computation in types alongside guaranteed polynomial time computation in terms. We prove the soundness of the systems using a realisability technique due to Dal Lago and Hofmann.<\/jats:p>\n                  <jats:p>\n                    Our long-term goal is to combine the extensional reasoning of type theory with intensional reasoning about the resources intrinsically consumed by programs. This paper is a step along this path, which we hope will lead both to practical systems for reasoning about programs\u2019 resource usage, and to theoretical use as a form of\n                    <jats:italic toggle=\"yes\">synthetic computational complexity theory<\/jats:italic>\n                    .\n                  <\/jats:p>","DOI":"10.1145\/3632918","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T15:48:51Z","timestamp":1704469731000},"page":"2288-2317","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Polynomial Time and Dependent Types"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4414-5047","authenticated-orcid":false,"given":"Robert","family":"Atkey","sequence":"first","affiliation":[{"name":"University of Strathclyde, Glasgow, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.002"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607862"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/507382.507386"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804090"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8425923"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","unstructured":"Robert Atkey. 2023b. Polynomial Time and Dependent Types - Extended Version. (2023). https:\/\/doi.org\/10.48550\/arXiv.2307.09145 10.48550\/arXiv.2307.09145 arXiv:2307.09145.","DOI":"10.48550\/arXiv.2307.09145"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_7"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24727-2_4"},{"key":"e_1_3_1_11_1","volume-title":"Dual Intuitionistic Linear Logic","author":"Barber Andrew","year":"1996","unstructured":"Andrew Barber. 1996. Dual Intuitionistic Linear Logic. Technical Report. University of Edinburgh."},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.049"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201998"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022251"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2951"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45413-6_10"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31485-8_3"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(4:7)2010"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-009-9210-x"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.12.025"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.MFCS.2021.35"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2015.04.006"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2014.10.009"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.46298\/lmcs-18(3:28)2022"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1998.2700"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90386-T"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_19"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571221"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000487"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511526619.004"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1999.782641"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00009-9"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.019"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796897002864"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1017\/s0956796800003889"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676969"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.10.018"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-30936-1_12"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29604-3_10"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_17"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498670"},{"key":"e_1_3_1_50_1","first-page":"230","volume-title":"International school on advanced functional programming","author":"Norell Ulf","year":"2008","unstructured":"Ulf Norell. 2008. Dependently typed programming in Agda. In International school on advanced functional programming. Springer, 230\u2013266."},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434308"},{"key":"e_1_3_1_53_1","article-title":"Syntax and Semantics of Linear Dependent Types","author":"V\u00e1k\u00e1r Matthijs","year":"2014","unstructured":"Matthijs V\u00e1k\u00e1r. 2014. Syntax and Semantics of Linear Dependent Types. CoRR abs\/1405.0033 (2014). http:\/\/arxiv.org\/abs\/1405.0033","journal-title":"CoRR"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632918","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632918","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:06:47Z","timestamp":1751645207000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632918"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":52,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632918"],"URL":"https:\/\/doi.org\/10.1145\/3632918","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}