headers
Pierre Lescanne | 5 Jul 1990 10:37
Picon

ALGEBRAIC AND LOGIC PROGRAMMING

Date: Wed, 4 Jul 90 17:53:33 +0200

      	          Second International Conference on

    	 	   ALGEBRAIC AND LOGIC PROGRAMMING

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

	 	Nancy (France), October 1st-3rd, 1990

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

                Organized by CRIN and INRIA-Lorraine

            Sponsored by CNRS, INRIA and Nancy Universities

                with the financial support from:

		Conseil Regional de Lorraine
		Conseil General de Meurthe et Moselle
		District de l'Agglomeration Nanceienne
		Universite de Nancy I
		Universite de Nancy II
		Institut National Polytechnique de Lorraine
		Universite de Wu"rzburg
		Mairie de Nancy

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

			SCIENTIFIC PROGRAM
(Continue reading)

Permalink | Reply | 0 comments |
headers
Paul Taylor | 12 Jul 1990 20:51
Picon

Commutative Diagrams in La/TeX

Date: Thu, 12 Jul 90 11:45:15 BST

A new version of my commutative diagrams package is now available.  Users
of the version released last September will know that it uses a matrix
syntax for the objects and morphisms, and is able to stretch horizontal
arrows to meet the objects at the endpoints. The new version is also able
to stretch verticals, and the diagonals have been re-worked.

