Subject: a paper
Date: Wed, 31 Mar 93 16:26:57 EST
From: pavlovic@triples.Math.McGill.CA (Dusko Pavlovic)

A paper on logic and factorisations

			MAPS I:
		RELATIVE TO A FACTORISATIONS SYSTEM 
		by Dusko Pavlovic

is available by anonymous ftp from triples.math.mcgill.ca. The file is
called mapsI-A4.dvi.Z (or mapsI-US.dvi.Z). It is in the directory
pub/pavlovic. Please let me know if you have problems fetching or
printing this file.

	Regards,
	Dusko Pavlovic




			Abstract	

Originally, the categorical calculus of relations was developed using
the canonical factorisation in regular categories. More recently,
relations restricted to a proper factorisation system have been
studied by several authors. In the present paper, we consider the
general situation, in which relations are induced by an arbitrary
stable factorisation. This extension of the calculus of relations is
necessary for a categorical development of strongly constructive (and
computational) logic, where non-monic relations come about naturally.

In this setting, we analyze the correspondence of the maps, i.e. the
total, single-valued relations, and the functions, as given by the
arrows in the underlying category.


++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Subject: mapsI
Date: Mon, 5 Apr 93 12:13:30 EDT
From: pavlovic@triples.Math.McGill.CA (Dusko Pavlovic)

There was a gap in section 3 of my paper "Maps I", announced here on
Friday. I noticed and fixed it on Sunday, but some people had already
downloaded it. Sorry about this. 
- Dusko Pavlovic  
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Subject: Piaget
Date: 10 Apr 93   10:08:40 EST
From: <cxm7@pop.cwru.edu>

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

	Has anyone here seen Piaget's book _Morphismes et Categories_?
I haven't yet, but will, and I wondered if anyone had an opinion
on it.  (It is not clear to me from the listing how much of it
is by Piaget.)

Best, Colin McLarty  


++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Subject: Workshop on Foundational Methods in Computer Science
Date: Sat, 10 Apr 93 10:21 PDT
From: hook@hood.cse.ogi.edu (Jim Hook)

Preliminary Announcement:  

	Second Annual Workshop on 
	Foundational Methods in Computer Science
	A workshop on applications of categories
		in computer science

Dates:  June 4-6, 1993

Location:  Reed College, Portland, Oregon

Overview:
This will be the second year of the workshop on foundational methods
in computer science.  It is an "informal, even casual," workshop
bringing together mathematicians and computer scientists with an
interest in category theory and its applications to computer science.

The workshop will have approximately the same format as last year,
with a one day tutorial on June 4 and short research presentations on
June 5 and 6.  There will not be a formal proceedings.  

Guests:
I am still in the process of contacting distinguished visitors and
guests.  Tutorials will be presented by Ernie Manes, Robin Cockett and
David Benson (there may be others as well).  

Participation: 
People wishing to participate should send me email.  We hope to
encourage the participation of researchers at all levels in this
workshop.

Fees: 
I have made arrangements for dormitory accommodations and classroom
space.  I haven't negotiated the meal plan yet and I haven't completed
a budget, so I don't yet have a registration fee calculated.  I hope
to keep the fees to an absolute minimum.

----------------------------------------------------------------------------
James Hook             | Department of Computer Science and Engineering
 hook@cse.ogi.edu      | Oregon Graduate Institute of Science & Technology
 Phone: (503) 690-1169 | 19600 N.W. von Neumann Drive
 Fax:   (503) 690-1029 | Beaverton, OR 97006-1999
----------------------------------------------------------------------------

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Subject: LICS93
Date:        Sat, 10 Apr 93 18:33:57 ADT
From: "daniel leivant" <leivant@cs.indiana.edu>

May I request you to post the following announcement on any
appropriate email distribution list, news board, newsletter,
or journal, which is in your responsibility.
I apologize for the rather impersonal nature of this memo,
and I hope this will not affect your willingness to assist with
LICS93 publicity.

Thanks very much in advance

Daniel Leivant
LICS Publicity Chair


                   LOGIC IN COMPUTER SCIENCE (LICS)
                   ********************************
                     Eighth Annual IEEE Symposium
                  June 19-23, 1993, Montreal, Canada


             ADVANCE REGISTRATION AND PROGRAM INFORMATION
             ============================================
 (The conference flyer is accessible via anonymous ftp from cs.indiana.edu,
     directory /pub/logic, files lics93.tex, lics93.dvi, lics93.ps etc.)

