Subject: Re: Papers available by Public ftp
From: [email-masked]
To: Greg Restall <[email-masked]>
Cc: [email-masked]
Date: Mon, 28 Mar 94 13:19:40 PST

--text follows this line--

	Date: Mon, 28 Mar 1994 15:04:37 +1000
	From: Greg Restall <[email-masked]>

	The directory contains a file README with short descriptions of the 
	works in the directory.  They include papers on substructural logics,

With regard to your "A Useful Substructural Logic" in that directory,
it is worth mentioning that this logic supports an equational
definition of transitive closure.  See my paper

	@InProceedings(
Pr90b,	Author="Pratt, V.R.",
	Title="Action Logic and Pure Induction",
	Booktitle="Logics in AI: European Workshop JELIA '90, LNCS 478",
	Editor="J. van Eijck", Publisher="Springer-Verlag", Pages="97-120",
	Address="Amsterdam, NL", Month=Sep, Year=1990)

making this point, abstract appended, paper available by anonymous ftp
as boole.stanford.edu:/pub/jelia.tex.

At a talk at a 1992 conference:

        @InProceedings(
Pr92c,  Author="Pratt, V.R.",
        Title="A Roadmap of Some Two-Dimensional Logics",
        Booktitle="Logic and Information Flow", 
        Editor="Van Eijck, J. and Visser, A.", Year="1994")
	(belatedly published only this year due to unplanned change of
	publisher by the organizers)

I identified a number of RA-like logics.  Your Peirce monoids appear on
my chart as the class RES of residuated monoids, while their expansion
with transitive closure is ACT (for action algebras).  This paper is
twod.tex on Boole.

Key to any equational definition of transitive closure is the ability
to express induction, which requires some form of antimonotonicity.
With residuated or Peirce monoids, antimonotonicity is supplied by
residuation (implication).  An alternative source of antimonotonicity
is Boolean negation, which I used much earlier to define transitive
closure equationally in

	@InProceedings(
Pr79c,	Author="Pratt, V.R.",
	Title="Models of program logics",
	Booktitle="20th Symposium on foundations of Computer Science",
	Address="San Juan", Month=Oct, Year=1979)

and

	@InProceedings(
Pr80b,	Author="Pratt, V.R.",
	Title="Dynamic algebras and the nature of induction",
	Booktitle="12th ACM Symposium on Theory of Computation",
	Address="Los Angeles", Month=Apr, Year=1980)

Vaughan Pratt

=============
Abstract:

In Floyd-Hoare logic programs are dynamic while assertions are static
(hold at states).  In action logic the two notions become one, with
programs viewed as on-the-fly assertions whose truth is evaluated along
intervals instead of at states.  Action logic is an equational theory
ACT conservatively extending the equational theory REG of regular
expressions with operations preimplication a -> b (HAD a THEN b) and
postimplication b <- a (b IF-EVER a).  Unlike REG, ACT is finitely
based, makes a* reflexive transitive closure, and has an equivalent
Hilbert system.  The crucial axiom is that of pure induction,
(a -> a)* = a -> a.

Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Tue, 29 Mar 1994 09:37:23 --100
From: [email-masked] (Jean Marc Andreoli)
To: [email-masked]
Subject: CFP, ECOOP'94 workshop (W4) on Logical Foundations of OOP
X-Sun-Charset: US-ASCII
Content-Length: 3793
Sender: [email-masked]
--text follows this line--

----------------------------------------------------------------------
			Call for participation

			   One day workshop
				  on
	Logical Foundations of Object Oriented Programming

		     in connection with ECOOP'94
		           4 - 8 July 1994
		           Bologna,  Italy

The aim of this workshop is to investigate the relation between logic,
computing and object oriented programming.

Both the declarative and computational aspects of logic have long been
exploited in the context of object-oriented programming. For instance,
researchers   have    investigated  the  use   of   static   type- and
effect-inferencing   mechanisms, and the   use of Dijkstra-Hoare-style
assertional systems  for   reasoning about state changes   produced by
method invocations.    Considerable work  has been done   in extending
basic declarative computational formalisms (e.g. lambda calculus) that
support  the essence  of  OOP.  On the   computational side, novel OOP
techniques have emerged from  the use of "agent-oriented" (concurrent)
programming languages based   on the computational interpretation   of
fragments of various logics.

Conversely,   some  of the fundamental  insights   of  OOP concern the
structuring  of large  (computational)  formal  descriptions so as  to
minimize change  in the face of  evolution. These insights are equally
applicable when the  formal systems are  also logical, as happens  for
example,   in constructing  large  domain  theories   of phenomena  of
interest.

Recent developments in substructural approaches to logic (e.g.  linear
logic) and rewriting logic offer the promise of considerably expanding
the repertoire of  logical techniques that  can be brought to  bear in
the design, execution and  analysis of OO systems. These  developments
internalize a  fundamental  notion  of localized state-change   within
logic. A primary objective of this workshop will be to investigate the
applicability and   usefulness of these   techniques to the  design of
real-world object-oriented computational systems.

