headers
LICS.DATABASE | 3 Apr 1991 22:47
Picon

LICS'91 Program

Date: Wed, 3 Apr 91 02:51:54 EST

                     Sixth Annual IEEE Symposium on 
                   LOGIC IN COMPUTER SCIENCE (LICS'91)
			    July 15-18, 1991
		Vrije Universiteit, Amsterdam, The Netherlands

   Sponsored by the IEEETC on Mathematical Foundations of Computing; CWI
   Amsterdam; and the Vrije Universiteit, Amsterdam; in cooperation with the
   Association for Computing Machinery--SIGACT, the Association for Symbolic
   Logic, and the European Association for Theoretical Computer Science.

      Below is the Technical Program and Conference Events for LICS 91.
      Registration, hotel and travel information will be broadcasted
      within a few days.  If you expect to attend LICS 91, the organizers
      would be grateful if you would immediately email the following reply
      to   lics91@...  ( *NOT* to the sender of the present message):
	             I HOPE TO ATTEND LICS 91 IN AMSTERDAM.
      In case price is a factor, note that early registration for authors and
      members of sponsoring organizations is expected to be about NLG 375
      ($215) including 6+ meals, and middle price single hotel room per night
      is about NLG 100 ($60).

			 LICS '91 ADVANCE PROGRAM

CONFERENCE EVENTS
=================
SUNDAY WELCOME AND REGISTRATION.  On July 14 there will be a welcome 
reception from 19:00 to 22:00, at the  Grand Caf'e Waterloo.
The Waterloo is on the Opera and City Hall complex, at Zwanenburgwal 15.
(Continue reading)

Permalink | Reply | 0 comments |
headers
mwpl | 8 Apr 1991 15:41
Picon
Picon

mwpl@...

Date: Mon, 08 Apr 91 07:53:27 -0400

             Montreal Workshop on Programming Languages
      -ALGEBRAIC AND LOGICAL APPROACHES IN PROGRAMMING LANGUAGES- 
                        April 29-30, 1991
                            Montreal

Organized by the Montreal Programming Languages Group in cooperation
with the Montreal Interuniversity Category Theory-Logic Seminar and 
the Queen's Workshop on Programming Languages.

Supported by the Center for Pattern Recognition and Machine Intelligence 
of Montreal and the Ministere d'enseignement superieure et recherche de Quebec 
under the Quebec-Ontario Cooperation Program.

The purpose of the workshop is to discuss together the various research
activities in programming languages and related fields from some
universities and research laboratories in Quebec, Ontario and northern 
New York State. Participation from other area is also welcome.  Our intention
is to hold workshops in this series twice a year in cooperation with
several research groups in the Quebec and Ontario area.

Algebraic and logical approaches in programming languages are becoming 
increasingly important both in the theoretical and the practical levels.
The first workshop will be focused on algebraic and logical aspects of 
programming languages, including new generation programming language design, 
semantics of programming languages, algebraic specification languages,
formal program verification, logical framework of the object-oriented paradigm,
and other issues related to algebraic or logical approaches to language theory.
(Continue reading)

Permalink | Reply | 0 comments |
headers
LICS | 10 Apr 1991 04:10
Picon

LICS'91 Registration

                         LICS '91 REGISTRATION
                              AND PROGRAM

                     Sixth Annual IEEE Symposium on 
                   LOGIC IN COMPUTER SCIENCE (LICS '91)
			    July 15-18, 1991
		Vrije Universiteit, Amsterdam, The Netherlands

   Sponsored by the IEEETC on Mathematical Foundations of Computing, CWI
   Amsterdam, and the Vrije Universiteit, Amsterdam, in cooperation with the
   Association for Computing Machinery--SIGACT, the Association for Symbolic
   Logic, and the European Association for Theoretical Computer Science.

[We apologize if you receive a bothersome number of copies of LICS
announcements. We are trying to coordinate our broadcasts among the
multiple mail lists and newsgroups reaching the LICS community, but these
efforts may not be effective for a while.]

GENERAL INFORMATION
===================
Register and reserve hotel rooms by sending the completed form below by
EMAIL to
	  lics91@... <LICS'91 Secretariat>
or by REGULAR MAIL to:
          LICS'91 Secretariat
          c/o CWI
          Kruislaan 413
          P.O. Box 4079
          1009 AB Amsterdam
          The Netherlands
(Continue reading)

Permalink | Reply | 0 comments |
headers
Clem Baker-Finch | 10 Apr 1991 04:31
Picon
Picon

monotonic subtype relations?

Date: Wed, 10 Apr 91 10:38:53 EST

One of my students (David Wright) is looking at type inference including
needed reduction information (see Tapsoft 1991).  An interesting feature of 
the work is that there is a 'subtype' relation that is naturally covariant 
in the sense that a leq a' & b leq b' implies a->b leq a'->b'.  (The usual 
implication is that a'->b leq a->b'.)  
It would seem to follow that the 'simple semantics' is inappropriate
for this type system.  I (we) would appreciate any pointers to any relevant
papers that readers may be aware of that may help us develop the 'right'
semantics, or indeed, any references to work involving such monotonic type
relations.  Suggestions most welcome.

--

-- 
Clem Baker-Finch			AARNet: clem@...
Information Sciences & Engineering	Phone:  +61 6 2522408
University of Canberra			Fax:    +61 6 2522191
PO Box 1, Belconnen
A.C.T.  Australia   2616
Permalink | Reply | 0 comments |
headers
John.Reynolds | 10 Apr 1991 18:38
Picon

Re: monotonic subtype relations?

To: Clem Baker-Finch <clem@...>
Cc: types@...
Date: Wed, 10 Apr 91 10:02:34 EDT

In Dana Scott's work, there are several notions of "subdomain" that may
fit your needs.  A retraction pair <f,g> from a domain D to a domain E
consists of continuous functions f from D to E and g from E to D
such that f;g is the identity on D. (I use semicolons for composition
in diagrammatic order.)  If g;f approximates the identity on E, then
the retraction pair is called a projection pair; if the identity on E
approximates g;f then the retraction pair is called a closure pair.

If <f,g> is a retraction (projection, closure) pair from D to E and
<f',g'> is a retraction (projection, closure) pair from D' to E' then
<f",g"> is a retraction (projection, closure) pair from D->D' to E->E',
where f"(h) = g;h;f' and g"(h) = f;h;g'.

Thus one could give a semantics to a subtyping relation where -> is 
monotonic in both arguments by using a functor from the preorder of
types to the category of retraction pairs (or either of its subcategories
of projection or closure pairs).  Informally, one interprets "a is a
subtype of b" as "There is a retraction pair from the domain denoted by a
to the domain denoted by b".

I hope this helps. -- John Reynolds
Permalink | Reply | 0 comments |
headers
kim | 11 Apr 1991 04:15
Picon

Re: monotonic subtype relations?

To: clem@..., John.Reynolds <at> proof.ergo.cs.cmu.edu
Cc: types@...
Date: Wed, 10 Apr 91 18:53:15 PDT

It wasn't clear from the original request whether the notion of "subtype"
referred to was the notion of subtype treated in object oriented
programming.  John Reynold's response (very carefully) referred to the
notion of "subdomain" rather than "subtype".  In case the original request
really had to do with the object-oriented notion, let me put in a strong
caution that the OOL notion of "subtype" is usually quite distinct from a
notion of ordering used, for example, to find fixed points or solve domain
equations.  For instance, the ordering of types in the finitary projection
model of the second order lambda calculus seems to have no relevance (alas!)
to the notions of subtype for OOL's.  If such a model were to be extended
to support subtypes, an entirely different ordering would be required for
the subtype hierarchy.

If the original enquiry had nothing to do with OOL's, ignore this caution.
Otherwise, beware!

	Kim Bruce
Permalink | Reply | 0 comments |
headers
C Barry Jay | 24 Apr 1991 17:30
Picon

Categorial View of Loop Invariants

Date: Wed, 24 Apr 91 11:12:27 bst

Program loops have a very simple categorical interpretation, as loop
diagrams, i.e. as diagrams with one object C and one morphism f,
necessarily an endomorphism of C.

			--
		      /    \
		     |      |
		     |      \/ 
		     |      
		   f |      C
		     |    
		     |      |
		      \    /
		        --

Of course, the limit of the loop is its fixpoints. The colimit,
however, is even more interesting. A cocone for the diagram is a
morphism g:C-->Q such that f;g = g. That is, an *invariant* for the
loop. Thus the colimit is the universal invariant of the loop. 

Definition 
A loop *converges* if it has an object of invariants Inv(f)
which is also an object of fixpoints such that the canonical composite

		Inv(f) --> C --> Inv(f)

is the identity.
(Continue reading)

Permalink | Reply | 0 comments |

Gmane