Abstract
We present three functional interpretations of intuitionistic linear logic and show how these correspond to well-known functional interpretations of intuitionistic logic via embeddings of IL ω into ILL ω. The main difference from previous work of the second author is that in intuitionistic linear logic the interpretations of !A are simpler (at the cost of an asymmetric interpretation of pure ILL ω) and simultaneous quantifiers are no longer needed for the characterisation of the interpretations.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Avigad, J., Feferman, S.: Gödel’s functional (“Dialectica”) interpretation. In: Buss, S.R. (ed.) Handbook of proof theory. Studies in Logic and the Foundations of Mathematics, vol. 137, pp. 337–405. North Holland, Amsterdam (1998)
Diller, J., Nahm, W.: Eine Variant zur Dialectica-interpretation der Heyting Arithmetik endlicher Typen. Arch. Math. Logik Grundlagenforsch 16, 49–66 (1974)
Girard, J.-Y.: Linear logic. Theoretical Computer Science 50(1), 1–102 (1987)
Gödel, K.: Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12, 280–287 (1958)
Hyland, J.M.E.: Proof theory in the abstract. Annals of Pure and Applied Logic 114, 43–78 (2002)
Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. In: Heyting, A. (ed.) Constructivity in Mathematics, pp. 101–128. North Holland, Amsterdam (1959)
Oliva, P.: Computational interpretations of classical linear logic. In: Leivant, D., de Queiroz, R. (eds.) WoLLIC 2007. LNCS, vol. 4576, pp. 285–296. Springer, Heidelberg (2007)
Oliva, P.: Modified realizability interpretation of classical linear logic. In: Proc. of the Twenty Second Annual IEEE Symposium on Logic in Computer Science LICS 2007. IEEE Press, Los Alamitos (2007)
Oliva, P.: An analysis of Gödel’s dialectica interpretation via linear logic. Dialectica 62(2), 269–290 (2008)
Oliva, P.: Functional interpretations of linear and intuitionistic logic. Information and Computation (to appear, 2009)
de Paiva, V.C.V.: The Dialectica categories. In: Gray, J.W., Scedrov, A. (eds.) Proc. of Categories in Computer Science and Logic, Boulder, CO, 1987. Contemporary Mathematics, vol. 92, pp. 47–62. American Mathematical Society, Providence (1989)
de Paiva, V.C.V.: A Dialectica-like model of linear logic. In: Dybjer, P., Pitts, A.M., Pitt, D.H., Poigné, A., Rydeheard, D.E. (eds.) Category Theory and Computer Science. LNCS, vol. 389, pp. 341–356. Springer, Heidelberg (1989)
Troelstra, A.S.: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol. 344. Springer, Berlin (1973)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ferreira, G., Oliva, P. (2009). Functional Interpretations of Intuitionistic Linear Logic. In: Grädel, E., Kahle, R. (eds) Computer Science Logic. CSL 2009. Lecture Notes in Computer Science, vol 5771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04027-6_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-04027-6_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-04026-9
Online ISBN: 978-3-642-04027-6
eBook Packages: Computer ScienceComputer Science (R0)