A Mixed λ-calculus

Studia Logica 87 (2-3):269-294 (2007)
  Copy   BIBTEX

Abstract

The aim of this paper is to define a λ-calculus typed in aMixed (commutative and non-commutative) Intuitionistic Linear Logic. The terms of such a calculus are the labelling of proofs of a linear intuitionistic mixed natural deduction NILL, which is based on the non-commutative linear multiplicative sequent calculus MNL [RuetAbrusci 99]. This linear λ-calculus involves three linear arrows: two directional arrows and a nondirectional one (the usual linear arrow). Moreover, the -terms are provided with seriesparallel orders on free variables. We prove a normalization theorem which explicitly gives the behaviour of the order during the normalization procedure.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,616

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Propositional Mixed Logic: Its Syntax and Semantics.Karim Nour & Abir Nour - 2003 - Journal of Applied Non-Classical Logics 13 (3-4):377-390.
λμ-calculus and Böhm's theorem.René David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
Intrinsically mixed states: an appreciation.Laura Ruetsche - 2004 - Studies in History and Philosophy of Science Part B: Studies in History and Philosophy of Modern Physics 35 (2):221-239.
$lambdamu$-Calculus and Bohm's Theorem.Rene David & Walter Py - 2001 - Journal of Symbolic Logic 66 (1):407-413.
The Situation Calculus: A Case for Modal Logic. [REVIEW]Gerhard Lakemeyer - 2010 - Journal of Logic, Language and Information 19 (4):431-450.
Valuation Semantics for Intuitionic Propositional Calculus and some of its Subcalculi.Andréa Loparić - 2010 - Principia: An International Journal of Epistemology 14 (1):125-33.
Causes and mixed probabilities.David Papineau - 1990 - International Studies in the Philosophy of Science 4 (1):79 – 88.

Analytics

Added to PP
2009-01-28

Downloads
26 (#524,588)

6 months
3 (#447,120)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Myriam Quatrini
Aix-Marseille University

Citations of this work

No citations found.

Add more citations

References found in this work

Non-commutative logic I: the multiplicative fragment.V. Michele Abrusci & Paul Ruet - 1999 - Annals of Pure and Applied Logic 101 (1):29-64.
Lambda Grammars and the Syntax-Semantics Interface.Reinhard Muskens - 2001 - In Robert Van Rooij & Martin Stokhof (eds.), Proceedings of the Thirteenth Amsterdam Colloquium. Amsterdam: ILLC. pp. 150-155.
The logic of types.Wojciech Buszkowski - 1987 - In Jan T. J. Srzednicki (ed.), Initiatives in Logic. M. Nijhoff. pp. 180--206.

Add more references