[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