The structure of exponentials: Uncovering the dynamics of linear logic proofs

Vincent Danos, Jean-Baptiste Joinet, Harold Schellinx

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We construct the exponential graph of a proof π in (second order) linear logic, an artefact displaying the interdependencies of exponentials in π. Within this graph superfluous exponentials are defined, the removal of which is shown to yield a correct proof π▹ with essentially the same set of reductions.

Applications to intuitionistic and classical proofs are given by means of reduction-preserving embeddings into linear logic.

The last part of the paper puts things the other way round, and defines families of linear logics in which exponential dependencies are ruled by a given graph. We sketch some work in progress and possible applications.
Original languageEnglish
Title of host publicationComputational Logic and Proof Theory
Subtitle of host publicationThird Kurt Gödel Colloquium, KGC'93 Brno, Czech Republic, August 24–27, 1993 Proceedings
EditorsGeorg Gottlob, Alexander Leitsch, Daniele Mundici
PublisherSpringer Berlin Heidelberg
Pages159-171
Number of pages13
Volume713
ISBN (Electronic)978-3-540-47943-7
ISBN (Print)978-3-540-57184-1
DOIs
Publication statusPublished - 1993

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume713

Fingerprint

Dive into the research topics of 'The structure of exponentials: Uncovering the dynamics of linear logic proofs'. Together they form a unique fingerprint.

Cite this