headers
Pippo Scollo | 2 May 1995 00:09
Picon
Picon
Picon

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
definite shape. Here's some more information about the AMAST newsletter
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
_AMAST Links_, or to previous issues, and if you have access to the
WWW, then please open either of the following:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Max KANOVITCH | 2 May 1995 23:51
Picon

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, 
     A for additives,
     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.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Michael Huth | 3 May 1995 13:37
Picon

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.
Permalink | Reply | 0 comments |
headers
Andrew Pitts | 10 May 1995 18:46
Picon
Picon
Favicon

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

Permalink | Reply | 0 comments |
headers
Marek Zaionc | 10 May 1995 18:58

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

Permalink | Reply | 0 comments |
headers
Amy Felty | 11 May 1995 06:28
Picon

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
visiting the LICS'95 home page at http://math.ucsd.edu/lics95/, or 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
reservation is made.
Permalink | Reply | 0 comments |
headers
Andrew Pitts | 10 May 1995 19:24
Picon
Picon
Favicon

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

Permalink | Reply | 0 comments |
headers
Michael Zeleny | 12 May 1995 18:59

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
ranging from type theory to philosophy of language.  Please contact
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?
Permalink | Reply | 0 comments |
headers
Ruy de Queiroz | 12 May 1995 17:48
Picon

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

Permalink | Reply | 0 comments |
headers
Wil Dekkers | 17 May 1995 09:11
Picon
Picon

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

Permalink | Reply | 0 comments |

Gmane