Undecidability of second order linear logic without exponentials

A new preprint is now available by ftp anonymous on lmd.univ-mrs.fr in the  
directory /pub/lafont.


  Undecidability of second order linear logic without exponentials (7 pages)

Recently, Lincoln, Scedrov and Shankar showed that the multiplicative fragment  
of second order intuitionistic linear logic is undecidable, using a simple  
encoding of second order intuitionistic logic. Here we prove that the  
multiplicative-additive fragment of second order (classical) linear logic is  
also undecidable. For this, we use an encoding of two counter machines  
originally due to Kanovich together with an argument of phase semantics. 

I take this opportunity to mention another paper related to linear logic:


  From Proof-Nets to Interaction Nets (21 pages)
  [To appear in the proceedings of the Linear Logic Workshop (Cornell, 1993)]

If we consider the interpretation of proofs as programs, say in intuitionistic  
logic, the question of equality between proofs becomes crucial: The syntax  
introduces meaningless distinctions whereas the (denotational) semantics makes  
excessive identifications. This question does not have a simple answer in  
general, but it leads to the notion of proof-net, which is one of the main  
novelties of linear logic.

The notion of interaction net comes from an attempt to implement the reduction  
of these proof-nets. It happens to be a simple model of parallel computation,  
and so it can be presented independently of linear logic. However, we think  
that it is also useful to relate the exact origin of interaction nets,  
especially for readers with some knowledge in linear logic. We take this  
opportunity to give a survey of the theory of proof-nets, including a new proof  
of the sequentialization theorem.