The workshop will  consist of short presentations  as well as informal
discussions.  We expect to establish  a state-of-the-art in the use of
logic for Object Oriented  Programming, as well  as to contribute to a
better  understanding  between researchers  in  this area.   Topics of
interest include but are not limited to the following:

- Logic based models for Object Oriented Programming
- Logic and change
- Use of logic in object-oriented domain modeling and analysis
- Declarative object-oriented real-time systems
- Abstraction, Encapsulation, and information hiding in logic
- Knowledge-structuring mechanisms in logic (inheritance, overriding...)
- Process-oriented mechanisms in logic (communication, synchronization...)

Last but not least, descriptions  of  applications developed on  logic
based object-oriented environments are welcome.

Organizers:
	Jean-Marc Andreoli (Rank-Xerox, Grenoble, France) and
	Vijay Saraswat (Xerox, Palo-Alto, California)

Please send a position paper (e-mail if possible, latex prefered) to

Jean-Marc Andreoli         | Tel:  +33 76 61 50 80
Rank Xerox Research Center | Switchboard:  +33 76 61 50 50
6 Chemin de Maupertuis     | Fax:  +33 76 61 50 99
38240 Meylan (France)      | E-mail:  [email-masked]

Specify whether you wish to make a presentation (in  that case, send a
title and 2-3-line abstract). Presentations are  limited to 15 minutes
and will be selected and scheduled by the organizers.

Submission due:		13 May, 1994
Date of the workshop:	4 July, 1994

IMPORTANT:
The  participation  to  the   workshop  is  free,  but  each  workshop
participant must have registered for the main ECOOP conference.
----------------------------------------------------------------------

Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Wed, 30 Mar 94 12:25:56 +0200
From: [email-masked] (Joerg Hudelmaier)
To: [email-masked]
Subject: papers available
Sender: [email-masked]
--text follows this line--

A number of recent papers related to linear logic
are available by anonymous ftp from
ftp.informatik.uni-tuebingen.de:

1) File /pub/LS/lamlog.{ps,dvi}.Z:
Classical Lambek Logic
by J. Hudelmaier and P. Schroeder-Heister.

A paper about proof theoretical properties of the two sided
version of classical noncommutative linear logic. In particular
we formulate a cut free yet complete sequent calculus for this logic.

2) File /pub/LS/hier.ps.Z:
On a hierarchy of fragments of intuitionistic propositional logic
by J. Hudelmaier.

We give a simple syntactic definition of a hierarchy H of sets of
so called CD-sequents such that intuitionistic provability of
the sequents in the stages of H is hard for successive stages of
the polynomial hierarchy. Moreover provability for the set of all
CD-sequents is PSPACE complete. One corollary says that the CD-
sequents provide a polynomial normal form for intuitionistic
propositional logic. Another corollary is

3) File /pub/LS/comp.ps.Z:
On the complexity of commutative and noncommutative linear logic
by J. Hudelmaier.

Here we show that the fragment of both commutative and noncommutative
linear logic based on (one) implication and additive conjunction
is PSPACE complete.

4) File /pub/LS/modal.ps.Z:
On a contraction free sequent calculus for the modal logic S4
by J. Hudelmaier.

We formulate a sequent calculus for S4 in which deductions of
sequents are bounded in length by the length of the endsequent.
The calculus is much more complicated than similar calculi for
intuitionistic propositional logic. But it may be possible to use
this calculus for an embedding of S4 into linear logic without
modalities in a manner similar to what has been done for
intuitionistic implication.

5) File /pub/LS/KTS4.ps.Z:
Improved decision procedures for the modal logics K,T, and S4
by J. Hudelmaier.

Using methods developped in 4) we arrive at decision procedures of
space complexity n log n, n log n, n*n log n for the logics K,
T, and S4 respectively.

Joerg Hudelmaier

Organization: Dipartimento di Informatica - Universita' di Pisa - Italy
From: Francesca Rossi <[email-masked]>
Subject: ilps94 call for workshop proposal (text+latex)
Date: Wed, 30 Mar 1994 18:00:20 +0100 (METDST)
Content-Length: 5323      
To: [email-masked]
Sender: [email-masked]
--text follows this line--

               Call For Workshop Proposals - ILPS'94
             INTERNATIONAL LOGIC PROGRAMMING SYMPOSIUM
         Sponsored by the Association for Logic Programming
                    Post-Conference Workshops
 
Ithaca, New York, USA
November 13 -- 19, 1994

The 1994 International Logic Programming Symposium will be held 
November 13-19, 1994, in Ithaca, New York, USA. Up to six post-conference 
workshops are planned for November 18-19.  Researchers from all areas of 
logic programming are invited to submit proposals.

To encourage active participation and exchange of ideas, the workshops will 
be kept small, preferably under 40 participants. The format of the workshop 
will be determined by the organizer(s) proposing the workshop, but ample 
time must be allowed for general discussion. Workshops can vary in length, 
but the optimal duration will be half a day or a full day.  Having two or 
three co-organizers for a workshop is strongly advised.  Workshops are 
particularly appropriate for specialized subcommunities of researchers for
whom a larger workshop or conference is not yet justified.

Proposals for workshops should be about two pages in length, and 
should contain:

o   A description of the workshop, identifying specific technical 
    issues that will be addressed.
