2 May 00:09 1995

### Information relating to the AMAST newsletter

Dear Philip,

In view of the frequent (and most welcome!) relevance of contributions
from the forum you moderate to the AMAST newsletter, I would appreciate
it if you could distribute the enclosed information.
Thank you very much, in advance.
Regards,
Pippo

-----------------------------------------------------------------------

[Please accept my apologies if you receive this message more than once.
G. Scollo]

The AMAST newsletter (the acronym stands for Algebraic Methodology
And Software Technology, from the name of a related conference series),
called _AMAST Links_, was started last year as an experiment. This has
made quite good progress so far, and has now reached some sort of
and the related mailing list.
_AMAST Links_ is issued monthly and has two forms: plain-text and
hypertext. The plain-text form is distributed by e-mail, while both
forms are made available on the World-Wide Web (WWW) and by anonymous
FTP. In the hypertext form, links to more detailed information, or to
information otherwise related to the announcements, are included when
available.
If you wish to have a look at individual pages of the latest issue of
WWW, then please open either of the following:

2 May 23:51 1995

### Non-commutative MLL2 is undecidable

Undecidability of Non-Commutative Second Order Multiplicative
Linear Logic

Max Kanovich

In referring to linear logic fragments,
let N stands for non-commutative versions
(with "\" and "/" being left and right implications, respectively,
and "*" being non-commutative product),
M for multiplicatives,
E for exponentials,
2 for second order quantifiers, and
I for "intuitionistic" version of linear logic fragments.

