headers
Vaughan Pratt | 3 Jan 1991 12:29
Picon

Concurrency and linear logic paper

Date: Wed, 2 Jan 91 23:03:40 PST

The following extended abstract can be retrieved by anonymous ftp from
boole.stanford.edu, IP address 36.8.0.65.  Instructions for retrieving
this and other papers may found in /pub/README.  Contact me,
pratt@..., if you need further assistance or would prefer
to receive a copy by email.

		  Concurrent Automata and Their Logic
			   Vaughan Pratt
			Stanford University

A concurrent automaton is a poset with a top (the global initial state)
and all nonempty sups (the local initial states).  These form a
nondegenerate self-dual category Aut admitting universally definable
operations constituting a concurrent programming language and
additional operations yielding a linear logic of concurrency.  The
cofree automaton !a is a power set whose dual ?a is a free automaton by
self-duality, obtainable from !a by moving the empty set to the top.
The linear logic theory Th(CSLat) of complete semilattices strictly
extends Th(Aut), having no counterexample to !a=?a since !a and ?a are
power sets on the underlying set of a but for dual reasons.  Both
theories strictly extend linear logic with such howlers as 0=1; these
but not !a=?a are removable by intersecting with classical logic,
equivalent to taking both sides of the respective dualities as a single
model.  This makes Aut the best model of linear logic to date.  The
self-duality of both categories facilitates a noncategorical account
requiring only elementary lattice theory for a complete understanding.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Vaughan Pratt | 4 Jan 1991 15:06
Picon

Corrections to "Concurrent Automata and their Logic"

Date: Fri, 4 Jan 91 00:46:20 PST

With regard to the paper "Concurrent Automata and their Logic" that I
announced yesterday, I included in it a brief treatment of !a and ?a
which I thought pretty much covered things.  On reflection today it was
apparent I'd botched this badly due to not having thought much about
these odd creatures before.  Now that I've rethought this I see a lot
more clearly what's going on, and have redone it as follows.

To begin with, ! and ? should be interchanged.  !a should be FU(a), the
free automaton on the underlying set of states of a, and ?a is its
dual, at least as an object; you need the dual to be ?a' for the maps
to be oriented correctly.

For example if a has 2 states then ?a and !a are respectively the
diamond and the steeple, denoting concurrency and choice.

                ?a:         !a:
                    *            *
                   / \           |
                  *   *          *
                   \ /          / \
                    *          *   *

I call these respectively verify(a) and debug(a).  (I badly wanted
verify(a) to be called !a ("of course it works"), and debug ?a ("why
does it not work?"), for obvious reasons.  Unfortunately one can only
achieve this if one takes schedules as the basic sort and automata
their looking glass reflection, which I am reluctant to do.)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Vaughan Pratt | 5 Jan 1991 16:06
Picon

automata or schedules !?

Date: Fri, 4 Jan 91 09:49:58 PST

As my confusion over which way round to make ! and ? highlights, there
is an interesting question as to whether automata or schedules
constitute the real world.  This is a theme I elaborate on in the
repaired paper, which I have just released now.  (*Please* throw away
your buggy version, very sorry about the nuisance.)

Let me go into additional detail here.  This is too long to go in the
paper, but a few concurrency specialists and/or philosophers may find
these ruminations of some interest.

Let me list the appropriate choice of linear logic symbols for certain
programming constructs, as a function whether one takes automata or
schedules for the models of one's logic (and hence the other for the
sentences).  This assumes the particular category of my paper, posets
with top and all nonempty sups.