CONFERENCE OFFICE.
=================
Please address forms, payments and inquiries to:

	LICS93 Secretariat, Conference Office
	McGill University
	550 Sherbrooke Str. West, West Tower, Suite 490
	Montreal, Canada H3A 1B9
      		Phone: (514) 398-3770    Fax: (514) 398-4854
      		Email:  lics93@cs.mcgill.ca

REGISTRATION DESK.
=================

A registration and information desk will be located at the
Stephen Leacock Building, and the Welcome Reception will take
place at Redpath Hall, both on McGill University's main campus.
Entering campus through the McTavish Street entrance (below the
corner of Dr. Penfield) Leacock will be the second building on
your left, and Redpath the first on your right.
The registration desk will operate on:

The desk will operate on:
    * Saturday, June 19: 2-6pm
    * Sunday, June 20: 7:30am-6pm
    * Monday, June 21: 8am-6pm
    * Tuesday, June 22: 8am-6pm
    * Wednesday, June 23: 8-11am


REGISTRATION FEES.
=================
A table of registration fees can be found on the registration form.
The member rate applies to  members of a sponsoring organization
(IEEE Computer Society, ACM, EATCS, ASL), members of the organizing
and program committees, and authors of accepted papers.  The student
rate applies to full time students.  All registration privileges are
extended to the reduced rates.  In the event of cancellation fees will
be refunded, except for a $50 cancelation fee, provided a written
request is received by the conference office by April 30.

Payment of fees must accompany the registration form.  Registrants
may use a charge card (Visa, MasterCard, or American Express) by
filling out the details and signing the appropriate portion of the
registration form.  Canadian and US residents may also send a personal
check or money order, which must be in their national currency.
Other registrants may also send an international money order, which
must be in Canadian dollars.  Checks and money orders should be payable
to "LICS'93-McGill University".

Fees include a 7% federal (GST) tax and a 4% provincial (PST) tax,
which are refundable (except for residents of Canada for GST and
residents of Quebec for PST).  Refund forms will be included in the
registration package.


LODGING.
=======
Blocks of rooms have been reserved at the Shangrila Hotel,
for a pre-tax rate of $96 per night (single or double), and at the
McGill University Royal Victoria College, for a pre-tax rate of $33
per night (single only).  Both are a few minute walk from the conference
site.  To guarantee your reservation a deposit must be made by May 14,
either by using a charge card (filling out the appropriate form in the
registration form), or by contacting the hotel directly.
All accommodation fees should be paid directly to the hotel at check-out time.
For further information, please contact:

	Le Shangrila Hotel
	3407 Peel Str.
	Montreal, Canada H3A 1W7
		Phone: 514-288.4141, 800-361.7791    Fax: 514-288.3021

	McGill Residences
	Royal Victoria College
	3425 University Street
	Montreal, Canada, H3A 1X6
		Phone: 514-398.6378    Fax: 514-398.4455
	
	Montreal Convention & Tourism Bureau
	1555 Peel Street, Room 600
	Montreal, Canada H3A 1X6
		Phone: 514-844.5400    Fax: 514-844.5757