The following produces a cube.
$$\diagram
     A'   &        &\rArr^{f'}&           &      B'     &       &         \\
          & \SE_a  &          &           & \vLine^{h'} & \SE_b &         \\
\dArr^{g'}&        &     A    &  \rArr_f  &    \HonV    &       &   B     \\
          &        & \dArr^g  &           &    \dArr    &       &         \\
     C'   & \hLine & \VonH    & \rArr^{k'}&      D'     &       & \dArr_h \\
          & \SE_c  &          &           &             & \SE_d &         \\
          &        &     C    &           &   \rArr^k   &       &   D     \\
\enddiagram$$

I shall dispatch electronic copies of the package & manual just before
I depart for the International Category Meeting in Italy (22-27 July)
(to allow for last minute bug-fixes while I print my own papers!).
Known past users should get it automatically, but to be sure, please
email me, including the word "diagrams" in your subject line.

Paul Taylor, Dept. of Computing, Imperial College, London SW7 2BZ, UK
email   pt@...   pt%ic.doc <at> ukacrl   or   ...!mcvax!ukc!icdoc!pt
phone +44 71 589 5111 x 5057 fax +44 71 581 8024

*************** PS LONDON PHONE NUMBERS HAVE CHANGED *******************
(Continue reading)

Permalink | Reply | 0 comments |
headers
Philip Wadler | 14 Jul 1990 00:01
Picon

Greatest fixpoints have existential types

Date: Fri, 13 Jul 90 19:12:44 BST

Hagino wrote a very nice paper on adding least and greatest fixpoints
of covariant functors explicitly to simply typed lambda calculus (LNCS
238).  He mentions that it is possible to code least fixpoints directly
in polymorphic lambda calculus, and states that he doesn't know whether
it is possible to similarly code greatest fixpoints.

Least fixpoint are coded in polymorphic lambda calculus by
the formula

	Lfix X. T(X)  =  All X. (T(X) -> X) -> X

where Lfix is the least fixpoint and T is a covariant functor (or,
equivalently, a type where X appears only in positive positions).  This
is not always a true least fixpoint, but will be so in certain models
(e.g., those satisfying parametricity).

Similarly, we can make the coding

	Gfix X. T(X)  =  Exists X. (X -> T(X)) * X

where Gfix is the greatest fixpoint and T is still a covariant
functor.  Is this known?  It seems an obvious dual of the least
fixpoint result, but Hagino seems unaware of it.  

For example, streams of integers are yielded by the greatest fixpoint
of T(X) = Int * X.  The formula above instantiates to

	   IntStream
(Continue reading)

Permalink | Reply | 0 comments |
headers
Ryu Hasegawa | 17 Jul 1990 17:21
Picon
Picon

Response to Wadler: Greatest fixpoints have existential types

Date: Mon, 16 Jul 90 20:27:07 JST

> Similarly, we can make the coding
> 
> 	Gfix X. T(X)  =  Exists X. (X -> T(X)) * X
> 
> where Gfix is the greatest fixpoint and T is still a covariant
> functor.  Is this known?

See [1][3].

In fact, in the models satisfying Reynolds' parametricity, Gfix X. T(X) is
a terminal fixed point of T, i.e., a terminal object of the category of
T-coalgebras, as well as Lfix X. T(X) is an initial fixed point ([1], [2]).
Moreover, parametricity is partially a necessary condition for the
existence of such fixed points.  These results are used to show that in
the category of pers, every realizable endofunctor has initial and
terminal fixed points [2].

R. Hasegawa

[1] R. Hasegawa (89) Parametric polymorphism and recursive type
 definitions, Master Thesis, RIMS, Kyoto University.
[2] R. Hasegawa (90) Categorical data types in parametric
 polymorphism, in preparation.
[3] G.C. Wraith (89) A note on categorical datatypes, LNCS 389.
Permalink | Reply | 0 comments |
headers
Stephen.Brookes | 17 Jul 1990 22:42
Picon

Call for papers: MFPS91

Date: Tue, 17 Jul 90 13:51:09 EDT
To: CMU-THEORYNET@..., logic <at> theory.lcs.mit.edu,
        types@...

			CALL FOR PAPERS: MFPS91
		Mathematical Foundations of Programming Semantics

			Carnegie Mellon University
			Pittsburgh, Pennsylvania
			  March 25--28, 1991

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 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

Papers are solicited on topics related to programming language semantics, 
including:
(Continue reading)

Permalink | Reply | 0 comments |
headers
Gerard Huet | 20 Jul 1990 12:37
Picon
Picon

Proceedings on Logical Frameworks: available online

Date: Thu, 19 Jul 90 22:19:19 +0200
To: meyer@...

Workshop on Logical Frameworks : Proceedings available

The Proceedings of the ESPRIT Basic Research Action ``Logical Frameworks''
First Annual Workshop, held in Sophia-Antipolis May 7-11 1990
are now freely available by anonymous ftp. 

This 500-pages volume contains 31 contributions, most of them original
research articles.

Connect by : 
ftp nuri.inria.fr

Name: ftp
Password: anonymous
cd esprit/bra/lf
dir

You will find there a README file, a compressed postscript file book.ps.Z,
and also a book.dvi and associated special ps files screen1.ps and screen2.ps,
if you want to use your own dvips translator.

Electronically publishing yours,
Gerard Huet
Permalink | Reply | 0 comments |
headers
David M. Jones | 27 Jul 1990 23:02
Picon

Proceedings on Logical Frameworks: available online

(In response to a suggestion from Mitch Wand re Huet's announcement of
20 Jul 90--TYPES MODERATOR)

> Workshop on Logical Frameworks : Proceedings available
>
> The Proceedings of the ESPRIT Basic Research Action ``Logical Frameworks''
> First Annual Workshop, held in Sophia-Antipolis May 7-11 1990
> are now freely available by anonymous ftp. 
>
> This 500-pages volume contains 31 contributions, most of them original
> research articles.

This is also now available via anonymous ftp from theory.lcs.mit.edu
(internet address 18.52.0.92) in the directory pub/lf.  Log in with
the username "anonymous."

This directory also contains a file called "contents.txt," which
contains the contents of the volume in ascii format.

Thanks are due to David Wald for his efforts in making this available.

David M. Jones
MIT Lab for Computer Science
Administrator, {types,logic,concurrency} <at> theory.lcs.mit.edu
Permalink | Reply | 0 comments |

Gmane