headers
Amy Felty | 7 Apr 1994 01:53
Picon

LICS'94 Program and Registration


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

Permalink | Reply | 0 comments |
headers
Giuseppe.Longo | 7 Apr 1994 14:33
Picon
Picon
Favicon

Colloquium:


LOGICAL RATIONALITY AND GEOMETRIC INTUITION
"Rationalite' logique et intuition geometrique"
Paris, 9 and 10 June 1994

Ecole Normale Superieure, 45, rue d'Ulm, Salle Dussane
75005 Paris

Jointly organised by the Departement Mathematiques et Informatique de  
l'ENS, CREA (Ecole polytechnique - CNRS) and the Institut d'histoire  
et de philosophie des sciences et des techniques (Paris I - CNRS)

Organizers: Daniel Andler (CREA & Paris X - Nanterre), 

  Giuseppe Longo (CNRS, ENS) et Hourya Sinaceur (CNRS, IHPST)

Thursday June 9, 1994
9h30	Ouverture du colloque: E. Guyon (Directeur, ENS)

10h	Rene Thom (IHES) : L'efficacite' pragmatique des  
mathematiques est-elle due a` la logique ou a` l'intutition  
geometrique?
10h50	Repondant : Giuseppe Longo (ENS)
11h15	Discussion

12h	Aperitif

14h	Alain Berthoz (College de France) : La geometrie euclidienne  
a-t-elle des fondements dans l'organisation des systemes sensoriels  
et moteurs ?
(Continue reading)

Permalink | Reply | 0 comments |
headers
Andrew "P." Black | 19 Apr 1994 20:11
Picon

Re: Foundations of Object-Oriented Languages

[I recommend the following as a useful (and brief!) summary
of current work on object-oriented languages, including
relevant type systems.  -- Philip Wadler, moderator]

     Foundations of Object-Oriented Languages: Workshop Report

A workshop on the foundations of object-oriented languages was held
17th-18th October 1993 at Stanford University, California, USA.  The
workshop was organized by Kim Bruce and Giuseppe Longo and sponsored by
ESPRIT and NSF.  Participation was by invitation only.

The purpose of the workshop was both to understand and compare the many
models of object-oriented languages, and to create better language
constructs and models.  The workshop consisted both of presentations and
lively discussions about such topics as challenge problems for type
systems, relative merits of different language designs and type systems,
and encapsulation and modularity. 

A ten-page report by Andrew Black and Jens Palsberg describes the talks
given at the workshop, and contains a dictionary of object-oriented
terminology and a list of open problems and benchmarks for type
systems.  The report was printed in SIGPLAN Notices Volume 29 Nr 3
(March 1994) but lacks the final page of references.  The full report
can be obtained from

    ftp://crl.dec.com/pub/DEC/sigplan94.ps.Z
or
    ftp://daimi.aau.dk/pub/palsberg/papers/sigplan94.ps.Z
(Continue reading)

Permalink | Reply | 0 comments |
headers
Peter Schroeder-Heister | 11 Apr 1994 17:46

Substructural Logics


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

Permalink | Reply | 0 comments |
headers
Ruy de Queiroz | 7 Apr 1994 18:32
Picon

Workshop on Logic, Lang., Inform. & Comp.


PLEASE NOTE: NEW DEADLINE,  NEW INVITED SPEAKER

	Workshop on Logic, Language, Information and Computation
			    WoLLIC '94
			July 28--30, 1994
			  Recife, Brazil

A Workshop on Logic, Language, Information and Computation, will be held
in Recife, on the northeastern coast of Brazil, from 28th to 30th July 1994.
Contributions are invited in the form of one page (300 words) abstract in all
areas related to logic, language, information and computation, including: pure
logical systems, proof theory, model theory, type theory, constructive
mathematics, lambda and combinatorial calculi, program logic and program
semantics, nonclassical logics, nonmonotonic logic, logic and language,
discourse representation, logic and AI, automated deduction, foundations of
logic programming, logic and computation, and logic engineering.

There will be a number of guest speakers, including some who are already part
of the advanced seminars of the parallel event (see below):
J. Barwise (Indiana), J. Cunha (Porto), J. Fiadeiro (Lisbon),
D. Gabbay (London), J. Lambek (McGill), T. Maibaum (London).
Four others have confirmed their participation: N. da Costa (Sao Paulo),
H. J. Ohlbach (Saarbruecken), U. Reyle (Stuttgart), K. Segerberg (Uppsala).