o   A discussion of the timeliness and relevance of the workshop. 
o   The name, postal address, phone and fax numbers, and email
    address of the workshop organizer(s) and identification of the 
    principal contact person. 
o   A proposed schedule for organizing the workshop, a preliminary 
    agenda, and the indication of the length of the workshop.

Proposals should be submitted no later than May 16, 1994. Organizers will 
be notified no later than June 16, 1994.

Workshop organizers will be responsible for:

o   Producing a "Call for Participation" in the workshop and posting it 
    via various electronic lists and/or other means.
o   Reviewing requests to participate in the workshop and selecting 
    participants.
o   Scheduling workshop activities.

Please submit proposals and inquiries (hardcopy or e-mail) to:

Howard Blair
School of Computer and Information Science
Syracuse University
Syracuse, New York 13244-4100
USA\
Phone: 315-443-3565
FAX: 315-443-1122
E-mail: [email-masked]

Return-Path: <@Sunburn.Stanford.EDU,@ICINECA.CINECA.IT:[email-masked]>
Date:  Wed, 30 MAR 94 18:44 N
From: [email-masked]
Reply-To: [email-masked]
Comments: GMAIL V1.3, DECnet, 21 Mar 1989
Subject: School Announcement
To: [email-masked]
X-Original-To:  [email-masked], HONSELL
Sender: [email-masked]
--text follows this line--

PRELIMINARY ANNOUNCEMENT

ADVANCED SCHOOL ON TYPED LAMBDA CALCULUS AND FUNCTIONAL PROGRAMMING

September 19 - September 30, 1994
CISM, Palazzo del Torso,
Piazza Garibaldi, 18 - UDINE Udine (ITALY)

The Advanced School is organized under the auspices of the Italian Chapter of
EATCS (European Association for Theoretical Computer Science) and UNESCO.
It is supported also by the University of Udine and the CNR.

   Formal Methods for specifying, modularizing, verifying, and reusing
large programs and systems, as well as principled languages, which allow to
apply rapidly such methods, are greatly needed in Computer Science.
   Typed Lambda Calculus has been recently understood as a central node in a
conceptual network  which links various fields of Logic to Computer Science.
It has made possible to transfer fruitfully ideas and techniques from
Category Theory, Proof Theory, Type Theory to Computer Science. Based on
formally solid and conceptually disciplined logical grounds, Typed Lambda
Calculus allows for the development of a mathematically clear style of
programming as well as for the design of flexible logical tools and methods
for Computer Science.
   In recent years, Typed Lambda Calculus has been impressively used also as a
metalanguage for defining formal systems for reasoning about Programs and as a
logical framework for designing interactive proof assistants} for computer
aided formal reasoning.

The School will offer 5 series of (approx.8-10) introductory and advanced
lectures on the connections between Typed Lambda Calculus and Category
Theory, Proof Theory, and Type Theory, and on the, more recent, applications of
Typed Lambda Calculus, such as the design of Typed Functional Languages,
General Proof Assistants, and Program Logics.

SCHOOL DIRECTORS

   M. DEZANI CIANCAGLINI (Torino)
   FURIO HONSELL (Udine)

LIST OF SPEAKERS

  JEAN-YVES GIRARD  (Marseilles)
      Proof Theoretic Foundations

  GERARD HUET  (INRIA Rocquencourt)
      Advanced Typed Functional Languages: Theorem Proving in Coq

  JOHN MITCHELL  (Stanford)
      Type Systems and Programming Languages

  EUGENIO MOGGI (Genova)
      Meta-languages and Applications

  S. RONCHI DELLA ROCCA  (Torino)
      Basic Lambda Calculus

The School is intended primarily for young researchers and PhD students in
Computer Science and Mathematics. During the School, participants will be
able to attend also informal talks and discussions of open problems.
PhD students may ask to sit for an examination at the School. It will consist
of a Seminar on a topic agreed upon by the Directors and the Speakers.
There will be demonstrations, and participants will have the opportunity to
use a computer environment.

To apply, participants should fill the form (to be publicized shortly) and
return it together with a recommandation letter to:

Advanced School Secretariat:
Professor F.Honsell
Universita' di Udine,
Dipartimento di Matematica e Informatica
via Zanon, 6,
33100 UDINE - ITALY
Tel: 39-432-272220  Fax:  39-432-510755

The DEADLINE for application is July 31st 1994. Further information can
be obtained via email under the address:

[email-masked]

FEES and SCHOLARSHIPS
The participation fee is 650.000 Italian Liras.
There is a limited number of scholarships available for people who cannot
obtain funding for their travel, participation fee and living expenses from
their institutions. A request for full or partial support should be enclosed
with the applications.

Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Wed, 6 Apr 94 19:53 EDT
From: [email-masked] (Amy Felty)
To: [email-masked]
Subject: LICS'94 Program and Registration
Sender: [email-masked]
--text follows this line--

[This announcement is being sent to email lists.  Our apologies for
multiple copies.]

                   LOGIC IN COMPUTER SCIENCE (LICS)
                   ********************************
                     Ninth Annual IEEE Symposium
                    July 3-7, 1994, Paris, France

             ADVANCE REGISTRATION AND PROGRAM INFORMATION
             ============================================

