[Prev][Next][Index][Thread]

Other references on linear logic and proof nets



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