Linearizing Intuitionistic Implication

• To: types
• Subject: Linearizing Intuitionistic Implication
• From: andre@saul.cis.upenn.edu (Andre Scedrov)
• Date: Thu, 05 Mar 92 11:49:06 EST
• Sender: meyer@theory.lcs.mit.edu

Date: Wed, 4 Mar 92 16:10:23 EST
To: linear@cs.stanford.edu

                  Linearizing Intuitionistic Implication 

                  P. Lincoln, A. Scedrov, and N. Shankar  


Abstract: An embedding of the implicational propositional intuitionistic
logic (IIL) into the nonmodal fragment of intuitionistic linear logic (IMALL) 
is given.  The embedding preserves cut-free proofs in a proof system that is 
a variant of IIL.  The embedding is efficient and provides an alternative 
proof of the PSPACE-hardness of IMALL.  It exploits several proof-theoretic 
properties of intuitionistic implication that analyze the use of resources 
in IIL proofs.  A preliminary version of this work was reported in LICS '91. 


A dvi file of the full paper is available by anonymous ftp by using the 
following dialogue: 


    % ftp ftp.cis.upenn.edu
    Name: anonymous
    Password:  [[enter your email address]]
    ftp> cd pub
    ftp> binary
    ftp> get lss91.dvi
    ftp> quit

• Prev: Notations for abstraction and product formation
• Next: Paper for ftp
• Index(es):
  • Main
  • Thread