[This information is available on the world-wide web at
        http://www.research.att.com/lics/
 Postscript, dvi, latex and plain text versions of the conference
 brochure are available via anonymous ftp from research.att.com in
 directory /dist/lics.]

CONFERENCE OFFICE. 
=================
Please address registration form and inquiries to

        LICS'94 Secretariat
        Claudie Thenault
        INRIA-Rocquencourt
        Relations Exterieures
        Domaine de Voluceau BP 105
        78153 Le Chesnay Cedex
        FRANCE
            Phone: 33 (1) 39 63 56 75
            Fax: 33 (1) 39 63 56 38
            E-mail: [email-masked] 

REGISTRATION
============
The registration form should be sent to the conference
office. Registration without payment (or purchase order) enclosed will
not be considered.  For early registration, payment must be received
by June 5.  Fees will be returned in full for any written cancellation
received before June 24. No refund will be made after this date.

A table of registration fees can be found on the registration form.
The member rate applies to members of ACM, IEEE, EATCS and INRIA,
members of the organizing and program committees and authors of
accepted papers.  The student rate applies to full time students; a
copy of the registrant's 1993-94 student card should be included with
the registration form.

The registration fee includes conference participation, a copy of the
proceedings, coffee breaks and an invitation to the welcome reception.
There is a separate charge for the banquet.

Payment must be in French currency, and can be made by bank cheque,
postal cheque, or foreign draft made payable to "Agent Comptable de
l'INRIA", by bank transfer to Tresorerie Generale des
Yvelines, Versailles, account number 10071-78000-00044009 15389, by
postal transfer to CCP Paris---30041-00001-09099 45 B 020-31, or
by institutional purchase order.  We have applied for permission to
allow registration by credit card, and hope to have confirmation of
this possibility by May 1. Participants wishing to use this facility
should contact our office at that time, preferably by email addressed
to [email-masked].  Bank transfers should specify registrant's name
and "Conference reference LICS94".


ACCOMMODATION
=============
Reservations can be made through the Wagonlit Travel Agency.  The
accommodation form should be sent with deposit before June 1 to:

        Wagonlit Travel
        Departement Congres &  Evenements
        50 Rue de Londres
        75008 Paris
        FRANCE
            Tel: 33 (1) 44 90 33 10
            Fax: 33 (1) 44 90 33 15

There are two categories of hotels available, as well as inexpensive
student lodging (no age limit) in an international center in Clichy
(north Paris).  Paris is very popular in the summer, so reservations
should be made as soon as possible.

A deposit is compulsory for hotel reservations, and student lodging
must be entirely prepaid.  Payment must be in French currency, and can
be made by bank cheque, Eurocheque, or foreign draft made payable to
"Wagonlit Travel", by bank transfer to the account 00021935201/61
B.N.P. Paris Saint Lazare, bank code 30004, branch code 0819,
"Wagonlit Travel---code comptable 04/670", or by credit card.  Hotel
deposits will be forwarded to the hotel less 60FF for reservation
fees.  The participant's bank charges must be added to the amount
transferred.

For cancellations made before June 1, payments will be refunded less
60FF for fees; no refunds will be made after June 1.

LOCATION
========
The Conference is being hosted by the Conservatoire National des Arts
et Metiers (CNAM) and will be part of its Bicentennial celebration.
CNAM is a well-known engineering school where professionals are taught
by professionals.  It houses the famous Musee National Des Arts et
Techniques, and is located at 292 Rue Saint Martin in the old center
of Paris, on the right bank of the river Seine.  It is walking
distance from Les Halles, the Centre National d'Art et de Culture
Georges-Pompidou (Beaubourg), the Hotel de Ville (City Hall) and the
cathedral Notre-Dame de Paris.  The nearest Metro station is Arts et
Metiers.

Paris normally enjoys pleasant summer weather in early July.  Days are
warm, but nights may be cool.  For general information on Paris,
contact the Paris Tourist Information Office, 127 Champs Elysees,
75008 Paris, phone number 33 (1) 49 52 53 54.

RECEPTIONS
==========
A Welcome Reception will be held on Sunday evening (17:00-19:00) in a
gallery of CNAM.  The Conference Banquet will be held in the palace
housing the Senate, the upper chamber of the French Parliament.  The
palace was built in the beginning of the 17th century for Marie de
Medicis, widow of King Henry IV.  It is located in the well-known
Jardins du Luxembourg.  To reserve a place at the banquet, the
appropriate column on the registration form must be marked; a banquet
reservation on site will not be possible.


LOCAL ARRANGEMENTS
================== 
Lunches are at the participants' own expense.  Participants may eat in
cafes and restaurants in CNAM's vicinity.  Telephone messages will be
delivered to participants during breaks.  Access to email will be
possible from CNAM.

The organizers cannot be held liable to conference participants for
injury, damage or loss of their personal property. It is suggested
that participants make their own insurance arrangements.

REGISTRATION DESK
=================
A registration and information desk located at the conference site
will operate on Sunday, July 3, from 15:00 to 18:00, and on the
remaining conference days from 8:00 to 18:00.

