Other references on linear logic and proof nets

• To: types
• Subject: Other references on linear logic and proof nets
• From: Jean Gallier <jean@saul.cis.upenn.edu>
• Date: Mon, 02 Dec 91 17:21:49 EST
• Sender: meyer@theory.lcs.mit.edu

Date: Mon, 02 Dec 91 10:18:24 EST
To: linear@cs.stanford.edu

Dear Pat, in view of previous messages, I would like to point out
that I give a proof of sequentialization for multiplicative proof nets in 

Constructive Logic Part II: Linear Logic and Proof nets.
University of Pennsylvania, CIS Dept.
tech. Report MS-CIS-91-75 (1991).
This is an update of  Digital PRL Report No 9.

The proof in the PRL report had a faulty lemma which is corrected
in the Penn Tech report. The proof does NOT explicitly use empires,
but I have since realized that for the quantifier case, some form of
empire is necessary.

I also discuss quite extensively phase semantics and quantales
(but under the name Girard structures ...!!!).

Part I is the report:

Constructive Logic Part I: A tutorial on proof systems and typed
lambda-calculi. 

University of Pennsylvania, CIS Dept.
tech Report MS-CIS-91-74 (1991).
This is the same as  Digital PRL Report No 8.

-- Jean

• Prev: Re: chains, etc & announcement on intuitionistic Tarski theorem
• Next: ordinals and Tarski's theorem
• Index(es):
  • Main
  • Thread