Submission: One page abstracts (preferably by e-mail to the address
*** wollic94@... ***) must be RECEIVED by **MAY 15, 1994**.
Authors will be notified of acceptance by June 5, 1994.  WoLLIC '94 is
sponsored by the Interest Group in Pure and Applied Logics (IGPL) and The
European Foundation for Logic, Language and Information (FoLLI).  Abstracts from
(Continue reading)

Permalink | Reply | 0 comments |
headers
Pat Lincoln | 20 Apr 1994 19:24
Favicon

WWW


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.
Permalink | Reply | 0 comments |
headers
J Roger Hindley | 25 Apr 1994 10:48

Change of address


The e-address of Roger Hindley has changed to

   j.r.hindley@...

(Former address  majrh@... will be
working for a few weeks more, but the Pyramid machine will
probably die soon.)

  Roger Hindley, Mathematics Dept., University College of Swansea,
                  Wales, U.K.  SA2 8PP

                 Tel. (+) 44-792-205678 ext. 4624
                 Fax (+) 44-792-295843
Permalink | Reply | 0 comments |
headers
Lawrence C Paulson | 25 Apr 1994 13:38
Picon
Picon
Favicon

Isabelle course -- final call


Dear Colleague,

Please forward the attached course announcement.  The course is about the
theorem prover Isabelle.  It will be held one week after LICS and two weeks
after CADE, to facilitate travel arrangements.  Please send technical
questions to Larry.Paulson@... and administrative ones to
rt10005@...

I apologize for multiple copies.

							Larry Paulson

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

UNIVERSITY OF CAMBRIDGE
Programme for Industry

Introduction to Theorem Proving, using "Isabelle"

11-13 July 1994
Course fee 650 pounds sterling
          (350 pounds sterling for academic participants)

AIM OF THE COURSE

Theorem proving systems are growing in popularity and are demonstrating
their utility in many fields: hardware/software verification, protocol
verification, program synthesis, artificial intelligence, and mathematics
research.  The aim of this course is to introduce participants to the
(Continue reading)

Permalink | Reply | 0 comments |
headers
Francois Lamarche | 26 Apr 1994 14:34
Picon

report annoucement


We wish to make the following announcement

           PROOF NETS FOR INTUITIONISTIC LOGIC I:

                      ESSSENTIAL NETS
                     preliminary report

                     Francois Lamarche

In this paper we develop a theory of proof objects for intuitionistic
logic with the connectors tensor, -o, & and !, that we call *essential
nets*.  This allows in particular the interpretation of the simply
typed lamda calculus, with or without product types.  We give a 
correctness criterion for essential nets:  there is an *intrinsic*
property that characterizes the essential nets that come from a proof.

Our methods depend very strongly on the fact that we are dealing with
intuitionistic linear logic (presented in a one-sided sequent fashion
using the Danos-Regnier polarities) and not the full classical
system: notice that all it takes to get full linear logic is the
introduction of linear negation.  Some time ago the author realized
that the system described here was very much simpler than the full
one, and this is due to the presence of a *dependence* (or
*causality*) relation  between the nodes of a net, that allows
for a simple definition of the empire of the nodes of polarity
Output. We strongly believe that this causality relation is essential
for the extension of this system to ones that contain ``partial
terms'', in other words to systems that allow for the expression of
partial recursive funtions and other related concepts of computer
(Continue reading)

Permalink | Reply | 0 comments |
headers
metayer | 25 Apr 1994 15:00
Picon
Favicon

paper annoucement


I recently obtained a geometrical interpretation of the provability
of multiplicative formulas in linear logic, based on a previous
homological approach of proofnets, as explained in the paper: 

     "VOLUME OF MULTIPLICATIVE FORMULAS AND PROVABILITY"

It can be obtained by anonymous ftp at frege.logique.jussieu.fr
Look for vmfp.dvi.Z in pub/scratch.
Here follows an introduction to the paper. Questions and comments are 
mostly welcome.

Best regards, 

Francois Metayer 

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

A module is a (possibly incorrect) proof-structure M together
with a set F of vertices of M, which we call the border
of M. Some extra conditions are required in the precise definition.
A typical example is the graph associated to a multiplicative formula,
with the set of vertices indexed by atomic subformulas
as border. Now the decision problem for multiplicative
formulas is a particular instance of the following question:

Is it possible to paste two given modules along their common
border such that the resulting graph becomes a proof-net?

This paper introduces a correspondance between modules with a given
(Continue reading)

Permalink | Reply | 0 comments |

Gmane