TRAVEL
======
Paris has two airports, Roissy-Charles de Gaulle, 30km north of
Paris, and Orly, 20km south of Paris.  A frequent Air France bus
service goes from Roissy to Place Charles de Gaulle-Etoile or Porte
Maillot in central Paris (the cost is about 48FF); from Orly the bus
goes to Invalides and stops on demand at Montparnasse (32FF).  There
is also train service.  From Roissy, the RER B line goes to Gare du
Nord or Chatelet; from Orly, the Orlyval goes to Antony where there
is a connection to the RER B (32FF).  A taxi from Orly to central
Paris costs about 150FF; from Roissy, 200FF.

The Metro offers a convenient way to get around the city.  Each trip
(with unlimited transfers) costs one ticket.  Tickets can be bought
individually, but a carnet of 10 is more practical.  RER lines
to the suburbs connect with the Metro and cost more.  Both Metro
and RER tickets can be purchased from ticket booths or machines.

A 40-45% discount may be obtained from AIR INTER for French domestic
blue and white flights, depending on the days of departure.  A voucher
can be requested on the registration form.

Participants requiring a visa for entry into France are strongly
advised to make their application in their home countries at least two
months prior to departure date.


                     LICS'94 REGISTRATION FORM
                     *************************

Last Name __________________________________________________

First Name _________________________________________________

Affiliation ________________________________________________

Street Address _____________________________________________

     _______________________________________________________

City _______________________________________________________

State/Zip __________________________________________________

Country ____________________________________________________

Phone(s) ___________________________________________________

Fax ________________________________________________________

E-mail _____________________________________________________

REGISTRATION RATES.  The fees below are in French currency and include
18.6% VAT.  Please circle the applicable fees.

                through June 5    from June 6

Regular              2200           2600
Member               1700           2100
Student              1000           1200
Banquet               300            300

Total Fee ___________________________________________________

Rate justification __________________________________________

Full-time student at ________________________________________

I need an AIR INTER discount form:  Yes / No

Payment (circle one): Cheque (Bank/Foreign Draft)
                      / Purchase Order
                      / Bank Transfer (include copy)


                     LICS'94 ACCOMMODATION FORM
                     **************************
                     to be returned before Jun 1

Last Name __________________________________________________

First Name _________________________________________________

Company ____________________________________________________

Street Address _____________________________________________

     _______________________________________________________

City _______________________________________________________

State/Zip __________________________________________________

Country ____________________________________________________

Phone(s) ___________________________________________________

Fax ________________________________________________________

1A.  HOTEL.  Please reserve:

     *...twin bed room shared by 2 persons

     *...single room

     in a hotel of ________ stars, for ________ nights,

     from _________________ to _________________(a.m.).

     Average rates in French currency, per room and per night,
     room only, taxes and service included:

     Category         Single/Twin       Deposit

     2**                385/500           460

     3***               550/700           760

1B.  YOUTH HOSTEL.  Please reserve:

     *...bed in a twin bed room, bathroom and toilets outside the
     room, compulsory stay of 4 nights (July 3 to 7, 1994),
     continental breakfast included, full prepayment compulsory, fixed
     rate per person 4 nights: 600FF.

2.  PAYMENT.  Deposit/prepayment of ____________ FF

    Circle one:  Visa / Eurocard / Mastercard
                 / Cheque (Bank/Euro/Foreign Draft)
                 / Bank Transfer (include copy)

    Credit card # __________________________ Exp. __________

    Signature _____________________________ Date ___________


                            CONFERENCE PROGRAM
                            ******************

SUNDAY, July 3
==============

REGISTRATION                                            (15:00-18:00)

WELCOME RECEPTION                                       (17:00-19:00)

MONDAY, July 4
==============

REGISTRATION                                              (8:00-9:00)

OPENING ADDRESSES                                         (9:00-9:25)

INVITED LECTURE I                                        (9:25-10:25)
    Chair: Robert Constable (Cornell)
    Rod Burstall (Edinburgh), Lambda-terms, proofs and refinement

SESSION 1: FINITE MODEL THEORY                          (10:50-12:30)
    Chair: Daniel Leivant (Indiana)

10:50 McColm's Conjecture,
    Yuri Gurevich (Michigan), Neil Immerman (U Mass) & Saharon Shelah
    (Hebrew U & Rutgers)

11:15 The expressive power of finitely many generalized quantifiers,
    Anuj Dawar (Swansea) & Lauri Hella (Helsinki)

11:40 Generalized quantifiers for simple properties,
    Martin Otto (RWTH Aachen)

12:05 How to define a linear order on finite models,
    Lauri Hella (Helsinki), Phokion Kolaitis (UC Santa Cruz), & Kerkk
    Luosto (Helsinki)

LUNCH                                                   (12:30-14:00)

SESSION 2: CONCURRENCY                                  (14:00-15:15)
    Chair: Vaughan Pratt (Stanford)

14:00 Finitary fairness,
    Rajeev Alur (Bell Labs) & Thomas Henzinger (Cornell)

14:25 Bisimulation is not (first-order) equationally axiomatisable,
    Peter Sewell (Edinburgh)