Additionally, a block of suites has been reserved at Le Monfort
at a special eight night rate (June 15th to June 23), ranging
from a studio (bed & sofa-bed) at the rate of C$400 to a two
bedroom apartment at C$725, all including small kitchen and dining area.
This is of particular interest to people attending both RTA (June 16-18)
and LICS (for RTA'93 information: rta93@cs.concordia.ca).
Le Monfort is a few minute walk from the RTA site, and a short
subway ride (or about 20 minute walk) from the LICS site.
Reservations must be made directly with the hotel by May 7:

	Le Monfort (attn. Gisele Gariepy)
	1975, de Maisonneuve Ouest
	Montreal H3H 1K4
		Phone: 514-934.0916    Fax 514-939.2552


AIRPORT INFORMATION.
===================
Domestic and US flights arrive at Dorval Airport.
Buses depart every 20 minutes to the Berri Metro in downtown Montreal,
a 20 minute ride, for a fare of $8.50.  The taxi fare is about $25.
Intercontinental flights arrive at Mirabel Airport, 56 km (35 miles)
from downtown.  There is a frequent bus service to the Berri Metro,
for a fare of $13.  Cab fare may reach $50.


               REGISTRATION AND ACCOMMODATION FORM
               ***********************************

First Name __________________  Last Name ___________________

Affiliation ________________________________________________

Mailing Address _____________________________________________

     _______________________________________________________

     _______________________________________________________

Phone(s) _______________________ Fax: ______________________

E-mail:  ___________________________________________________


RATES.  Fees indicated below are in [Canadian dollars/US dollars].
Please indicate the applicable rate (and currency) by circling
it on the table, and also writing it in.

                through 05.14    from 05.15      on site

Regular	      	   425/340 	  500/400 	 600/480
Member		   375/300 	  450/360 	 550/440
Student 	   200/160 	  250/200 	 300/240


  * Fee: ____________  * Justification: ______________________


HOTEL RESERVATION.   Please mark the desired accommodation:

    * Shangrila  single / double

    * McGill Residences (only single)

    * Arrival: _____________    * Departure: _________________

    * No reservation requested


MODE OF PAYMENT   (Note: Accomodations must be guaranteed by May 14.
                   See REGISTRATION section above.)

Please circle one:

    Check    Money Order    VISA    MC    AmExp

Credit Card Information (if applicable):

    Name on card ________________________________

    Card Number _________________________________

    Expiration date _____________________________


    Signature ___________________________________

Charge card to be used for (please mark the appropriate):

    registration fees / accommodation guarantee / both


                     CONFERENCE PROGRAM
                     ******************
           (All talks at Stephen Leacock Building)


SATURDAY, June 19
=================

REGISTRATION (at Stephen Leacock Bldng)               (2:00-6:00 pm)

WELCOME RECEPTION (at Redpath Hall)                   (5:00-7:00 pm)


SUNDAY, June 20
===============

TUTORIAL (8:30-10:00am) Chair: R. Constable (Cornell)
    Andrew M. Pitts (Cambridge): Bisimulation and co-induction


SESSION 1: TYPES   Chair: M. Abadi (DEC-SRC)          (10:30-12:30)

10:30 The  genericity  theorem  and   the   notion of
      parametricity in the polymorphic lambda-calculus
    Giuseppe Longo (ENS), Kathleen Milsted (DEC-PRL)
    & Sergei Soloviev (Russian Academy of Science)

11:00 Standard  ML  weak polymorphism and imperative constructs,
    My Hoang (Stanford), John Mitchell (Stanford)
    & Ramesh Viswanathan (Stanford)

11:30 A lambda calculus of objects and method specialization,
    John Mitchell (Stanford), Furio Honsell (Udine)
    & Kathleen Fisher (Stanford)

12:00 Strong normalization for second order classical natural deduction,
    Michel Parigot (Paris VII)


HOSTED LUNCH (at the University Center Cafeteria)     (12:30-2:00)


SESSION 2: DEDUCTION    Chair: N. Shankar (SRI)       (2:00-4:00)

2:00 Automated production of traditional proofs for
    constructive geometry theorems,
    Shang-Ching  Chou (Wichita State), Xiao-Shan Gao (Edinburgh)
    & Jing-Zhong Zhang (Wichita State)

2:30 On the  unification  problem for cartesian closed categories,
    Paliath  Narendran (SUNY-Albany), Frank Pfenning (CMU)
    & Richard Statman (CMU)

3:00 Functional unification of higher-order patterns,
    Tobias Nipkow (TU Muenchen)

3:30 Set constraints are the monadic class,
    Leo Bachmair (SUNY-Stony Brook), Harald Ganzinger
    (Max Planck Inst) & Uwe Waldmann (Max Planck Inst)


SESSION 3: SEMANTICS   Chair: P.J. Freyd (U. Penn)   (4:30-6:00)

4:30 Relational properties of recursively defined domains,
     Andrew M. Pitts (Cambridge)

5:00 Full abstraction for a shared variable parallel language,
     Stephen Brookes (CMU)

5:30 A coinduction principle for recursive data types
	based on bisimulation,
     Marcelo P. Fiore (Edinburgh)


BUSINESS MEETING (at Leacock Building)               (8:00-10:00)


MONDAY, June 21
===============

TUTORIAL    Chair: Y. Moschovakis (UCLA)             (8:30-10:00)
    Phokion G. Kolaitis (UC Santa Cruz): Finite-model theory


SESSION 4: MODAL & TEMPORAL LOGICS                   (10:30-12:30)
     Chair: M.Y. Vardi (IBM-Almaden)

10:30 In and out of temporal logic,
     Amir Pnueli (Weizmann Inst) & Lenore Zuck (Yale)

11:00 On completeness of mu-calculus,
     Igor  Walukiewicz (Warsaw)

11:30 On model checking for real-time properties with durations,
     A. Bouajjani (LGI-IMAG),  R. Echahed (LGI-IMAG)
     & J.Sifakis (LGI-IMAG)

12:00 Verifying programs with unreliable channels,
     Parosh Abdulla (Uppsala) & Bengt Jonsson (Uppsala)


LUNCH BREAK                                      (12:30-2:00)


SESSION 5: FINITE-MODEL THEORY                   (2:00-4:00)
     Chair: P.G. Kolaitis (UC Santa Cruz)

2:00 y = 2x vs. y = 3x
     Alexei Stolboushkin (UCLA) &  Damian Niwinski (Warsaw)

2:30 Monadic second-order logic and hypergraph orientation,
     Bruno Courcelle (Bordeaux I)

3:00 Infinitary logics and very sparse random graphs,
     James F. Lynch (Clarkson)

3:30 Asymptotic probabilities of languages with generalized quantifiers,
     Guy Fayolle (INRIA), Stephane Grumbach (INRIA)
     & Christophe Tollu (Paris-Nord)


SESSION 6: LOGIC PROGRAMMING                        (4:30-6:00)
     Chair: D. Miller (U. Penn)

4:30 Compositional analysis for concurrent constraint programming,
     Moreno Falaschi (Padova), Maurizio Gabbrielli (Pisa),
     Kim Marriott (Monash) & Catuscia Palamidessi (Genova)

5:00 Rules of definitional reflection,
     Peter Schroeder-Heister (Tubingen)

5:30 Encoding the calculus of constructions in a higher-order logic,
     Amy Felty (Bell Labs)


CONFERENCE RECEPTION (at Redpath Hall)               (6:00-7:30)

EVENING LECTURE (at Leacock Bldg)                    (8:00-9:00)
     Chair: M. Okada (Concordia)
     Jim Lambek (McGill):
     Programs, grammars and arguments --
     a personal view of some connections between
     computation, language and logic


TUESDAY, June 22
================

INVITED TALK Chair: P. Panangaden (McGill)           (9:00-10:00)
     Jon Barwise (Indiana): Information flow in imperfect channels


SESSION 7: LAMBDA CALCULUS                           (10:30-12:30)
     Chair: S. Abramsky (Imperial Coll)

10:30 A typed pattern calculus,
     Val Breazu-Tannen (U.Penn), Delia Kesner (INRIA/Paris-Sud)
     & Laurence Puel (Paris-Sud)

11:00 Non-determinism in a functional setting,
     C.-H. Luke Ong (Cambridge/Singapore)

11:30 Adequacy for untyped translations of typed lambda-calculi,
     Wesley Phoa (U. of New South Wales)

12:00 Local and asynchronous beta-reduction,
     Vincent Danos (CNRS) & Laurent Regnier (CNRS)


LUNCH BREAK                                           (12:30-2:00)


SESSION 8: COMPLEXITY & DATABASES                     (2:00-4:00)
     Chair: P. Clote (Boston Coll)

2:00 An exponential  separation  between  the  matching
     principle and the pigeonhole principle,
     Paul Beame (U Washington) & Toniann Pitassi (UC San Diego)



2:30 Some desirable conditions for feasible functionals of type 2,
     Anil Seth (Tata Institute)

3:00 Database query languages embedded in the typed lambda calculus,
     Gerd G. Hillebrand (Brown), Paris C. Kanellakis (Brown)
     & Harry G.Mairson (Brandeis)

3:30 Homomorphic tree embeddings and their applications
    to recursive  program optimization,
     V.S. Lakshmanan (Concordia), Karima Ashraf (Concordia)
     & Jiawei Han (Simon Fraser)


SESSION 9: REWRITING    Chair: P. Lescanne (CRIN)      (4:30-6:00)

4:30 The order types of termination orderings on terms,
    strings and multisets,
     Ursula Martin (St.Andrews) & Elizabeth Scott (St.Andrews)

5:00 The unifiability problem in ground AC theories,
     Paliath Narendran (SUNY-Albany)
     & Michael Rusinowitch (INRIA/CRIN)

5:30 Lambek grammars are context free,
     Mati Pentus (Moscow U)


FREE EVENING


WEDNESDAY, June 23
==================

INVITED TALK  Chair: M.Abadi (DEC-SRC)               (8:45-9:45)
    Gordon D.Plotkin (Edinburgh): Type theory and recursion


SESSION 10: CONCURRENCY   Chair: B.Bloom (Cornell)   (10:05-12:35)

10:05 Typing and subtyping for mobile processes,
     Benjamin Pierce (Edinburgh) & Davide Sangiorgi (Edinburgh)

10:35 Decomposability, decidability and axiomatisability for
	bisimulation equivalence on basic parallel processes,
     Soren Christensen (Edinburgh), Yoram Hirshfeld (Edinburgh)
     & Faron Moller (Edinburgh)

11:05 A fully abstract denotational model for higher-order processes,
     M.Hennessy (Sussex)

11:35 Self-synchronization of concurrent processes,
     Lalita Jategaonkar (MIT) & Albert R. Meyer (MIT)

12:05 Bisimulation and open maps,
     Andre Joyal (UQAM Montreal), Mogens Nielsen (Aarhus)
     & Glynn Winskel (Aarhus)


END OF CONFERENCE



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

LICS General Chair: Robert L. Constable

1993 Conference Co-chairs: Mitsuhiro Okada & Prakash Panangaden

1993 Program Chair: Moshe Y. Vardi

Publicity Chair: Daniel Leivant


PROGRAM COMMITTEE:
=================

M. Abadi, S. Abramsky, B. Bloom, P. Clote, P.J. Freyd, D. Harel,
K.G. Larsen, P. Lescanne, D. McAllester, J. Meseguer, D. Miller,
Y. Moschovakis, N. Shankar, C. Talcott, M.Y. Vardi, and P. Wolper.


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

M. Abadi, S. Abramsky, S. Artemov, J. Barwise, M. Blum, A. Borodin,
A. Bundy, S. Buss, E. Clarke, R. Constable (Chair), E. Engeler,
J. Gallier, U. Goltz, Y. Gurevich, S. Hayashi, G. Huet, G. Kahn,
D. Kapur, C. Kirchner, R. Kosaraju, J.W. Klop, P. Kolaitis,
D. Leivant, A.R. Meyer, G. Mints, J. Mitchell, Y. Moschovakis,
M. Okada, P. Panangaden, A. Pitts, G. Plotkin, S. Ronchi della Rocca,
G. Rozenberg, A. Scedrov, D. Scott, J. Tiuryn, M.Y. Vardi, R. de Vrijer.



++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Subject: Re:  Piaget
Date: Mon, 12 Apr 93 13:58:42 EDT
From: barr@triples.Math.McGill.CA (Michael Barr)

Bizarre!  No, I haven't seen nor heard of it.  

I spoke with Aczel, who gave a talk at the recent meeting in New Orleans
I was at.  He has toned down his claims for NWF sets quite a bit and now
only claims that they are useful for intuition.  He does prefer to talk
of sets and classes, where I might prefer an inaccessible, but that is
perfectly harmless as far as I am concerned.

Michael
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Subject: ftp access: Adjoint Char'n of Cat of Sets
Date: April 12,1992
From: Bob Rosebrugh <rrosebrugh@mta.ca>

The paper whose abstract follows is available by anonymous ftp in the directory
pub/papers/rosebrugh   at sun1.mta.ca (138.73.1.12)
as the files 
accs.{dvi,tex}
If you download the latter you need to know that it is in LaTeX and uses the
bibliography file accs.bib and Mike Barr's diagram macros, diagram.tex,
both found in the same directory.  Don't hesitate to contact me if you
experience any difficulties or need ftp instructions.

I will gladly forward a paper copy. If you request one be sure to include a
full postal address.

Bob Rosebrugh
+++++++++++++++++++++++++++++++++++
An adjoint characterization of the category of sets

Robert Rosebrugh and R. J. Wood

Abstract

If a category B with Yoneda embedding Y : B ---> CAT(B^op,set) 
has an adjoint string, U -| V -| W -| X -| Y, then B is equivalent to set.


++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Subject: Upgrade to CTCS
Date: Tue, 13 Apr 93 11:58:07 EDT
From: barr@triples.Math.McGill.CA (Michael Barr)

 
\item[p. 236] (Frank Piessens).  The statement, ``It would be incorrect
to assume in general (although it is true in familiar examples) that
every node of $\Tsc$ is a limit of a diagram in the graph of $\Ssc$'' is
wrong.  The reason is that $\Tsc\op$ is a full subcategory of the
category $\Fun(\Ssc,\Set)$ (to be precise, that should be the free
category generated by the graph underlying $\Ssc$) and every functor is
a colimit of representables and, hence, in $\Tsc$, every functor is a
limit of them.  Thus every object of the theory is a limit of a diagram
built from the objects and arrows of $\Ssc$.
 
\item[p. 387] (Nico Verwer).  The solution to Exercise 4 of 8.3 contains
several errors. The right hand label of the diagram should be $<f,g>$,
the lower left corner of the diagram should be $B$ and the $f\x g$ in
the displayed line that begins $G(X)=\ldots$ should also be $<f,g>$.
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Subject: *** Modulated Bicategories ***
Date: Thu, 15 Apr 93 14:59:15 +1000
From: domv@macadam.mpce.mq.edu.au

                    Paper Preprint Available
                    ========================

The following paper preprint is available for anonymous
FTP from ftp.mpce.mq.edu.au (137.111.216.12) in
/pub/maths/Categories/mod.bicats.ps.Z
The abstract is available as /pub/maths/Categories/mod.bicats.abs

                MODULATED BICATEGORIES.

Aurelio Carboni, Scott Johnson, Ross Street, and Dominic Verity

ABSTRACT:

The concept of regular category has several 2-dimensional analogues
depending upon which special arrows are chosen to mimic monics. Here,
the choice of the conservative arrows, leads to our notion of
faithfully conservative bicategory K in which two-sided discrete
fibrations become the arrows of a bicategory F=DFib(K). While the
homcategories F(B,A) have finite limits, it is important to have
conditions under which these finite ``local'' limits are preserved by
composition (on either side) with arrows of F. In other words, when
are all fibrations in K flat? Novel axioms on K are provided for this,
and we call a bicategory H modulated when H^op is such a K. Thus, we
have {\bf constructed} a proarrow equipment ()_*:H-->M (in the sense
of Wood) with M=F^coop.  Moreover, M is locally finitely cocomplete
and certain collages exist.

In the converse direction, if M is any locally countably cocomplete
bicategory which admits finite collages, then the bicategory M^* of
maps in M is modulated. {Recall that a 1-cell in a bicategory is
called a {\it map\/} when it has a right adjoint.}
---------------------------------------------------------------------------
To fetch and print a copy of the file, use the following procedure:

        % ftp ftp.mpce.mq.edu.au
        Name: anonymous
        Password: <user>@<site.domain>
        ftp> cd /pub/maths/Categories
        ftp> binary
        ftp> get mod.bicats.ps.Z
        ftp> quit
        % uncompress mod.bicats.ps.Z
        % lpr -P<postscript-printer> mod.bicats.ps

If your site does not support the Unix uncompress program, or you
have trouble fetching compressed files, our server can uncompress
the file for you.  Simply fetch mod.bicats.ps instead of mod.bicats.ps.Z.


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

Dominic Verity, Macquarie University, NSW 2109, Australia.
email: domv@macadam.mpce.mq.edu.au

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Subject: Monograph announcement
Date: Thu, 15 Apr 93 15:55:29 +0200
From: curien@dmi.ens.fr

The second, thoroughly revised, edition of my monograph

  Categorical combinators, Sequential algorithms and Functional  

  programming, by P.-L. Curien

just appeared in the series Progress in Theoretical Computer Science,
Birkhauser.

I enclose the contents of the back cover, the table of contents, and
the preface to the second edition, to give an idea of the contents and
of the improvements with respect to the first edition.  Order and
price info are given at the end.

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


BACK COVER

This book is a thoroughly revised edition of a monograph that  appeared
under the same title in 1986 in the Series Research Notes in
Theoretical Computer Science, Pitman.  It presents an approach to the
design and implementation of sequential programming languages based  on
the relationship between lambda-calculus and category theory.

The foundations of a new "categorical" combinatory logic are laid
down. Compilation and evaluation techniques are investigated. A  simple
abstract machine, called the Categorical Abstract Machine, is
presented: it has served as the core of the implementation of the
language CAML, of the ML family, developped at INRIA-Roquencourt and
Ecole Normale Supe'rieure, and first released in 1987.  The main
characteristics of this approach are conceptual simplicity and
compacity, with bearings on portability, efficiency, and correctness
proofs.

A mathematical semantics of sequentiality is proposed, in which
"sequential algorithms" rather than functions are used to interpret
procedures. The theoretical investigation has led to the development
of a programming language, {bold CDS0}, in which basic and functional
types are not differentiated. The evaluation framework is a
demand-driven data flow network. The model of sequential algorithms is
fully abstract with respect to this language: two procedures have the
same denotation if and only if they have the same behaviour.
Background on full abstraction is given.

The new edition covers new results, and introduces new connections, as
suggested by the following non exhaustive list of keywords:  confluence
properties of categorical combinators, explicit substitutions,  control
operations, linear logic, geometry of interaction, strong stability.

-------------------------------------------------
TABLE OF CONTENTS

PREFACE TO THE SECOND EDITION 


PREFACE

TABLE OF DEPENDENCIES

INTRODUCTION 



1. CATEGORICAL COMBINATORS 


	1.1 Introducing categorical combinators 


	1.2 lambda-calculus and untyped categorical combinatory logic  


	1.3 Types and cartesian closed categories
	1.4 From untyped calculus to typed calculus: axiomatizing a 						
	universal type
	1.5 Models of the %lbd%-calculus
	1.6 Equivalences of presentations 


	1.7 Evaluation of categorical terms 


	1.8 Discussion

2. SEQUENTIAL ALGORITHMS 


	2.1 Concrete data structures
	2.2 Representation theorems  


	2.3 Domain equations
	2.4 Sequential functions  


	2.5 Sequential algorithms 


	2.6 The category of concrete data structures and sequential 


	algorithms 


	2.7 Discussion
 


3. CDS0: THE KERNEL OF A FUNCTIONAL LANGUAGE 


	3.1 Declaring concrete data structures
	3.2 The language of constants: states and sequential 


	algorithms 


	3.3 The language of expressions
	3.4 Operational semantics: presentation
	3.5 Operational semantics: the rules of CDS01 


	3.6 Full abstraction for CDS01 


	3.7 Discussion 



4. THE FULL ABSTRACTION PROBLEM 


	4.1 The languages PCF, PCFP and PCFC
	4.2 Sequential algorithms and extensionality: the bicds's
	4.3 Complete bicds's
	4.4 Extensional algorithms and definability
	4.5 Discussion

5. CONCLUSION 



6. MATHEMATICAL PREREQUISITES 



REFERENCES

INDEX OF DEFINITIONS

INDEX OF SYMBOLS

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

PREFACE TO THE SECOND EDITION
  


This book is a revised edition of the monograph which appeared under  

the same title in the series Research Notes in Theoretical Computer  

Science, Pitman, in 1986. In addition to a general effort to improve  

typography, English, and presentation, the main novelty of this  

second edition is the integration of some new material. Part of it is  

mine (mostly jointly with coauthors). Here is brief guide to these  

additions.

- I have augmented the account of categorical combinatory logic with  

a description of the confluence properties of rewriting systems of  

categorical combinators (Hardin, Yokouchi), and of the newly  

developed calculi of explicit substitutions (Abadi, Cardelli, Curien,  

Hardin, Le'vy, and Rios), which are similar in spirit to the  

categorical combinatory logic, but are closer to the syntax of  

%lbd%-calculus (Section 1.2). 


- The study of the full abstraction problem for PCF and extensions of  

it has been enriched with a new full abstraction result: the model of  

sequential algorithms is fully abstract with respect to an extension  

of PCF with a control operator (Cartwright, Felleisen, Curien). An  

order-extensional model of error-sensitive sequential algorithms is  

also fully abstract for a corresponding extension of PCF with a  

control operator and errors (Sections 2.6 and 4.1).

- I suggest that sequential algorithms lend themselves to a  

decomposition of the function spaces that leads to models of linear  

logic (Lamarche, Curien), and that connects sequentiality with games  

(Joyal, Blass, Abramsky) (Sections 2.1 and 2.6).

- There is even more to the connection with linear logic:
the operational semantics of sequential algorithms, formalized in  

Chapter 3, bears striking similarities with the geometry of  

interaction, developed for linear logic by Girard in 1988. In Section  

3.4, I have included a prologue and a picture to help conveying this  

conceptual similarity.

- I include a short description of some results of Bucciarelli and  

Ehrhard, who have proposed a more abstract theory of sequential  

algorithms (Section 2.4), an extensional (but not order-extensional)  

notion of strong stability, that is closed under exponentiation and  

coincides with sequentiality at first order
(Section 2.6), and a method of order-extensional embedding (Section  

4.4).

- These results are reported mostly in the form of exercises. I have  

decorated some exercises with a star to stress that their solution  

represents a significant work. The reader can use them as a quick  

reference to the source papers.

Here are a few other new works that I account for:

- adaptations of abstract environment machines to carry out full  

normalization of %lbd%-terms (Cre'gut, Asperti, Curien) (Section  

1.2);

- a hierarchical coherence theorem whose proof by Lafont gives as a  

side-effect a proof of termination of the execution of simply typed  

terms by the categorical abstract machine (Section 1.3);

- the inability of graph reduction of categorical combinators to  

implement optimal sharing of reductions (Curien, Field, Le'vy)  

(Section 1.7);

- further results on representation theorems for event domains, and  

solutions of domain equations (Droste) (Sections 2.2 and 2.3);
 


- the striking connection between (extensional) sequential algorithms  

and the oracle semantics of higher-order recursion theory developed  

by Kleene in the last years of his scientific career (Section 2.7);

- the works of Brookes and Geva on various approaches to intensional  

continuous semantics (Section 2.7);

- the use of logical relations to obtain a full abstraction result  

for order up to 3 (Sieber) (Sections 4.1 and 4.2).

...

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

To order:

in North America call (201) 348-4033, or write Birkhaeuser,
44 Hartz Way, Secaucus, NJ  07096-2491. 


outside North America, please contact Birkhaeuser Verlag AG,  

Klosterberg 23, CH-4010, Basel, Switzerland. 

FAX 061 271 7666.

Price:  $64.50 (US dollars) (hardcover only)



++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Subject: Categories of relational structures
Date:        Fri, 30 Apr 93 20:31:14 ADT
From: Vaughan Pratt <pratt@CS.Stanford.EDU>

Define a relational structure (A,R) to consist of a set A and a n-ary
relation on A for some ordinal n.  A homomorphism f:(A,R)->(B,S) is a
function f:A->B between the underlying sets of two relational
structures of the same arity, such that f(R) c S.  Write Str_n for the
category of all n-ary relational structures and homomorphisms between
them, and Str for the sum in CAT of Str_n over all ordinals n.

1.  What is the term for the notion of full subcategory of either Str_n
or Str?  Failing that, what would be a suitable term?  Relational
categories?  Categories of relational structures?

Familiar examples of such categories and an upper bound on their
arities include those of groups (3), rings (4), fields (4), lattices
(3), vector spaces over the field K (1+max(|K|,2)), directed graphs
(2), posets (2), and categories (3).

I would expect complete lattices, complete Boolean algebras,
topological spaces, and hypergraphs not to embed in Str_n for any n,
because their structural elements (subsets, e.g. open sets) have no
fixed cardinality bound, unlike n-tuples.  A pointer to a proof of such
nonembedding, or a demonstration of how to embed them, would be greatly
appreciated.  Since the concept is such a natural one, this question
must surely have been looked at before.

2.  What generalizations of Str or Str_n have been considered?

One can make Str a bit more "communicative" by permitting homomorphisms
between dissimilar structures (A,R), (B,S) of respective arities m<n.
Do this by padding out (A,R) to arity n by defining R(n) to be the set
of n-tuples of A whose first m elements satisfy R.  This probably looks
about as useful today as the telephone did in 1879.
