{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,24]],"date-time":"2025-11-24T07:08:17Z","timestamp":1763968097189,"version":"3.41.2"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,10,23]],"date-time":"2012-10-23T00:00:00Z","timestamp":1350950400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["272487"],"award-info":[{"award-number":["272487"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>A system of linear dependent types for the lambda calculus with full\nhigher-order recursion, called dlPCF, is introduced and proved sound and\nrelatively complete. Completeness holds in a strong sense: dlPCF is not only\nable to precisely capture the functional behaviour of PCF programs (i.e. how\nthe output relates to the input) but also some of their intensional properties,\nnamely the complexity of evaluating them with Krivine's Machine. dlPCF is\ndesigned around dependent types and linear logic and is parametrized on the\nunderlying language of index terms, which can be tuned so as to sacrifice\ncompleteness for tractability.<\/jats:p>","DOI":"10.2168\/lmcs-8(4:11)2012","type":"journal-article","created":{"date-parts":[[2013,11,29]],"date-time":"2013-11-29T13:21:33Z","timestamp":1385731293000},"source":"Crossref","is-referenced-by-count":11,"title":["Linear Dependent Types and Relative Completeness"],"prefix":"10.46298","volume":"Volume 8, Issue 4","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9200-070X","authenticated-orcid":false,"given":"Ugo Dal","family":"Lago","sequence":"first","affiliation":[]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,10,23]]},"reference":[{"key":"716:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/974\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/974\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:00:27Z","timestamp":1681243227000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/974"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,10,23]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(4:11)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1104.0193","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1104.0193","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,10,23]]},"article-number":"974"}}