1 Sep 1992 16:51

### Paper available by ftp

Date: Mon, 31 Aug 92 16:38:50 EDT

First Order Linear Logic Without Modalities is NEXPTIME-Hard

P. Lincoln  and  A. Scedrov

ABSTRACT: In this paper the decision problem is studied for the
multiplicative-additive fragment of linear logic with first order
quantifiers. This fragment is shown to be NEXPTIME-hard. The hardness
proof combines Shapiro's logic programming simulation of nondeterministic
Turing machines with the standard proof of the PSPACE-hardness of
quantified boolean formula validity, utilizing some of the surprisingly
powerful and expressive machinery of linear logic. In contrast to
previous work on linear logic proof search as a computational paradigm,
in which a computation proceeds upwards'' along a proof tree, here the
computation steps are applied horizontally across'' the leaves of a
proof tree.

This paper can be retrieved by anonymous ftp using the instructions below.
If you would like a copy but cannot use ftp to this site, please send me your

% ftp ftp.cis.upenn.edu
Name: anonymous
ftp> cd pub/papers/scedrov
ftp> binary
ftp> get mall1.dvi
ftp> quit



2 Sep 1992 17:49

### paper available by FTP

Date: Tue, 1 Sep 92 10:14:03 -0700
To: linear@...

Constant-Only Multiplicative Linear Logic is NP-Complete
P. Lincoln  and  T. Winkler

This paper explores the decision problem for
multiplicative linear logic without propositions.  The
fragment is shown to be NP-Complete.  Reduction from
3-Partition is used to demonstrate hardness, while
the obvious "guess and check entire proof" procedure
shows that this decision problem is in NP.  This result
lends evidence that the linear circuit evaluation problem
(testing validity of expressions in AND, OR, TRUE, and FALSE
in multiplicative linear logic) is intractable.  This paper
is based on work by the authors and N. Shankar, as well as
earlier work by Girard and others.

% ftp ftp.csl.sri.com
Name: anonymous
ftp> cd pub/lincoln
ftp> binary
ftp> get comult-npc.dvi
ftp> quit


2 Sep 1992 17:58

### Category Theory and Computer Science, Sep. 7-10, '93, Amsterdam

Date: Wed, 2 Sep 92 15:46:47 BST

1993
********* Preliminary Announcement ***********
*                                            *
*    CATEGORY THEORY AND COMPUTER SCIENCE    *
*    ------------------------------------    *
*                                            *
*          Fifth Biennial Meeting            *
*                                            *
**********************************************

CTCS-5

Dates: 7th-10th September 1993.
Venue: CWI, Amsterdam, The Netherlands.

The fifth of the biennial conferences on category theory and computer science
is to be held in Amsterdam in 1993.

The purpose of the conference series is the advancement of the foundations of
computing using the tools of category theory, algebra, geometry and logic.
Whilst the emphasis is upon applications of category theory, it is recognised
that the area is highly interdisciplinary and the organising committee welcomes
submissions in related areas. Topics central to the conference include:
*   The semantics of computation
*   Program logics and specification
*   Type theory and its semantics
*   Domain theory
*   Linear logic and its semantics


3 Sep 1992 21:07

### paper available by ftp

Date: Thu, 3 Sep 1992 14:13:30 +0100 (BST)

The following paper is now available by anonymous ftp from
theory.doc.ic.ac.uk, in papers/Abramsky. Anyone needing a hard copy
should send me their postal address.

--------

\documentstyle[11pt]{article}

\begin{document}
\bibliographystyle{alpha}
\title{Games and Full Completeness for Multiplicative Linear Logic}
Imperial College.}

\maketitle

\begin{abstract}
We present a game semantics for Linear Logic, in which formulas denote
games and proofs denote winning strategies.  We show that our semantics
yields a categorical model of Linear Logic and prove  {\em full
completeness} for Multiplicative Linear Logic with the MIX rule: every
winning strategy is the denotation of a unique cut-free proof net.  A key
role is played by the notion of {\em history-free} strategy; strong connections
are made between history-free strategies and the Geometry of Interaction.
Our semantics incorporates a natural notion of polarity, leading to a
refined treatment of the additives.  We make comparisons with related work
by Joyal, Blass {\it et al}.
\end{abstract}


7 Sep 1992 07:09

### Map theory

Date: Sun, 6 Sep 92 09:40:36 +0200

MAP THEORY

An index/glossary is now available by anonymous ftp
for the following paper:

Klaus Grue: Map theory,
Theoretical Computer Science 102 (1992) 1-133
Elsevier