Lincoln, Scedrov, and Shankar showed the undecidability
of IMLL2 and IMALL2 by embedding of LJ2 (announced in this forum,
to appear in LICS '95).
Lafont has proved the undecidability of MALL2 (announced in this
forum, to appear in the Journal of Symbolic Logic).
Recently, Lafont and Scedrov proved that MLL2 is undecidable
(announced in this forum).

As for non-commutative linear logic,
Emms shows embedding of LJ2 into N-IMLL2 as well,
Kanovich proved the undecidability of Lambek calculus enriched by
the exponential !, and thereby the undecidability of N-MELL.

Here we prove that classical N-MLL2 is also undecidable.

3 May 13:37 1995

### paper available

The paper The Greatest Symmetric Monoidal Closed Category of
Scott-Domains' is available on my ftp-guest account at Imperial
College under

smc.dvi.Z

In it we show that Linear Domains and Linear Maps [MFPS'93] are the greatest
symmetric monoidal closed category of Scott-Domains such that linear
implication is modeled by the space of all linear maps in the
EXTENSIONAL order.

With best regards,
--Michael Huth.

10 May 18:46 1995

### Summer School on SEMANTICS AND LOGICS OF COMPUTATION

A Newton Institute Summer School

SEMANTICS AND LOGICS OF COMPUTATION

25--29 September 1995
Newton Institute, Cambridge, UK

in collaboration with the
ESPRIT CLICS-II project

Second Call for Registration

The Summer School on Semantics and Logics of Computation is being held
as part of a six-month research programme on Semantics of Computation
at the Isaac Newton Institute for Mathematical Sciences, a new
international research centre in Cambridge UK. The Summer School is
sponsored by the CEC ESPRIT research project "Categorical Logic in
Computer Science, II" (CLICS-II). The aim is to present a number of
modern developments in semantics and logics of computation in a way
that is accessible to graduate-level students. Registrations from
postgraduate students will be given priority, but applications by
interested academics and industrialists are also welcomed.

===============================COURSES================================

Samson Abramsky (Imperial)
"Semantics of interaction"
(4 lectures)

10 May 18:58 1995

### papers available

Two papers "Fixpoint Technique for Counting Terms in Typed Lambda
Calculus" and "Lambda definability is decidable for  second order
types and for regular third order types" are available by anonymous
ftp.

"Fixpoint Technique for Counting Terms in Typed Lambda Calculus"

Abstract:  Typed lambda calculus with denumerable set of ground types is
considered. The aim of the paper is to show procedure for counting closed
terms in long normal forms. It is shown that there is a surprising
correspondence between the number of closed terms and the fixpoint
solution of the polynomial equation in some complete lattice. It is proved
that counting of terms in typed lambda calculus can be reduced to the
problem of finding least fixpoint for the system of polynomial equations.
The algorithm for finding the least fixpoint of the system of polynomials
is considered. By the well known Curry Howard isomorphism the result can
be interpreted as a method for counting proofs in the implicational
fragment of the propositional intuitionistic logic. The problem of number
of terms was studied but never published by Ben - Yelles and Roger
Hindlay. Similarly Hirokawa proved that complexity of the question whether
given type ( formula ) possess an infinite number of normal terms (proofs)
is polynomial space complete.

"Lambda definability is decidable for second order types and
for regular third order types"

Abstract: It has been proved by Loader that Statman-Plotkin conjecture
fails. It means that it is undecidable to determine whether or not the
given function in the full type hierarchy is lambda definable. The Loader

11 May 06:28 1995

### LICS'95 2nd Call for Participation

[Since it is relevant and SHORT, I am distributing this conference
announcement to types.  -- Philip Wadler, moderator, Types Forum.]

Tenth Annual IEEE Symposium on
Logic in Computer Science

June 26-29, 1995
San Diego, California

The conference program and registration forms (*) can be obtained by
anonymous ftp from research.att.com, directory /dist/lics.

*** Preregistration deadline is May 26 ***

For early registration, payment must be received by May 26, 1995.  The
deadline for reserving on-campus housing is also May 26; reservations
received later than this are subject to availability.

-----------

(*) Although it is not mentioned on the registration form, vegetarian
and kosher banquet meals are available if requested at the time the

10 May 19:24 1995

### THEMES IN THE SEMANTICS OF COMPUTATION

A Newton Institute Workshop

THEMES IN THE SEMANTICS OF COMPUTATION

17--21 July 1995
Newton Institute, Cambridge, UK

Call for Registration

BACKGROUND

The workshop will take place as part of the Newton Institute programme
on the Semantics of Computation. The general aims of the programme are
twofold. First, to refine the current framework for the semantics of
computation so that it is capable of dealing with the more subtle
computational features present in the programming languages of today
and tomorrow.  Secondly, to provide a framework for interaction
between such fundamental research and the issues confronted by
language designers and software engineers. We particularly have in
mind current developments such as object-based concurrent programming,
and projects to develop the next generation of advanced programming
languages, such as ML 2000.  The range of technical and conceptual
challenges involved in this work requires active collaboration and
flow of information between overlapping communities of mathematicians,
computer scientists and computer practitioners.

WORKSHOP PROGRAMME

The workshop is intended to open up some of the themes to be pursued

12 May 18:59 1995

### Church Festschrift Refereeing

The Alonzo Church Festschrift, sponsored by the ASL and edited by
Tony Anderson and myself, is seeking referees for a number of papers
me for further information.

Cordially, - Mikhail | Why is it that all those who have become eminent
Zeleny@... | in   philosophy  or  politics  or poetry  or art
UCLA Philosophy Dept | are  clearly  of   an  atrabilious  temperament?

12 May 17:48 1995

### A New Basic Set or Proof Transformations

A New Basic Set of Transformations between Proofs
(Abstract)
(Submitted for presentation at Logic Colloquium '95, August 9-17, Haifa, Israel)

Deductive systems based on the so-called Curry-Howard isomorphism [How80] have
an interesting feature: normalization and strong normalization (Church-Rosser
property) theorems can be proved by reductions on the terms of the functional
calculus.  Exploring this important characteristic, we have proved these
theorems for the Labelled Natural Deduction (LND) [deQGab92] via a term
rewriting system (TRS) constructed from the LND-terms of the functional calculus
[deOldeQ94,deOldeQ95].  The LND system is an instance of Gabbay's Labelled
Deductive Systems (LDS) [Gab94], which is based on a generalization of the
functional interpretation of logical connectives [GabdeQ92] (i.e. Curry-Howard
isomorphism).

Proving the termination' and confluence' properties for the TRS associated to
the LND system (TRS-LND) [deOldeQ94], we have in fact proved the normalization
and strong normalization theorems for the LND system, respectively.  The
termination' property guarantees the existence of a normal form of the
LND-terms, while the confluence' property its uniqueness.  Thus, because of the
Curry-Howard isomorphism, we have that every LND derivation converts to a normal
form (normalization theorem) and it is unique (strong normalization theorem)
[deOl95,deOldeQ95].

The significance of applying this technique in the proof of the normalization
theorems lies in the presentation of a simple and computational method, which
allowed the discovery of a new basic set of transformations between proofs,
which we baptized as $\iota$ (iota)-reductions' [deOl95]. With this result, we
obtained a confluent system which contains the $\eta$-reductions.

17 May 09:11 1995

### positions in Nijmegen

Postgraduate studentships at the Computing Science Institute of the
University of Nijmegen, The Netherlands

The Computing Science Institute of the University of Nijmegen has vacancies
for postgraduate students who have just obtained their M.Sc degree   or
will do so within a few months,  on the following 3 projects:

1-Unification of program transformations, automated deduction, functional
specifications and computer algebra.

2-Distributed operating systems in pure functional languages.

3-Parallel evaluation of functional programs.

The projects are for 4 years and should result in a Ph.D thesis.

The positions are open for persons having a EC-passport.

Applications for the positions, including a  curriculum vitae, marks and
two  names of referees for recommendations should be sent before May 25 to
Catholic University Nijmegen,
Faculty of Mathematics and Computer Science
Personele Zaken
Toernooiveld 1
6525 ED Nijmegen
The Netherlands

Please name the project in which you are interested and also the reference
number 55-95.