14:50 Foundations of timed concurrent constraint programming,
    Vijay Saraswat (Xerox PARC), Radha Jagadeesan (Loyola) & Vineet
    Gupta (Stanford)

SESSION 3: SEMANTICS I                                  (15:40-16:55)
    Chair: Achim Jung (Darmstadt)

15:40 A fully abstract semantics for concurrent graph reduction,
    Alan Jeffrey (Sussex)

16:05 An axiomatization of computationally adequate domain-theoretic
    models of FPC,
    Marcelo Fiore & Gordon Plotkin (Edinburgh)

16:30 On strong stability and higher-order sequentiality,
    Loic Colson & Thomas Ehrhard (Marne-la-Vallee)

SESSION 4: DOMAIN THEORY                                (17:10-18:00)
    Chair: Carl Gunter (U Penn)

17:10 Linear types, approximation and topology,
    Michael Huth, Achim Jung & Klaus Keimel (Darmstadt)

17:35 Domain theory and integration,
    Abbas Edalat (Imperial Coll.)

BUSINESS MEETING                                              (20:00)

TUESDAY, July 5
===============

TUTORIAL I                                                (8:30-9:45)
    Chair: Moshe Vardi (Rice)
    Ed Clarke (CMU), Model Checking

SESSION 5: CONSTRAINTS                                  (10:00-10:50)
    Chair: Harald Ganzinger (MPI Saarbrucken)

10:00 Negative set constraints with equality: an easy proof of
    decidability,
    Witold Charatonik (Wroclaw) & Leszek Pacholski (Polish Academy of
    Sciences)

10:25 Systems of set constraints with negative constraints are
    NEXPTIME-complete,
    Kjartan Stefansson (Cornell)

SESSION 6: MODAL AND TEMPORAL LOGICS I                  (11:15-12:30)
    Chair: Dexter Kozen (Cornell)

11:15 A compositional proof system for the modal mu-calculus,
    Hendrik Reif Andersen (TU Denmark), Colin Stirling (Edinburgh) &
    Glynn Winskel (Aarhus)

11:40 On the parallel complexity of model-checking in the modal
    mu-calculus,
    Shipei Zhang, Oleg Sokolsky & Scott Smolka (SUNY Stony Brook)

12:05 Complexity transfer for modal logic,
    Edith Hemaspaandra (Le Moyne)

LUNCH                                                   (12:30-14:00)

SESSION 7: TYPES I                                      (14:00-15:15)
    Chair: Paris Kanellakis (Brown)

14:00 Typability and type-checking in the second-order lambda-calculus
    are equivalent and undecidable,
    J.B. Wells (Boston U)

14:25 Efficient inference of object types,
    Jens Palsberg (Northeastern)

14:50 Type inference and extensionality,
    Adolfo Piperno (Roma) & Simona Ronchi della Rocca (Torino)

SESSION 8: CONSTRUCTIVE MATHEMATICS                     (15:40-16:55)
    Chair: Daniel Leivant (Indiana)

15:40 A groupoid model refutes uniqueness of identity types,
    Martin Hofmann (Edinburgh) & Thomas Streicher (LMU Muenchen)

16:05 A non-elementary speed-up in proof length by structural clause
    form transformation,
    Matthias Baaz, Christian Fermueller & Alexander Leitsch (TU Wien)

16:30 Upper and lower bounds for tree-like cutting planes proofs,
    Russell Impagliazzo (UC San Diego), Toniann Pitassi (UC San Diego)
    & Alasdair Urquhart (Toronto)

SESSION 9: COMPLEXITY AND DATABASES                     (17:10-18:00)
    Chair: David McAllester (MIT)

17:10 The power of reflective relational machines,
    Serge Abiteboul (INRIA), Christos Papadimitriou (UC San Diego) &
    Victor Vianu (UC San Diego)

17:35 A syntactic characterization of NP-completeness,
    J. Antonio Medina & Neil Immerman (U Mass)

EVENING LECTURE                                         (19:30-20:30)
    Chair: Jean-Pierre Jouannaud (Paris Sud & CNRS)
    Corrado Boehm (Roma), An algebraic view of the lambda-calculus

WEDNESDAY, July 6
=================

TUTORIAL II                                               (8:30-9:45)
    Chair: Samson Abramsky (Imperial Coll.)
    Gerard Berry (CMA),
    The semantics of synchronous concurrent languages

SESSION 10:  LOGIC PROGRAMMING                          (10:00-10:50)
    Chair: Krzysztof Apt (CWI)

10:00 The declarative semantics of the Prolog selection rule,
    Robert Staerk (U Muenchen)

10:25 Semantics of meta-logic in an algebra of programs,
    Antonio Brogi & Franco Turini (Pisa)

SESSION 11: LINEAR LOGIC                                (11:15-12:30)
    Chair: Samson Abramsky (Imperial Coll.)

11:15 A multiple-conclusion meta-logic,
    Dale Miller (U Penn)

11:40 Proof search in first-order linear logic and other cut-free
    sequent calculi,
    Patrick Lincoln & N. Shankar (SRI)

12:05 Linear logic, totality and full completeness,
    Ralph Loader (Oxford)

