Functional Interpretations of Intuitionistic Linear Logic

DOI10.1007/978-3-642-04027-6_3MaRDI QIDQ5902221zbMATH OpenOpenAlexFDO

Authors Gilda Ferreira, Paulo Oliva

Publication date 12 November 2009

Published in Computer Science Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1012.1174

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Structure of proofs (03F07) Functionals in proof theory (03F10) Relative consistency and interpretations (03F25) Proof-theoretic aspects of linear logic and other substructural logics (03F52)

Abstract: We present three different functional interpretations of intuitionistic linear logic ILL and show how these correspond to well-known functional interpretations of intuitionistic logic IL via embeddings of IL into ILL. The main difference from previous work of the second author is that in intuitionistic linear logic (as opposed to classical linear logic) the interpretations of !A are simpler and simultaneous quantifiers are no longer needed for the characterisation of the interpretations. We then compare our approach in developing these three proof interpretations with the one of de Paiva around the Dialectica category model of linear logic.

Recommendations

• Functional interpretations of intuitionistic linear logic
• Computational interpretations of linear logic
• Functional interpretations of linear and intuitionistic logic
• Hybrid functional interpretations of linear and intuitionistic logic
• Full intuitionistic linear logic

Cites work

• Computational Interpretations of Classical Linear Logic
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Functional interpretations of linear and intuitionistic logic
• scientific article; zbMATH DE number 1215497 (Why is no real title available?)
• scientific article; zbMATH DE number 3216998 (Why is no real title available?)
• Linear logic
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Proof theory in the abstract
• ÜBER EINE BISHER NOCH NICHT BENÜTZTE ERWEITERUNG DES FINITEN STANDPUNKTES

Cited in

(14)

• Linearizing intuitionistic implication
• Operational interpretations of linear logic
• Hybrid functional interpretations of linear and intuitionistic logic
• Proof interpretations with truth
• Hybrid Functional Interpretations
• Modeling linear logic with implicit functions
• On bounded functional interpretations
• Functional Interpretation of Logics for ‘Generally’
• Semantical observations on the embedding of Intuitionistic Logic into Intuitionistic Linear Logic
• THE CHARACTERIZATION OF WEIHRAUCH REDUCIBILITY IN SYSTEMS CONTAINING
• Around classical and intuitionistic linear logics
• Functional interpretations of intuitionistic linear logic
• Uniform functional interpretations
• Functional interpretations of linear and intuitionistic logic

This page was built for publication: Functional Interpretations of Intuitionistic Linear Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5902221)