{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:09:37Z","timestamp":1760202577795,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2007,11,15]],"date-time":"2007-11-15T00:00:00Z","timestamp":1195084800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/assumed-1991-2003"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>In a previous work Baillot and Terui introduced Dual light affine logic\n(DLAL) as a variant of Light linear logic suitable for guaranteeing complexity\nproperties on lambda calculus terms: all typable terms can be evaluated in\npolynomial time by beta reduction and all Ptime functions can be represented.\nIn the present work we address the problem of typing lambda-terms in\nsecond-order DLAL. For that we give a procedure which, starting with a term\ntyped in system F, determines whether it is typable in DLAL and outputs a\nconcrete typing if there exists any. We show that our procedure can be run in\ntime polynomial in the size of the original Church typed system F term.<\/jats:p>","DOI":"10.2168\/lmcs-3(4:10)2007","type":"journal-article","created":{"date-parts":[[2008,6,3]],"date-time":"2008-06-03T13:14:33Z","timestamp":1212498873000},"source":"Crossref","is-referenced-by-count":10,"title":["Verification of Ptime Reducibility for system F Terms: Type Inference in Dual Light Affine Logic"],"prefix":"10.46298","volume":"Volume 3, Issue 4","author":[{"given":"Vincent","family":"Atassi","sequence":"first","affiliation":[]},{"given":"Patrick","family":"Baillot","sequence":"additional","affiliation":[]},{"given":"Kazushige","family":"Terui","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2007,11,15]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1234\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1234\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:06:17Z","timestamp":1681243577000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1234"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,11,15]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-3(4:10)2007","relation":{"is-same-as":[{"id-type":"arxiv","id":"0710.1153","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0710.1153","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2007,11,15]]},"article-number":"1234"}}