LUNCH                                                   (12:30-14:00)

SESSION 12: TYPES II                                    (14:00-15:15)
    Chair: Frank Pfenning (CMU)

14:00 The emptiness problem for intersection types,
    Pawel Urzyczyn (Warsaw)

14:25 Subtyping and parametricity,
    Gordon Plotkin (Edinburgh), Martin Abadi (DEC SRC) & Luca Cardelli
    (DEC SRC)

14:50 On the Church-Rosser property for expressive type systems and
    its consequences for their metatheoretic study,
    Herman Geuvers (Nijmegen) & Benjamin Werner (Cornell & INRIA)

SESSION 13: SEMANTICS II                                (15:40-16:55)
    Chair: Prakash Panangaden (McGill)

15:40 A semantics of object types,
    Martin Abadi & Luca Cardelli (DEC SRC)

16:05 Passivity and independence,
    Uday Reddy (Illinois)

16:30 A general semantics for evaluation logic,
    Eugenio Moggi (Genova)

SESSION 14: CATEGORY THEORY                             (17:10-18:00)
    Chair: Glynn Winskel (Aarhus)

17:10 Reflexive graphs and parametric polymorphism,
    Edmund Robinson (Sussex) & Giuseppe Rosolini (Genova)

17:35 Categories, allegories and circuit design,
    Carolyn Brown (Sussex) & Graham Hutton (Chalmers)

BANQUET

THURSDAY, July 7
================

INVITED LECTURE II                                       (9:00-10:00)
    Chair: Gerard Huet (INRIA)
    Henk Barendregt (Nijmegen),
    Results and problems related to proof-checking

SESSION 15: REWRITING                                   (10:00-10:50)
    Chair: Jean-Pierre Jouannaud (Paris Sud & CNRS)

10:00 Rewrite techniques for transitive relations,
    Leo Bachmair & Harald Ganzinger, (Max-Planck-Institut)

10:25 Normalised rewriting and normalised completion,
   Claude Marche (CNRS & INRIA)

SESSION 16: LAMBDA-CALCULUS                             (11:15-12:30)
    Chair: Jean-Jacques Levy (INRIA)

11:15 Modularity of strong normalization and confluence in the
    algebraic lambda-cube,
    Franco Barbanera (Torino), Maribel Fernandez (Paris Sud & CNRS),
    & Herman Geuvers (Nijmegen)

11:40 Cyclic lambda graph rewriting
    Zena Ariola (U Oregon) & Jan Willem Klop (CWI)

12:05 Paths in the lambda-calculus,
    Andrea Asperti (Bologna), Vincent Danos (CNRS & Paris 7), Cosimo
    Laneve (INRIA & CMA), & Laurent Regnier (CNRS)

LUNCH                                                   (12:30-14:00)

SESSION 17: MODAL AND TEMPORAL LOGIC II                 (14:00-15:15)
    Chair: Colin Stirling (Edinburgh)

14:00 A trace based extension of linear time temporal logic,
    P.S. Thiagarajan (SPIC Madras)

14:25 Axioms for knowledge and time in distributed systems with
    perfect recall,
    Ron van der Meyden (NTT Tokyo)

14:50 Compositional verification of real-time systems,
    Edward Chang (Stanford), Zohar Manna (Stanford), & Amir Pnueli
    (Weizmann Institute)

SESSION 18: LOGIC IN ARTIFICIAL INTELLIGENCE            (15:40-16:55)
    Chair: Peter Schroeder-Heister (Tuebingen)

15:40 Logical bilattices and inconsistent data,
    Ofer Arieli & Arnon Avron (Tel Aviv)

16:05 A modal logic for subjective default reasoning,
    Shai Ben-David & Rachel Ben-Eliyahu (Technion)

16:30 Language completeness of the Lambek calculus,
    Mati Pentus (Moscow State)

SESSION 19: AUTOMATED DEDUCTION}                        (17:10-18:00)
    Chair: Gerard Huet (INRIA)

17:10 Rigid E-unifiability is NEXPTIME-complete,
    Jean Goubault (Bull)

17:35 Higher-order narrowing,
    Christian Prehofer (TU Muenchen)

END OF CONFERENCE



CONFERENCE ORGANIZATION
***********************

LICS General Chair: Robert L. Constable

1994 Conference Co-chairs: Gerard Huet & Jean-Pierre Jouannaud

1994 Program Chair: Samson Abramsky

Publicity Co-chairs: Amy Felty & Douglas Howe

1994 Local Arrangements: A. Theis-Viemont & C. Thenault

PROGRAM COMMITTEE:
==================
S. Abramsky, K. Apt, H. Ganzinger, C. Gunter, A. Jung, 
P. Kannelakis, D. Kozen, D. Leivant, J.-J. Levy, 
D. McAllester, P. Panangaden, F. Pfenning, V. Pratt, 
P. Schroeder-Heister, C. Stirling, G. Winskel.

ORGANIZING COMMITTEE:
=====================

