headers
Gianluigi Bellin | 2 Mar 1992 22:09
Picon

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.
Permalink | Reply | 0 comments |
headers
garrel | 5 Mar 1992 17:46

Notations for abstraction and product formation

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

According to the information received in reply to my earlier query about
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
an earlier reference.  I also had helpful correspondence about the
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@...
Permalink | Reply | 0 comments |
headers
Andre Scedrov | 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
    Password:  [[enter your email address]]
    ftp> cd pub
    ftp> binary
    ftp> get lss91.dvi
    ftp> quit
Permalink | Reply | 0 comments |
headers
Jon Barwise | 9 Mar 1992 03:30
Picon
Picon
Picon

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
Permalink | Reply | 0 comments |
headers
John_Reynolds | 19 Mar 1992 00:05
Picon

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
"anonymous" and your usual user <at> machine name as a password.
(Continue reading)

Permalink | Reply | 0 comments |
headers
glb | 23 Mar 1992 19:24
Picon

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
(Continue reading)

Permalink | Reply | 1 comment |
headers
Albert R. Meyer | 23 Mar 1992 20:41
Picon

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@...
Permalink | Reply | 0 comments |
headers
Richard Blute | 25 Mar 1992 20:20
Picon

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.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Frans.Snijders | 29 Mar 1992 04:55
Picon
Picon
Favicon

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}
(Continue reading)

Permalink | Reply | 0 comments |

Gmane