{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T12:03:04Z","timestamp":1759147384881,"version":"3.41.2"},"reference-count":18,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,3,27]],"date-time":"2011-03-27T00:00:00Z","timestamp":1301184000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia, I.P.","award":["SFRH\/BPD\/34527\/2006"],"award-info":[{"award-number":["SFRH\/BPD\/34527\/2006"]}]},{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia, I.P.","award":["PTDC\/MAT\/104716\/2008"],"award-info":[{"award-number":["PTDC\/MAT\/104716\/2008"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We present three different functional interpretations of intuitionistic\nlinear logic ILL and show how these correspond to well-known functional\ninterpretations of intuitionistic logic IL via embeddings of IL into ILL. The\nmain difference from previous work of the second author is that in\nintuitionistic linear logic (as opposed to classical linear logic) the\ninterpretations of !A are simpler and simultaneous quantifiers are no longer\nneeded for the characterisation of the interpretations. We then compare our\napproach in developing these three proof interpretations with the one of de\nPaiva around the Dialectica category model of linear logic.<\/jats:p>","DOI":"10.2168\/lmcs-7(1:9)2011","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T12:18:47Z","timestamp":1316780327000},"source":"Crossref","is-referenced-by-count":1,"title":["Functional Interpretations of Intuitionistic Linear Logic"],"prefix":"10.46298","volume":"Volume 7, Issue 1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1447-9764","authenticated-orcid":false,"given":"Gilda","family":"Ferreira","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paulo","family":"Oliva","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2011,3,27]]},"reference":[{"key":"10.2168\/LMCS-7(1:9)2011_Avigad(98)","doi-asserted-by":"crossref","unstructured":"J. Avigad and S. Feferman. G\u00f6del's functional (``Dialectica\") interpretation. In S. R. Buss, editor,Handbook of proof theory, volume 137 ofStudies in Logic and the Foundations of Mathematics, pages 337-405. North Holland, Amsterdam, 1998.","DOI":"10.1016\/S0049-237X(98)80020-7"},{"issue":"2-3","key":"10.2168\/LMCS-7(1:9)2011_Biering(2008)","doi-asserted-by":"crossref","first-page":"290","DOI":"10.1016\/j.apal.2008.07.004","volume":"156","author":"B. Biering","year":"2008","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.2168\/LMCS-7(1:9)2011_Blute(04)","doi-asserted-by":"crossref","unstructured":"R. Blute and P. Scott. Category theory for linear logicians. In T. Ehrhard, P. Ruet, J-Y. Girard, and P. Scott, editors,Linear Logic in Computer Science, pages 1-52. Cambridge University Press, 2004.","DOI":"10.1017\/CBO9780511550850.002"},{"key":"10.2168\/LMCS-7(1:9)2011_Diller(74)","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/BF02025118","volume":"16","author":"J. Diller and W. Nahm","year":"1974","journal-title":"Arch. Math. Logik Grundlagenforsch"},{"issue":"6","key":"10.2168\/LMCS-7(1:9)2011_GO(2010)","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1002\/malq.200910112","volume":"56","author":"J. Gaspar and P. Oliva","year":"2010","journal-title":"Mathematical Logic Quarterly"},{"issue":"1","key":"10.2168\/LMCS-7(1:9)2011_Girard(87B)","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(87)90045-4","volume":"50","author":"J.-Y. Girard","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"10.2168\/LMCS-7(1:9)2011_Goedel(58)","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","volume":"12","author":"K. G\u00f6del","year":"1958","journal-title":"Dialectica"},{"key":"10.2168\/LMCS-7(1:9)2011_Hyland(02)","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1016\/S0168-0072(01)00075-6","volume":"114","author":"J. M. E. Hyland","year":"2002","journal-title":"Annals of Pure and Applied Logic"},{"key":"10.2168\/LMCS-7(1:9)2011_Kreisel(59)","unstructured":"G. Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting, editor,Constructivity in Mathematics, pages 101-128. North Holland, Amsterdam, 1959."},{"key":"10.2168\/LMCS-7(1:9)2011_Oliva(2007A)","doi-asserted-by":"crossref","unstructured":"P. Oliva. Computational interpretations of classical linear logic. InProceedings of WoLLIC'07, LNCS 4576, pages 285-296. Springer, 2007.","DOI":"10.1007\/978-3-540-73445-1_20"},{"key":"10.2168\/LMCS-7(1:9)2011_Oliva(2007)","doi-asserted-by":"crossref","unstructured":"P. Oliva. Modified realizability interpretation of classical linear logic. InProc. of the Twenty Second Annual IEEE Symposium on Logic in Computer Science LICS'07. IEEE Press, 2007.","DOI":"10.1109\/LICS.2007.32"},{"issue":"2","key":"10.2168\/LMCS-7(1:9)2011_Oliva(2008)","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1111\/j.1746-8361.2008.01135.x","volume":"62","author":"P. Oliva","year":"2008","journal-title":"dialectica"},{"issue":"5","key":"10.2168\/LMCS-7(1:9)2011_Oliva(2009A)","doi-asserted-by":"crossref","first-page":"565","DOI":"10.1016\/j.ic.2008.11.008","volume":"208","author":"P. Oliva","year":"2010","journal-title":"Information and Computation"},{"key":"10.2168\/LMCS-7(1:9)2011_dePaiva(1989A)","doi-asserted-by":"crossref","unstructured":"V. C. V. de Paiva. The Dialectica categories. In J. W. Gray and A. Scedrov, editors,Proc. of Categories in Computer Science and Logic, Boulder, CO, 1987, pages 47-62. Contemporary Mathematics, vol 92, American Mathematical Society, 1989.","DOI":"10.1090\/conm\/092\/1003194"},{"key":"10.2168\/LMCS-7(1:9)2011_dePaiva(1989B)","unstructured":"V. C. V. de Paiva. A Dialectica-like model of linear logic. In D. Pitt, D. Rydeheard, P. Dybjer, A. Pitts, and A. Poign\u00e9, editors,Category Theory and Computer Science, Manchester, UK, pages 341-356. Springer-Verlag LNCS 389, 1989."},{"key":"10.2168\/LMCS-7(1:9)2011_dePaiva(1991)","unstructured":"V. C. V. de Paiva. The Dialectica categories. Technical Report 213, Computer Laboratory, University of Cambridge, Jan 1991."},{"issue":"4","key":"10.2168\/LMCS-7(1:9)2011_Schellinx(1991)","doi-asserted-by":"crossref","first-page":"537","DOI":"10.1093\/logcom\/1.4.537","volume":"1","author":"H. Schellinx","year":"1991","journal-title":"Journal of Logic and Computation"},{"key":"10.2168\/LMCS-7(1:9)2011_Troelstra(73)","doi-asserted-by":"crossref","unstructured":"A. S. Troelstra.Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, volume 344 ofLecture Notes in Mathematics. Springer, Berlin, 1973.","DOI":"10.1007\/BFb0066739"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1110\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1110\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:03:45Z","timestamp":1681243425000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1110"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3,27]]},"references-count":18,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(1:9)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1012.1174","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1012.1174","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2011,3,27]]},"article-number":"1110"}}