2 Mar 1992 22:09

### Italian Workshop in Siena: a disclaimer

Date: Mon, 2 Mar 92 11:05:40 GMT
To: linear@...

In the report of the "Informal Workshop of Italian researchers in
Linear Logic", a title for my talk is given by the coordinators
which credits me with a general theory of "formulas with polarities":

> 10) Gianluigi Bellin   (Edimburgh)
>     "On formulas with polarities"

In Siena I briefly (25 minutes) sketched the motivations for my work
on "Proof Nets for Classical Logic LC", which is simply a solution
of the combinatorial problem proposed in section 1.5, i) of the preprint
by J-Y. Girard "A new constructive logic: classical logic". An abstract
of the result was posted in "linear@..." on Dec 11, 1991.

Gianluigi Bellin

PS: I take the occasion to suggest that linear logicians of all nationalities
and ancestral backgrounds should take the opportunity of attending the
second informal workshop -- if it is held in Siena -- and appreciate the
artistic treasures, the well-preserved environment, and the communal
spirit of that town.


5 Mar 1992 17:46

### Notations for abstraction and product formation

Date: Thu, 5 Mar 92 10:57:38 EST

type-labeled lambda-abstraction, abstraction terms of the form
lambda x:X.Y were, in fact, introduced by de Bruijn.  (Jon Seldin
gets the palm here --- he located this form of abstraction in an
old technical report written by de Bruijn, and nobody has come up with
question with Mike Beeson, Roger Hindley, and Phil Scott.)

Does anybody know where the related notation for products, Pi x:X.Y,
originated?  Martin-Lof has been using (essentially) this notation
for a long time in his work on constructive type theory, but perhaps
it comes from AUTOMATH, too.

Garrel Pottinger
garrel@...


5 Mar 1992 17:49

### Linearizing Intuitionistic Implication

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

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
ftp> cd pub
ftp> binary
ftp> get lss91.dvi
ftp> quit


9 Mar 1992 03:30

### Paper for ftp

To: linear@...
Date: Fri, 06 Mar 92 09:14:07 -0500

Some people has asked for the paper referred to in my paper
"Constraints, channels, and the flow of information." The older paper,
"Information links in domain theory" shows how the notion of
information link can be seen as a generalization of the notions of
continuous function and approx mapping, in domain theory, and also
observes that the same holds for stable function on coherence spaces.
This paper is now on phil.indiana.edu for ftp. It is on /ftp/pub as
Barwise-mfps.tex. A dvi version is also available there.  If you want
a hard copy, write meboyle@...  Jon


19 Mar 1992 00:05

### material for anonymous ftp

Date: Wed, 18 Mar 92 18:03:43 EST

I am making a selection of papers and notes in LATEX format, LATEX macros for
drawing diagrams and various cateory-theoretic notations, and a cumulative
bibliography in BIBTEX format available for anonymous ftp.  The papers and
notes are:

"The Coherence of Languages with Intersection Types"

"Preliminary Design of the Programming Language Forsythe"

"Replacing Complexity with Generality: The Programming Language Forsythe"

"Even Normal Forms Can be Hard to Type"

"Types, Abstraction, and Parametric Polymorphism, Part 2"
(with Ma QingMing)

"Syntactic Control of Interference, Part 2"

"On Functors Expressible in the Polymorphic Typed Lambda Calculus"
(with Gordon D. Plotkin)

"Introduction to the Polymorphic Lambda Calculus"

"Semantics as a Design Tool" (class notes)

To access this material, do ftp e.ergo.cs.cmu.edu, with the username as



23 Mar 1992 19:24

### proof nets for classical MLL and linear lambda terms (401 lines)

Date: Sat, 21 Mar 92 18:31:05 GMT
To: linear@...

Every proof net for classical multiplicative linear logic (CMLL)
represents an equivalence class of linear lambda terms,
which are built also with a constructor tensor' and its dual let'.

In fact, each Danos-Regnier switching on a proof net determines
such a lambda term, hence a natural deduction [or sequent] derivation
in intuitionistic multiplicative linear logic (IMLL).

This property clarifies the difference between Danos and Regnier'
correctness conditions for proof nets (The structure of multiplicatives,
Arch. for Math. Log. 28, 1989) and the others, e.g., by Ketonen and myself.

The above remark results from conversations with Jacques van de Wiele.
Thanks to Jacques and Laurent Regnier for their stimulating visit to Edinburgh.

Gianluigi Bellin
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%this is TeX, not LaTeX%%%%%%%%%%%%%%%%
\magnification = \magstep1
\raggedbottom
\def\phbl0{\vrule height .5ex width .0ex}               %%thin phantom box
\def\bull{\vrule height 1.3ex width 1.0ex depth -.1ex } %%black box
\def\limp{\mathrel{-\!\circ}}
\def\bang{\hbox{\bf !}}
\def\whynot{\hbox{\bf ?}}

V.~Danos, L.~Regnier and J.~van~de~Wiele, among others, have given representations


23 Mar 1992 20:41

### mkilian@...

Return-Path: <mkilian@...>
Date: Fri, 20 Mar 92 14:40:16 EST
From: mkilian@...
To: colloquium
Subject: Kim Bruce to visit on April 16th.

Professor Kim Bruce of Williams College will be visiting on April 16th
to present a colloquium on a formal model of an object-oriented
programming language.  If you are interested in meeting with Professor
Bruce, please let me know as soon as possible.

Thanks,

Michael Kilian
mkilian@...


25 Mar 1992 20:20

### Re: Proof Nets and Lambda Terms

Date: Wed, 25 Mar 92 13:08:10 EST
To: linear@...

This is in regards to G. Bellin's recent note on proof nets and
equivalence classes of linear lambda terms. I believe that my recent
work relating proof nets and coherence is relevant to his result.

The question of coherence arose originally in algebraic topology.
Basically, coherence amounts to determining which diagrams commute in
categories with certain additional structure. Typically, this
structure is a tensor product and implication (as in intuitionistic linear
logic), or a tensor product and a dualizing functor (as in classical
linear logic). Examples of such categories are numerous in algebraic
topology and homological algebra.

It was the fundamental observation of J. Lambek that logical
principles could be used to approach this problem. The idea is to view
the morphisms which comprise the diagram as deductions in a deductive
system, under a process analogous to the Curry-Howard isomorphism.
Then coherence reduces to determining the equivalence relation of the
corresponding deductive system. Given this interpretation, logical
methods, most notably cut-elimination, can be put to use. This
approach has yielded a great many results. (Please see the references
in my paper.)

Since multiplicative linear logic can be viewed as a logic about
tensor categories, it was hoped that proof nets could be used to
provide better coherence results. There is a straightforward
translation procedure, which assigns a proof net to a morphism in an
autonomous (tensor, implication) or *-autonomous (tensor, duality) category.


29 Mar 1992 04:55

### TLCA'93 Call for Papers

Date: Fri, 27 Mar 1992 15:25:53 GMT

latex file with the first announcement and call for
papers for TLCA'93 - International Conference on Typed Lambda Calculi and
Applications, to be held in Utrecht, The Netherlands, March 16-18 1993.

\documentstyle{article}

\parindent 0cm
\pagestyle{empty}
\textwidth 18cm
\textheight 28cm
\topmargin -2.5cm
\oddsidemargin -1.2cm
\evensidemargin 0cm

\begin{document}
\begin{center}
{\LARGE First Announcement and Call for Papers}
\end{center}
\smallskip

\begin{center}
{\Huge  International Conference on}
\end{center}
\begin{center}
{\Huge Typed Lambda Calculi and Applications}
\end{center}
\begin{center}
{\Huge TLCA}