Map theory is a foundation of mathematics based on lambda-
calculus instead of logic and sets, and thereby fulfills
Church's original aim of introducing lambda-calculus. Map
theory can do anything ZFC set theory can do. In particular,
all of classical mathematics is contained in map theory.
In addition, and contrary to set theory, map theory has
unlimited abstraction and contains a computer programming
language as a natural subset. Map theory is as simple and
homogeneous as ZFC set theory. The paper presents map theory,
develops ZFC within map theory and gives a relative
consistency proof for map theory.

The index is available in LaTeX format by anonymous ftp
>from the University of Copenhagen. Instructions:

* Connect to host ftp.diku.dk [129.142.96.1]
* go to directory /pub/diku/users/grue
* "get" the file "mapindex.tex" from that directory


8 Sep 1992 02:59

### Re: Map theory

Date: 07 Sep 92 09:52:01 PDT (Mon)

From: Klaus Grue <grue@...>
Date: Sun, 6 Sep 92 09:40:36 +0200
...
In addition, and contrary to set theory, map theory has
unlimited abstraction and contains a computer programming
language as a natural subset.

Presumably these terms must be defined carefully in order to prevent
SETL from being a "natural subset" of set theory.

Vaughan Pratt


8 Sep 1992 21:50

Return-Path: <grue@...>
Date: Tue, 8 Sep 92 15:54:52 +0200

...
In addition, and contrary to set theory, map theory has
unlimited abstraction and contains a computer programming
language as a natural subset.

Klaus Grue

Presumably these terms must be defined carefully in order to prevent
SETL from being a "natural subset" of set theory.

Vaughan Pratt

Here is a more complete (and longer) description:

Map theory has six basic concepts: Functional application,
lambda abstraction, if-then-else, a single atom T, Hilbert's
epsilon operator (also known as the choice operator) and a
'well-foundedness' predicate. Omitting Hilbert's epsilon
operator and the well-foundedness predicate yields a Turing
complete computer programming language.

On the contrary, ZFC has four basic concepts: Membership, negation,
implication and universal quantification. No subset of these
concepts form a Turing complete computer programming language.

ZFC has limited abstraction in that {x|p(x)} merely is guaranteed
to exist if x is restricted to some set.


8 Sep 1992 23:34

### Re: 2 questions re: mapping from IL to ILL

To: linear@...
Date: 01 Sep 92 22:46:48 PDT (Tue)
Received: from Ghoti.Stanford.EDU by theory.lcs.mit.edu (5.65c/TOC-1.2S)
id AA06476; Tue, 08 Sep 92 17:23:42 EDT

>The first question concerns the mapping
>	| A -> B |   ==>   !| A | -o | B |
>I can't see why this isn't
>        | A -> B |   ==>   !( !| A | -o | B |)

Then it wouldn't follow that -> was intuitionistic implication.  In
particular you couldn't show A->(B->C) = (B&A)->C.  With the first
mapping this follows via
A->(B->C) = !A-o(!B-oC) = (!B <at> !A)-oC = !(B&A)-oC = (B&A)->C.
With your mapping you get stuck thus:
A->(B->C) = !(!A-o!(!B-oC)) = ?

(By A=B I mean constructive equivalence, i.e. isomorphism, of A and B
rather than their identity.  Nonconstructive equivalence would settle
for independent proofs of A|-B and B|-A, constructive equivalence adds
the further requirement that these proofs compose via cut to yield the
standard (identity) proofs of A|-A and B|-B.)

>or
>        | A -> B |   ==>   !| A | -o !| B |

Similar problem:
A->(B->C) = !A-o!(!B-o!C) = ?

>The second question concerns


9 Sep 1992 18:29

### quantum logics

Date: Wed, 9 Sep 92 09:55 BST
To: linear@...

Does anybody know anything about sequent calculi for quantum logics?
Thomas Forster


9 Sep 1992 18:31

### MFPS IX

Date: Tue, 8 Sep 92 17:03:55 EDT

Call for Papers

MFPS IX

The Ninth Conference on the
Mathematical Foundations of Programming Semantics

April 7 - 10, 1993
New Orleans, LA  USA

The Ninth Conference on the Mathematical Foundations of Programming
Semantics will be held at Tulane University, New Orleans, LA USA from
April 7 to April 10, 1993.  The conference will consist of six one-hour
invited talks and of talks selected from submissions.  There also will be
two Special Sessions.  The MFPS conferences are devoted to those areas of
mathematics, logic and computer science which are related to the semantics
of programming languages.  The series has particularly stressed providing a
forum where both mathematicians and computer scientists can meet and exchange
ideas about problems of common interest.  We also welcome submissions by
researchers in neighboring areas,'' since we have attempted to maintain some
breadth in the scope of the series.

The invited speakers for MFPS IX are:

Peter Aczel (Manchester)              Dale Miller (Pennsylvania)
Pierre-Louis Curien (LIENS-DMI)       Andrew Pitts (Cambridge)
Albert Meyer (MIT)                    Gordon Plotkin (Edinburgh)