Hostname: page-component-6bf8c574d5-w79xw Total loading time: 0 Render date: 2025-02-22T12:09:29.880Z Has data issue: false hasContentIssue false

Subnets of proof-nets in multiplicative linear logic with MIX

Published online by Cambridge University Press:  01 December 1997

GIANLUIGI BELLIN
Affiliation:
Equipe de Logique Mathématique, Université de Paris 7 Denis Diderot, CNRS (URA 753) - UFR de Mathématiques, 2 Place Jussieu - Case 7012, 75251 Paris Cedex 05 (France)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

This paper studies the properties of the subnets of a proof-net for first-order Multiplicative Linear Logic without propositional constants (MLL), extended with the rule of Mix: from [vdash ]Γ and [vdash ]Δ infer [vdash ]Γ, Δ. Asperti's correctness criterion and its interpretation in terms of concurrent processes are extended to the first-order case. The notions of kingdom and empire of a formula are extended from MLL to MLL+MIX. A new proof of the sequentialization theorem is given. As a corollary, a system of proof-nets is given for De Paiva and Hyland's Full Intuitionistic Linear Logic with Mix; this result gives a general method for translating Abramsky-style term assignments into proof-nets, and vice versa.

Type
Research Article
Copyright
1997 Cambridge University Press