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) Proof-theoretic aspects of linear logic and other substructural logics (03F52) Relative consistency and interpretations (03F25) Functionals in proof theory (03F10)

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

• scientific article; zbMATH DE number 1215497 (Why is no real title available?)
• scientific article; zbMATH DE number 3216998 (Why is no real title available?)
• Computational Interpretations of Classical Linear Logic
• Eine Variante zur Dialectica-Interpretation der Heyting-Arithmetik endlicher Typen
• Functional interpretations of linear and intuitionistic logic
• 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

(13)

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

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)