Since this note was motivated by concerns about ! and ?, for the sake
of minimizing notation changes in this note I'll use linear logic
notation throughout this note:  & for Girard's additive product, ^8 for
inverted ampersand, + for additive plus (Girard's circle plus), and  <at> 
for tensor product.  I will always assume & means product, + coproduct,
and  <at>  tensor.  I'm not sure what ! and ? should be, but I've taken the
equation !a <at> !b = !(a&b) as the orienting criterion and noting that the
tensor product of free automata in Aut is free.

		Automata as models        Schedules as models

concurrence            &                       +
(Continue reading)

Permalink | Reply | 0 comments |
headers
Vaughan Pratt | 7 Jan 1991 15:29
Picon

automata run schedules

Date: Sun, 6 Jan 91 21:51:29 PST

On Friday I wrestled with the question of which side of The Mirror
(Alice's looking glass) to locate this theory that I've been writing
about, namely concurrent automata (state spaces) and schedules (event
spaces).  Which are the objects and which are their duals, the function
spaces to a dualizing object?

If the subject matter had been vector spaces, one would know right away
that this kind of question had no mathematical content.  A vector space
is a vector space, whether it is doing duty as an object or a function
space.

It's the same thing here.  Only the application cares.

Since I want this theory not just for its mathematics but for a
programming language I'm designing, I do care which are the vector
spaces and which their duals in this application.

On Friday I voted that automata, or state spaces, were vector spaces.
That is, I said that the automata were the objects in the "real world,"
and were the things that product and coproduct and tensor were to be
applied to.  Schedules or event spaces were then their duals.

After reflecting on this for a couple of days I now want to change my
vote.  I really do want to treat schedules, or event spaces, as the
objects and to regard the automata as the reflection or dual of
schedules.

This has the advantage to me of putting me back in the framework I have
(Continue reading)

Permalink | Reply | 0 comments |
headers
Giuseppe Longo | 11 Jan 1991 18:29
Picon

5th Jumelage on Typed Lambda Calculus

Date: Fri, 11 Jan 91 09:55:41 +0100

Here is the program of the fifth meeting of the EEC Jumelage project
                        "Typed Lambda Calculus"
directed by J.Y. Girard.

For any question, contact the local organizer:

Giuseppe Longo
Laboratoire d'Informatique
Ecole Normale Superieure
45, Rue D'Ulm
75005  Paris   (France)

(tel. ++33-1-4329-1225 poste 3328, secr.3279, direct 4326-7240;
FAX 4634-0531;    e-mail: longo@...)

(Please note the new PERMANENT address of G.L.)

****************************************************************************
                5TH JUMELAGE MEETING ON TYPED LAMBDA CALCULUS

                     February 1-6, 1991, PARIS

****************************************************************************
                            FRIDAY 1st

09.30         WELCOME
09.45 - 10.30 Jean-Yves Girard
              "Denotational semantics of classical logic"
(Continue reading)

Permalink | Reply | 0 comments |
headers
Barbara Radle | 16 Jan 1991 18:54
Picon

Optimal Derivation in Term Rewriting Systems, 1/29, 10:45am

Date: Wed, 16 Jan 91 10:31:56 EST

			SEMINAR

		Date: Tuesday, January 29, 1991
		Time: Refreshments at 10:45 a.m.
		Place: Second Floor Lounge

	Optimal Derivation in Term Rewriting Systems
		Without Critical Pairs

			Luc Maranget
			   INRIA

			Abstract

	This work introduces a new notion of labeled Term
Rewriting Systems (labeled TRS).  This notion expresses sharing
in TRS.  A new notion of conditional TRS is also introduced.
Conditional TRS allows us to extend the properties of TRS
without critical pairs to a class of Systems wider than the
usual one.  In this extended notion of systems without critical
pairs, optimal derivations are characterized.  Furthermore, for
any normalizable term, it is possible to compute an optimal
normalizing derivation.

	These results are applied to two systems describing weak
lambda-calculi.  The call-by-name-with-sharing or lazy strategy
is shown to be optimal in these systems.
(Continue reading)

Permalink | Reply | 0 comments |
headers
Stephen.Brookes | 17 Jan 1991 16:31
Picon

MFPS91 conference

Date: Wed, 16 Jan 91 13:52:31 EST
To: CMU-TheoryNet-Request@..., concurrency <at> theory.lcs.mit.edu,
        theory-logic@..., types <at> theory.lcs.mit.edu

	MATHEMATICAL FOUNDATIONS OF PROGRAMMING SEMANTICS (MFPS91)
			March 25-28, 1991
		    Carnegie Mellon University
		    School of Computer Science
		       Pittsburgh, Pa 15213
		
		       GENERAL INFORMATION

This conference is the seventh in a series intended to bring together 
computer scientists and mathematicians for discussion of research problems, 
results and directions in programming language semantics. 
A major goal of the series is to provide a forum for researchers in all 
areas surrounding semantics to report on their research progress, 
and to improve communication and interactions between mathematicians and 
computer scientists who work in these areas. 
The conference covers a broad range of topics related to programming language
semantics, including:

	Order-theoretic, topological and categorical approaches
	Applications to programming language design and implementation
	Program analysis and verification
	Theory of concurrency
	Types and polymorphism

PROGRAM COMMITTEE
The program committee for MFPS91 includes:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Stephen.Brookes | 17 Jan 1991 16:40
Picon

MFPS91 program

Date: Wed, 16 Jan 91 15:04:56 EST
To: THEORYNT@..., concurrency <at> theory.lcs.mit.edu,
        theory-logic@..., types <at> theory.lcs.mit.edu

	MATHEMATICAL FOUNDATIONS OF PROGRAMMING SEMANTICS (MFPS91)
		    	March 25-28, 1991
		    Carnegie Mellon University
		    School of Computer Science
		       Pittsburgh, Pa 15213

		      CONFERENCE PROGRAM

INVITED SPEAKERS
The following have agreed to be invited speakers at MFPS91:

	Jon Barwise, Indiana University
	John Reynolds, Carnegie Mellon University
	Dana Scott, Carnegie Mellon University
	Mitchell Wand, Northeastern University
	Glynn Winskel, Aarhus University

CONTRIBUTED PAPERS
The following papers have been selected by the program committee:

On Relating Concurrency and Nondeterminism
Luca Aceto (University of Sussex, UK)

HSP type theorems in the category of posets
Michael Barr (McGill University, Montreal, Canada)
(Continue reading)

Permalink | Reply | 0 comments |
headers
Stephen.Brookes | 17 Jan 1991 16:40
Picon

MFPS91 local arrangements

Date: Wed, 16 Jan 91 15:06:15 EST
To: THEORYNT@..., concurrency <at> theory.lcs.mit.edu,
        theory-logic@..., types <at> theory.lcs.mit.edu

	MATHEMATICAL FOUNDATIONS OF PROGRAMMING SEMANTICS (MFPS91)
			March 25-28, 1991
		    Carnegie Mellon University
		    School of Computer Science
		       Pittsburgh, Pa 15213
		    

 	            TRAVEL and LOCAL ARRANGEMENTS

ACCOMMODATION
A block of hotel rooms has been reserved for use by MFPS participants at:
	Holiday Inn at University Center
	100 Lytton Avenue (at Fifth Avenue)
	Pittsburgh, PA  15213.
	Telephone (412) 682-6200.
	Rate: Singles $85 (9% tax).

	Confirmation Dates: Arrival    Sunday    March 24 1991
			    Departure  Thursday  March 28 1991
	Room rates and the block of rooms have been guaranteed until March 10.
	Please be sure to identify yourself as a participant in the
	``Mathematical Foundations of Programming Semantics'' conference
	when making a reservation, to assure special group rates.
 	
TRANSPORTATION
	The hotel and CMU are located in the Oakland area of Pittsburgh.
(Continue reading)

Permalink | Reply | 0 comments |

Gmane