M. Abadi, S. Abramsky, S. Artemov, A. Borodin, A. Bundy, S. Buss,
E. Clarke, R. Constable (Chair), A. Felty, U. Goltz, Y. Gurevich,
S. Hayashi, D. Howe, G. Huet, J.-P. Jouannaud, D. Kapur, C. Kirchner, 
P. Kolaitis, R. Kosaraju, D. Kozen, D. Leivant, A.R. Meyer, D. Miller,
J. Mitchell, Y. Moschovakis, M. Okada, P. Panangaden, A. Pitts,
G. Plotkin, J. Remmel, S. Ronchi della Rocca, G. Rozenberg, A. Scedrov, 
D. Scott, J. Tiuryn, M.Y. Vardi.

Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Mon, 11 Apr 94 17:46:58 +0200
From: [email-masked] (Peter Schroeder-Heister)
To: [email-masked]
Subject: Substructural Logics
Sender: [email-masked]
--text follows this line--

A collection of papers originating from a conference held 1990
at the University of T\"ubingen is now available.

Kosta Do\{v}sen & Peter Schroeder-Heister (Eds.),
Substructural Logics. 
Oxford University Press 1993.
ISBN 0-19-853777-8.
UK-Price: GBP 40.00, US-Price:  approx.  USD 60.00.

(On cover and title page of the printed edition the
editors are listed in non-alphabetical order. This is due
to an error by the publisher. It does not express any rank order.)  

Contents:

Preface

A Historical Introduction to Substructural Logics
K. Do\v{s}en 

Life in the Undistributed Middle
N. Belnap 

Theorems in Classical Logic are Instances of Theorems in Condensed
BCI Logic
M.W. Bunder  

Partial Gaggles Applied to Logics with Restricted Structural Rules
J.M. Dunn 

A General Theory of Structured Consequence Relations
D.M. Gabbay  

Decidability and Interpolation for a First-Order Relevance Logic
A. Kron 

Logic without Structural Rules (Another Look at Cut Elimination)
J. Lambek 

>From Categorial Grammar to Bilinear Logic
J. Lambek  

The Semantics of Entailment 0
R.K. Meyer and E.D. Mares 

Semantics for Substructural Logics
H. Ono 

The Semantics of Pretopologies
G. Sambin  

Lambda-Terms with Functional Symbols and Decidability in
Certain Closed Categories
S. V. Soloviev 

Tutorial on Linear Logic
A.S. Troelstra 

The Landscape of Deduction
J. van Benthem  

Index 

The preface and the first page of each chapter are contained in
the file /pub/LS/substruc.ps.Z which can be ftp'ed from
ftp.informatik.uni-tuebingen.de.

Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Thu, 14 Apr 94 16:56 EDT
From: [email-masked] (Amy Felty)
To: [email-masked]
Subject: LICS'94 registration and ASL members
Sender: [email-masked]
--text follows this line--

                      LOGIC IN COMPUTER SCIENCE                   
                   ********************************
                     Ninth Annual IEEE Symposium
                    July 3-7, 1994, Paris, France

Please note the following correction to the LICS'94 registration
information: the member rate also applies to members of the
Association for Symbolic Logic.

[Complete program and registration information is available on the
 world-wide web at
        http://www.research.att.com/lics/
 Postscript, dvi, latex and plain text versions of the conference
 brochure are available via anonymous ftp from research.att.com in
 directory /dist/lics.]

Date: Wed, 20 Apr 1994 08:19:44 +0100
To: [email-masked]
From: [email-masked]
Subject: PhD theme
Sender: [email-masked]
--text follows this line--

I have so far taken a broad interest in Linear Logic, but have not yet
found out in which direction to do do any further work. This is probably
due to the lack of interest among colleages and therfore the impossiility
of apt on site discussions.

As I am still determined to do further work on Linear Logic I have two
questions:

1) What are the main fields of interest to researchers (i.e *you*) at the
moment?

2) Do you have any suggestions as to which topics (open problems) I could
focus on for my PhD?

Any help and suggestions are gratefully accepted. Thanks in advance.
Berndt

----------------------------------------------------------------------------
Berndt Farwer
Universit"at Hamburg     \\\\\    \\\\\\\
FB Informatik             \\  \\   \\      [email-masked]
Diplomand TGI              \\\\\    \\\\      phone (++44)+40-54715-244
Vogt-K"olln-Str. 30         \\  \\   \\       fax   (++44)+40-54715-246
D-22301 Hamburg              \\\\\    \\
Germany

Return-Path: <@Sunburn.Stanford.EDU:[email-masked]>
Date: Wed, 20 Apr 94 10:24:14 -0700
From: Pat Lincoln <[email-masked]>
To: [email-masked]
Subject: WWW
Sender: [email-masked]
--text follows this line--

I have built a small www server for linear logic:

http://www.csl.sri.com/linear/sri-csl-ll.html

This contains two implementations of a par symbol for TeX, a picture
from last year's workshop, archives of old messages to the linear
mailing list, and pointers to ftp directories containing papers
previously announced on the linear mailing list.  Also reachable
from there in http://www.csl.sri.com/history.html is a picture of
the original mouse (developed at SRI in the 1960's) and other 
items of computing history.

Although ftp is a slower and uglier interface than mosaic,
the linear information is available through anonymous ftp to:
ftp.csl.sri.com in directory /pub/linear.

pdl.