Switch to: References

Citations of:

A new deconstructive logic: Linear logic

Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx

Journal of Symbolic Logic 62 (3):755-807 (1997)

Add citations

You must login to add citations.

Call-by-name reduction and cut-elimination in classical logic.Kentaro Kikuchi - 2008 - Annals of Pure and Applied Logic 153 (1-3):38-65.details We present a version of Herbelin’s image-calculus in the call-by-name setting to study the precise correspondence between normalization and cut-elimination in classical logic. Our translation of λμ-terms into a set of terms in the calculus does not involve any administrative redexes, in particular η-expansion on μ-abstraction. The isomorphism preserves β,μ-reduction, which is simulated by a local-step cut-elimination procedure in the typed case, where the reduction system strictly follows the “ cut=redex” paradigm. We show that the underlying untyped calculus is confluent (...) Download Export citation Bookmark 4 citations
A focused approach to combining logics.Chuck Liang & Dale Miller - 2011 - Annals of Pure and Applied Logic 162 (9):679-697.details We present a compact sequent calculus LKU for classical logic organized around the concept of polarization. Focused sequent calculi for classical, intuitionistic, and multiplicative–additive linear logics are derived as fragments of the host system by varying the sensitivity of specialized structural rules to polarity information. We identify a general set of criteria under which cut-elimination holds in such fragments. From cut-elimination we derive a unified proof of the completeness of focusing. Furthermore, each sublogic can interact with other fragments through cut. (...) Download Export citation Bookmark 3 citations
Polarized games.Olivier Laurent - 2004 - Annals of Pure and Applied Logic 130 (1-3):79-123.details We generalize the intuitionistic Hyland–Ong games to a notion of polarized games allowing games with plays starting by proponent moves. The usual constructions on games are adjusted to fit this setting yielding game models for both Intuitionistic Linear Logic and Polarized Linear Logic. We prove a definability result for this polarized model and this gives complete game models for various classical systems: , λμ-calculus, … for both call-by-name and call-by-value evaluations. Download Export citation Bookmark 3 citations
On the unity of duality.Noam Zeilberger - 2008 - Annals of Pure and Applied Logic 153 (1-3):66-96.details Most type systems are agnostic regarding the evaluation strategy for the underlying languages, with the value restriction for ML which is absent in Haskell as a notable exception. As type systems become more precise, however, detailed properties of the operational semantics may become visible because properties captured by the types may be sound under one strategy but not the other. For example, intersection types distinguish between call-by-name and call-by-value functions, because the subtyping law ∩≤A→ is unsound for the latter in (...) Download Export citation Bookmark 2 citations
Polarized and focalized linear and classical proofs.Olivier Laurent, Myriam Quatrini & Lorenzo Tortora de Falco - 2005 - Annals of Pure and Applied Logic 134 (2):217-264.details We give the precise correspondence between polarized linear logic and polarized classical logic. The properties of focalization and reversion of linear proofs are at the heart of our analysis: we show that the tq-protocol of normalization for the classical systems and perfectly fits normalization of polarized proof-nets. Some more semantical considerations allow us to recover LC as a refinement of multiplicative. Download Export citation Bookmark 2 citations
The additive multiboxes.Lorenzo Tortora de Falco - 2003 - Annals of Pure and Applied Logic 120 (1-3):65-102.details We introduce the new notion of additive “multibox” for linear logic proof-nets. Thanks to this notion, we define a cut-elimination procedure which associates with every proof-net of multiplicative and additive linear logic a unique cut-free one. Download Export citation Bookmark 2 citations
On the linear decoration of intuitionistic derivations.Vincent Danos, Jean-Baptiste Joinet & Harold Schellinx - 1995 - Archive for Mathematical Logic 33 (6):387-412.details We define an optimal proof-by-proof embedding of intuitionistic sequent calculus into linear logic and analyse the (purely logical) linearity information thus obtained. Download Export citation Bookmark 1 citation
On the form of witness terms.Stefan Hetzl - 2010 - Archive for Mathematical Logic 49 (5):529-554.details We investigate the development of terms during cut-elimination in first-order logic and Peano arithmetic for proofs of existential formulas. The form of witness terms in cut-free proofs is characterized in terms of structured combinations of basic substitutions. Based on this result, a regular tree grammar computing witness terms is given and a class of proofs is shown to have only elementary cut-elimination. Download Export citation Bookmark
Advances in Natural Deduction: A Celebration of Dag Prawitz's Work.Luiz Carlos Pereira & Edward Hermann Haeusler (eds.) - 2012 - Dordrecht, Netherland: Springer.details This collection of papers, celebrating the contributions of Swedish logician Dag Prawitz to Proof Theory, has been assembled from those presented at the Natural Deduction conference organized in Rio de Janeiro to honour his seminal research. Dag Prawitz’s work forms the basis of intuitionistic type theory and his inversion principle constitutes the foundation of most modern accounts of proof-theoretic semantics in Logic, Linguistics and Theoretical Computer Science. The range of contributions includes material on the extension of natural deduction with higher-order (...) Download Export citation Bookmark

1