{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T12:02:35Z","timestamp":1759147355461,"version":"3.37.3"},"reference-count":19,"publisher":"Wiley","issue":"6","license":[{"start":{"date-parts":[[2010,11,9]],"date-time":"2010-11-09T00:00:00Z","timestamp":1289260800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"funder":[{"name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","award":["SFRH\/BD\/36358\/2007"],"award-info":[{"award-number":["SFRH\/BD\/36358\/2007"]}]},{"DOI":"10.13039\/501100000288","name":"Royal Society","doi-asserted-by":"crossref","award":["516002.K501\/RH\/kk"],"award-info":[{"award-number":["516002.K501\/RH\/kk"]}],"id":[{"id":"10.13039\/501100000288","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mathematical Logic Qtrly"],"published-print":{"date-parts":[[2010,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This article systematically investigates so\u2010called \u201ctruth variants\u201d of several functional interpretations. We start by showing a close relation between two variants of modified realizability, namely modified realizability with truth and q\u2010modified realizability. Both variants are shown tobe derived from a single \u201cfunctional interpretation with truth\u201d of intuitionistic linear logic. This analysis suggests that several functional interpretations have truth and q\u2010variants. These variants, however, require a more involved modification than the ones previously considered. Following this lead we present truth and q\u2010variants of the Diller\u2010Nahm interpretation, the bounded modified realizability and the bounded functional interpretation (\u00a9 2010 WILEY\u2010VCH Verlag GmbH &amp; Co. KGaA, Weinheim)<\/jats:p>","DOI":"10.1002\/malq.200910112","type":"journal-article","created":{"date-parts":[[2010,11,9]],"date-time":"2010-11-09T08:34:48Z","timestamp":1289291688000},"page":"591-610","source":"Crossref","is-referenced-by-count":3,"title":["Proof interpretations with truth"],"prefix":"10.1002","volume":"56","author":[{"given":"Jaime","family":"Gaspar","sequence":"first","affiliation":[]},{"given":"Paulo","family":"Oliva","sequence":"additional","affiliation":[]}],"member":"311","published-online":{"date-parts":[[2010,11,9]]},"reference":[{"key":"e_1_2_1_2_2","doi-asserted-by":"crossref","unstructured":"J.Avigad andS.Feferman G\u00f6del's functional (\u201cDialectica\u201d) interpretation. In: Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics volume 137 (S. R. Buss ed.) pp. 337\u2013405 (Elsevier 1998).","DOI":"10.1016\/S0049-237X(98)80020-7"},{"key":"e_1_2_1_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02025118"},{"key":"e_1_2_1_4_2","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1140641178"},{"key":"e_1_2_1_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2004.11.001"},{"key":"e_1_2_1_6_2","doi-asserted-by":"crossref","unstructured":"G.Ferreira andP.Oliva Functional interpretations of intuitionistic linear logic. In: Proceedings of CSL volume 5771 of LNCS (E. Gr\u00e4del and R. Kahle eds.) pp. 3\u201319 (Springer 2009).","DOI":"10.1007\/978-3-642-04027-6_3"},{"key":"e_1_2_1_7_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_1_8_2","unstructured":"R. J.Grayson Derived rules obtained by a model\u2010theoretic approach to realisability. Handwritten notes from M\u00fcnster University (1981)."},{"key":"e_1_2_1_9_2","doi-asserted-by":"crossref","unstructured":"M.\u2010D.Hernest andP.Oliva Hybrid functional interpretations. Proceedings of CiE LNCS 5028 pp. 251\u2013260 (2008).","DOI":"10.1007\/978-3-540-69407-6_29"},{"key":"e_1_2_1_10_2","unstructured":"K. F.J\u00f8rgensen Finite type arithmetic: Computable existence analysed by modified realisability and functional interpretation. Master's Thesis University of Roskilde (2001)."},{"key":"e_1_2_1_11_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.200410004"},{"key":"e_1_2_1_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01794980"},{"key":"e_1_2_1_13_2","doi-asserted-by":"publisher","DOI":"10.2307\/2586648"},{"key":"e_1_2_1_14_2","unstructured":"U.Kohlenbach Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Monographs in Mathematics (Springer 2008)."},{"key":"e_1_2_1_15_2","doi-asserted-by":"crossref","unstructured":"P.Oliva Computational interpretations of classical linear logic. In: Proceedings of WoLLIC'07 LNCS 4576 pp. 285\u2013296 (Springer 2007).","DOI":"10.1007\/978-3-540-73445-1_20"},{"key":"e_1_2_1_16_2","doi-asserted-by":"crossref","unstructured":"P.Oliva Modified realizability interpretation of classical linear logic. In: Proc. of the Twenty Second Annual IEEE Symposium on Logic in Computer Science LICS'07 pp. 431\u2013440 (IEEE Press 2007).","DOI":"10.1109\/LICS.2007.32"},{"key":"e_1_2_1_17_2","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.2008.01135.x"},{"key":"e_1_2_1_18_2","unstructured":"P.Oliva Hybrid functional interpretations of linear and intuitinistic logic. To appear in: J. Logic Computation."},{"key":"e_1_2_1_19_2","doi-asserted-by":"crossref","unstructured":"A. S.Troelstra Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics volume 344 (Springer 1973).","DOI":"10.1007\/BFb0066739"},{"key":"e_1_2_1_20_2","unstructured":"A. S.Troelstra andD.van Dalen Constructivism in Mathematics. An Introduction. Studies in Logic and the Foundations of Mathematics volume 121 (North Holland 1988)."}],"container-title":["Mathematical Logic Quarterly"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.200910112","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.200910112","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/malq.200910112","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,13]],"date-time":"2023-11-13T18:04:57Z","timestamp":1699898697000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/malq.200910112"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,11,9]]},"references-count":19,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2010,12]]}},"alternative-id":["10.1002\/malq.200910112"],"URL":"https:\/\/doi.org\/10.1002\/malq.200910112","archive":["Portico"],"relation":{},"ISSN":["0942-5616","1521-3870"],"issn-type":[{"type":"print","value":"0942-5616"},{"type":"electronic","value":"1521-3870"}],"subject":[],"published":{"date-parts":[[2010,11,9]]}}}