Questions on LU and ITT

To: linear@cs.stanford.edu
Subject: Questions on LU and ITT
From: Sanjiva Prasad <sanjiva@ecrc.de>
Date: Thu, 13 May 93 11:39:40 +0200
Approved: types@dcs.gla.ac.uk



(This message was earlier posted to the logic mailing 
 list, but no responses were received.)

I seem to have evermore questions as I learn more about proof theory, linear
logic and LU.

1.  Has a sequent presentation of Martin-Lo"f Intuitionistic Type Theory been
    published?

2.  The next pair of questions are about the Intuitionistic fragments of LU
    and their relation to the traditional sequent calculi for Intuitionistic 
    logic.

    From my undersanding of Girard's paper on LU, the translation of the 
    intuitionistic fragments of LU into the traditional sequent calculi for
    intuitionistic logic are straightforward, but the other way things may
    be more delicate.  Has someone proven a result showing that cut-free
    (resp. not necessarily cut free) intuitionistic proofs translate into
    cut-free (resp. not necessarily cut free) proofs within the intuitionistic 
    fragment of LU (i.e. with sequents maintaining the specified restrictions
    at each stage in the proof).
  
 I would appreciate any information on the connections between LU's
 intuitionistic fragment and usual calculi for intuitionistic logic.

Thanks,
Sanjiva					(sanjiva@ecrc.de)


Sanjiva Prasad,  Guest Magus				E-mail: sanjiva@ecrc.de
European Computer Industry Research Centre		Off: +49 89 92 69 91 58
Arabellastrasse 17					Fax: +49 89 92 69 91 70
8000 Muenchen 81, Germany				Res: +49 89 16 33 59