Date: Mon, 4 Jul 1994 11:48:49 +0500 (GMT+4:00)
Subject: Computing: the Australian Theory Seminar (CATS)
Date: Mon, 4 Jul 1994 10:39:19 +1000
From: Barry Jay
Computing: the Australian Theory Seminar (CATS)
Sydney
17th-19th December, 1994
PRELIMINARY ANNOUNCEMENT
CATS will be open to all aspects of the theory of computer science. It
will provide an opportunity for the scattered community of computing
theorists in Australia and New Zealand to meet and exchange views in
an informal setting. The following people have already expressed an
interest in coming.
Robin Cockett (Calgary)
Eugenio Moggi (Genoa)
Maurice Nivat (France)
Phil Wadler (Glasgow)
The format would be informal, with an easy
balance between lectures and discussions:
registration costs will be kept low.
Please reply NOW if you are interested in
coming. Further details will be supplied when
approximate numbers can be gauged.
Please distribute this announcement widely.
Barry Jay
University of Technology, Sydney
Australia
cbj@socs.uts.edu.au
Date: Tue, 5 Jul 1994 08:52:38 +0500 (GMT+4:00)
Subject: Re: Birkhoff variety theorem
Date: Mon, 4 Jul 94 09:01:23 EDT
From: Michael Barr
I have been away and then too busy to examine my mail in detail. I don't
think I have such a result. However, it is likely that John Power's
thesis has something on that. He is in Edinburgh, but is aliased on this
machine[moderator note: `this machine'=`triples.math.mcgill.ca'], so you can
write him here.
Date: Tue, 5 Jul 1994 08:54:41 +0500 (GMT+4:00)
Subject: Categorical completeness results for the simply-typed lambda calculus.
Date: Mon, 04 Jul 94 18:35:50 +0100
From: Alex Simpson
I would like to know if the results below are folklore. They don't
seem to be, as some recent papers have given lengthy proofs of special
cases. On the other hand, they do follow rather easily from an old result
due to Statman.
The results concern two categorical notions of completeness for
beta-eta conversion relative to the interpretation of the simply-typed
lambda-calculus in cartesian closed categories.
Let C be any CCC (not necessarily with finite limits).
Let I_X be the initial CCC generated by a nonempty set X of objects.
We say that beta-eta conversion has a COMPLETE INTERPRETATION IN C
if there is a faithful CC-functor from I_X to C.
We say that beta-eta conversion is COMPLETE FOR C if the class of all
CC-functors from I_X to C is collectively faithful.
(REMARK. These two definitions do not depend upon X as there is a
faithful CC-functor from C_X to C_1, where 1 is a singleton set.)
EXAMPLES. One category in which beta-eta conversion has a complete
interpretation is the category of sets. (This essentially follows from
Friedman's completeness theorem. The inclusion of product types makes
no significant difference. This latter remark also applies below, e.g.
to the quoted Statman theorem.) It is clear that if beta-eta
conversion has a complete interpretation in any C then it is also
complete for C. The converse does not hold: the category of finite
sets is complete but has no complete interpretation. (That it has no
complete interpretation was observed by Friedman. That it is complete
essentially follows from the Plotkin/Statman finite model theorem.)
Finally, for a trivial example of a C for which beta-eta conversion is
not complete, take C to be any cartesian closed preorder.
The results give necessary and sufficient conditions on C for the
two forms of completeness to hold.
THEOREM 1. Beta-eta conversion has a complete interpretation in C iff
C has an endomorphism all of whose iterates are distinct.
THEOREM 2. Beta-eta conversion is complete for C iff C is not a preorder.
Just some brief comments on the proofs. The stronger result is
Theorem 1. Theorem 2 can be derived from it by showing that if C is
not a preorder then C^omega (the countably infinite power of C) has a
"non-repeating" endomorphism as required by Theorem 1. Theorem 2 can
also be proved by mimicking the full type hierarchy over a finite set
within C, or alternatively by using Statman's characterization of
beta-eta conversion as a maximal congruence relation on closed terms
satisfying "typical ambiguity".
Theorem 1 is proved using a different Statman result. We use sigma to
range over types defined using exponentials and finite products from
one base type, 0. We use L,M,N to range over closed terms in the
simply-typed lambda-calculus with types as above. We use =be for
beta-eta equality between terms.
Define the type T = (0 -> 0 -> 0) -> (0 ->0).
THEOREM (Statman [1]). For any sigma there is an L of type sigma -> T
such that, for all M, N of type sigma, M =be N iff L(M) =be L(N).
To prove Theorem 1, let a: A --> A be a non-repeating endomorphism
in C. One defines a CC-functor, F, from I_{0} to C by setting:
F(0) = (A -> A) -> (A -> A).
One can show that F is faithful on the hom-set I_{0}(1,T) (by
encoding binary trees as Church numerals in F(0)). It follows
from Statman's theorem above that F is faithful.
[1] Statman, R.
On the existence of closed terms in the typed lambda-calculus I.
In Hindley, J. R. and Seldin, J. P. eds.
To H. B. Curry Essays on Combinatory Logic, Lambda Calculus and
Formalism.
Academic Press.
1980.
-----------------------------------------------------------------------------
Alex Simpson email: Alex.Simpson@dcs.ed.ac.uk
LFCS, Dept. of Computer Science,
University of Edinburgh,
Edinburgh EH9 3JZ, UK. Tel: +44 (0)31 650 5113
Date: Tue, 5 Jul 1994 22:18:48 +0500 (GMT+4:00)
Subject: ANNOUNCE: XY-pic version 2.11 released...
Date: Tue, 5 Jul 1994 13:45:28 +0200
From: kris@diku.dk
Dear CATEGORY THEORY COMMUNITY,
[Thank you for all the positive replies ... so this time I'll only ask
those who do NOT wish news about XY-pic or who get it from other
sources to send me an email saying so :-]
This is to announce yet another BUG FIX release of my DIAGRAM DRAWING
PACKAGE, XY-pic: version 2.11. It fixes the following user visible
bugs in version 2.10:
* Arrow tips were reversed in a few cases (thanks to Clemens Beckstein
for finding this (also)).
* Repeated labels on arrows now works.
* The PostScript backend sometimes did curves wrong; this is fixed.
Futhermore it adds a new `Graph Combinator feature' which is specially
designed for enterting diagrams with graph structure. Please test it
and comment on it.
Please retrieve the new version by anonymous ftp from
ftp.diku.dk : /diku/users/kris/TeX
ftp.mpce.mq.edu.au : /pub/maths/TeX
or the CTAN `macros/generic/diagrams/xypic' mirror which will be up to
date in a day or so.
Regards,
Kristoffer Rose
--
Kristoffer Ho/gsbro ROSE Internet: kris@diku.dk
DIKU, U of Copenhagen, Universitetsparken 1, 2100 Ko/benhavn O/, DANMARK
phone: +45 35321400 direct: +45 35321420 fax: +45 35321401
--
W3 home
Date: Wed, 6 Jul 1994 21:48:51 +0500 (GMT+4:00)
Subject: Re: Categorical completeness results for the simply-typed lambda calculus.
Date: Wed, 6 Jul 94 14:25:55 EDT
From: Djordje Cubric
I would like to make ``a point of an empty set'' and say that Friedman's
completeness theorem for typed lambda calculus (with appropriate changes)
implies the completeness result for free cartesian closed categories (as
mentioned in a recent posting of Alex Simpson) provided that one proves
first that in a free ccc all objects have a global support. One way to do
that is to prove the confluence for the appropriate system of reductions.
Some of the recent papers were dealing with these reductions.
One can see that the completeness holds even when the free ccc has also free
arrows among freely generated types.
Djordje Cubric
Date: Thu, 7 Jul 1994 11:24:43 +0500 (GMT+4:00)
Subject: Revised version of Acyclic models
Date: Thu, 7 Jul 94 09:02:39 EDT
From: Michael Barr
A totally revised version of Acyclic models is now available for ftp
on my directory on triples. .tex, .dvi and .ps versions are there.
Michael
Date: Thu, 7 Jul 1994 21:51:43 +0500 (GMT+4:00)
Subject: Re: Empty types and typed lambda calculus
Date: Thu, 07 Jul 94 09:37:26 -0700
From: "John C. Mitchell"
We looked into this kind of thing about seven or eight years ago. See
@inproceedings(
mmms87, author="A. R. Meyer and J. C. Mitchell and E. Moggi and R. Statman",
Key="MMMS 87",
Title="Empty types in polymorphic lambda calculus",
Booktitle="Proc. 14th ACM Symp. on Principles of
Programming Languages",
Month="January",Year="1987",
pages="253-262",
Note="Reprinted with minor revisions in
{\it Logical Foundations of Functional Programming,}
ed. G. Huet, Addison-Wesley (1990) 273--284.")
@article(
mm87, author="Mitchell, J.C. and Moggi, E.",
Title="Kripke-style models for typed lambda calculus",
Journal="Ann. Pure and Applied Logic",
Volume="51",Year="1991",
pages="99--124",
Note="Preliminary version in
{\it Proc. IEEE Symp. on Logic in Computer Science,} 1987, pages
303--314.")
@incollection(
MitchScott,Author="Mitchell, J.C. and Scott, P.J.",
Title="Typed lambda calculus and cartesian closed
categories",
Booktitle="Categories in Computer Science and
Logic, Proc. Summer Research Conference,
Boulder, Colorado, June, 1987",
Series="Contemporary Mathematics",
volume="92",
publisher="Amer. Math. Society",
editors="J.W. Gray and A. Scedrov",
Year="1989",
pages="301-316")
Friedman's completeness theorem is completeness of beta,eta for
full classical model (i.e., Set). Deductive completeness fails
for Set and for models (interpretations into categories) where
every type (every object named by a type expression) is required
to be non-empty (have a global element). I tried to clarify this
in my book (still to appear). If anyone is seriously interested,
I could email the appropriate sections of the book.
John Mitchell
Date: Mon, 11 Jul 1994 21:39:03 +0500 (GMT+4:00)
Subject: Conference: Category Theory and Computer Science (CTCS)
Date: Mon, 11 Jul 94 11:39:36 BST
From: David Rydeheard
Preliminary Announcement and Call for Papers
------------------------------------------------------------------------
CATEGORY THEORY AND COMPUTER SCIENCE
CTCS-6
7th-11th August 1995
University of Cambridge, UK.
------------------------------------------------------------------------
The sixth of the biennial conferences on Category Theory and Computer Science
is to be held in Cambridge in 1995, in conjunction with the third Cambridge
Summer Meeting in Category Theory.
The purpose of the conference series is the advancement of the foundations
of computing using the tools of category theory, algebra, geometry and logic.
Whilst the emphasis is upon applications of category theory, it is recognised
that the area is highly interdisciplinary and the organising committee welcomes
submissions in related areas. Topics central to the conference include:
Models of computation Program logics and specification
Type theory and its semantics Domain theory
Linear logic and its applications Categorical programming
Submissions purely on category theory are also acceptable as long as the
applicability to computing is evident.
Previous meetings have been held in Guildford (Surrey), Edinburgh,
Manchester, Paris and Amsterdam.
It is anticipated that the proceedings will be published by Springer in the
LNCS series.
IMPORTANT DATES
Submission of papers February 1, 1995
Notification of acceptance April 14, 1995
Final papers due June 1, 1995
SUBMISSION OF PAPERS.
Authors should send 5 hard copies of a draft paper (maximum of 20 pages) to
Dr. David Pitt,
Department of Mathematical and Computing Sciences,
University of Surrey,
Guildford, Surrey, GU2 5XH,
United Kingdom.
LOCAL ARRANGEMENTS
Dr. Peter Johnstone,
Department of Pure Mathematics and Mathematical Statistics,
16 Mill Lane,
Cambridge, CB2 1SB,
United Kingdom.
Registration forms for the joint conference will be available nearer to the
date.
Organising and programme committee:
S. Abramsky, P.-L. Curien, P. Dybjer, P. Johnstone, G. Longo, G. Mints,
J. Mitchell, E. Moggi, D. Pitt, A. Pitts, A. Poigne, D. Rydeheard,
F-J. de Vries, E. Wagner.
-------------------------------------------------------------------------------
Date: Tue, 19 Jul 1994 13:38:24 +0500 (GMT+4:00)
Subject: Re: Anouncement of Preprints
Date: Tue, 19 Jul 1994 16:33:59 +1000
From: Murray Adelman
I have mounted four papers by John Corbett and myself that attempt to
use sheaf theory to interpret Quantum Logic (or our version thereof)
on the Sydney University ftp site.
They are called
Adelman-Corbett.ps ---Long with a lot of expository material for
physicists.
comparison.ps---Attempts to compare Birkhoff and vonNeumann Quantum
logic to the internal logic of the category of sheaves over state
space
newpaper.ps--- Attempts to show how continuous data can become
discrete data via the global sections functor
heidelberg.ps---Derives a formula for interference of particles that
allows more of the configuration of the experiment to be parametrized
than the usual Hilbert Space description.
The union of heidelberg.ps and comparison.ps approximates (and perhaps
supersedes) Adelman-Corbett.ps which is somewhat older.
They can be obtained by anonymous ftp from
maths.su.oz.au
in the directory
sydcat/papers/murray
Regards,
Murray
Date: Tue, 19 Jul 1994 13:37:10 +0500 (GMT+4:00)
Subject: E-M factorization system question
Date: Mon, 18 Jul 1994 20:35:02 -0700
From: "William H. Rowan"
I am working on a construction which, given a category with an E-M
factorization system (such as onto-oneone functions in the category of sets
or universal algebras of a given type) provides an embedding
F:A --> B
where A is the given category, and F embeds A fully into B. B also has an
E-M factorization system. However, if a is an object of A, then the e's of
Fa are exactly all filters in the lattice of e's of a in A, and the m's of
Fa are exactly all filters in the lattice of m's of a in A.
The question, of course, is, has this been done by anyone before and if so,
please provide a reference to that work.
whr
Date: Tue, 26 Jul 1994 09:07:58 +0500 (GMT+4:00)
Subject: New edition of "Category Theory for Computing Science"
Date: Mon, 25 Jul 1994 14:13:54 -0400
From: "Charles F. Wells"
We are revising our text, "Category Theory for Computing
Science", for its second edition. We would appreciate any
comments or suggestions concerning this revision, including
papers and books we should refer to, new topics we should
include, and topics we could delete. Please reply to either of
us.
Michael Barr Charles Wells
barr@triples.math.mcgill.ca cfw2@po.cwru.edu
--
Charles Wells, Department of Mathematics, Case Western Reserve University
10900 Euclid Avenue, Cleveland OH 44106-7058, USA
Phone 216 368 2880 or 216 774 1926
FAX 216 368 5163
Date: Tue, 26 Jul 1994 09:03:03 +0500 (GMT+4:00)
Subject: characterization of geometric morphisms of the form Pi_I ??
Date: Wed, 20 Jul 94 20:32:52 +0200
From: Thomas Streicher
I would like to know whether somebody knows of an abstract
characterization of those geometric morphisms (between elementary
toposes) which are of the form Pi_I : E/I -> E for some I in E ?
My - maybe misleading - intuition is that a topos is a generalized
locale and the functor I* : E -> E/I corresponds to the locale
morphisms corresponding to open subspace inclusions.
(If L is a locale and x is in L then the mapping y |-> x inf y
from L to { z : L | z less or equal x } is the locale
morphism corresponding to the open subspace inclusion of the open
subset given by x into the space given by L).
Maybe it is also wrong to think of a topos simply as generalized
locale and that the "generalized locale" is given by the fibration
Sub(E) -> E and not by the fibration cod : Map(E) -> E . What I
know about open geometric morphisms seems to confirm this latter
viewpoint.
So I am a bit confused and would appreciate any hints !
Thomas Streicher
Date: Tue, 26 Jul 1994 09:13:08 +0500 (GMT+4:00)
Subject: Papers
Date: Sat, 23 Jul 1994 11:53:22 +1000
From: Murray Adelman
There seems to be some problem obtaining the papers that I announced a
few days ago. I have put them in a second location
ftp.mpce.mq.edu.au
in the directory
/pub/maths/murray
(This is more patriotic, as it is the Macquarie University server
instead of the Sydney University server :-)
Sorry for the inconvenience.
Murray
Date: Tue, 26 Jul 1994 09:05:46 +0500 (GMT+4:00)
Subject: second call for papers, TLCA
Date: Thu, 21 Jul 1994 14:16:59 +0000
From: Philippa Gardner
Please find enclosed the second call for papers for TLCA'95. I
apologise to those who receive many copies of this announcement.
Philippa Gardner
---------------------------------------------------------------
Second Call for Papers, TLCA
International Conference on Typed Lambda Calculi and Applications
April 10--12, 1995, Edinburgh, Scotland
The second international conference on Typed Lambda Calculi and
Applications will be held April 10--12, 1995, at Edinburgh in Scotland.
The conference aims at providing a forum for the presentation and
discussion of recent research in the following areas:
Proof theory of type systems
Logic and type systems
Typed lambda calculi as models of (higher order) computation
Semantics of type systems
Proof verification via type systems
Type systems of programming languages
Typed term rewriting systems
The program of TLCA will consist of about 30 selected presentations in
plenary sessions. The program committee for TLCA is chaired by
M. Dezani and has the following members:
H. Barendregt (Catholic University of Nijmegen)
M. Dezani (Chairperson, University of Turin)
J-Y. Girard (University of Marseilles)
R. Hindley (University of Swansea)
F. Honsell (University of Udine)
J. W. Klop (CWI)
G. Longo (ENS)
A. Meyer (MIT)
G. Plotkin (University of Edinburgh)
P. Scott (University of Ottawa)
J. Smith (University of Gothenburg/Chalmers)
J. Tiuryn (University of Warsaw)
Call for Papers
Original contributions are solicited for TLCA; they should be sent to the
conference secretariat. Electronic submission (PostScript only) is
preferred; hard copy (6 copies required) will also be accepted. Papers
should be clearly written and allow the program committee to assess the
merits of the work. References and comparisons with related work
should be included. Papers should not exceed 15 standard pages and
should be accompanied by a one-page abstract. The deadline for
submissions is September 8, 1994. Authors will receive notification of
acceptance by November 12, 1994. Definitive versions of papers will
be due December 15, 1994.
Proceedings
It is intended to publish the accepted papers as a volume of the Springer
Verlag Lecture Notes in Computer Science series.
Organizing Committee
G. Cleland, P. Gardner, M. Lekuse, G. Plotkin (University of
Edinburgh)
Important Dates
Sept. 8, 1994 Deadline for submissions
Nov. 12, 1994 Notification of acceptance
Dec. 15, 1994 Final version of paper
April 10, 1995 TLCA
TLCA Secretariat
TLCA Secretariat
Professor M. Dezani
Universita di Torino
Dipartimento di Informatica
Corso Svizzera, 185
10149 Torino
ITALY
Tel: 39-11-7429232 Fax: 39-11-751603
Email: dezani@di.unito.it
Lambda-Calculus Network Meeting
Participants of TLCA are welcome to attend a Lambda-Calculus
Network Meeting to be held immediately before the conference.
-------------------------------------------------------------
\documentstyle{article}
\parindent 0cm
\pagestyle{empty}
\textwidth 18cm
\textheight 28cm
\topmargin -2.5cm
\oddsidemargin -1.2cm
\evensidemargin 0cm
\begin{document}
\begin{center}
{\LARGE Second Call for Papers} \end{center}
\smallskip
\begin{center}
{\Huge Second International Conference on}
\end{center}
\begin{center}
{\Huge Typed Lambda Calculi and Applications}
\end{center}
\begin{center}
{\Huge TLCA}
\end{center}
\smallskip
\begin{center}
{\Large April 10--12, 1995, Edinburgh, Scotland}
\end{center}
\bigskip
The second international conference on Typed Lambda
Calculi and Applications will be held
April 10--12, 1995, at Edinburgh in
Scotland. The conference aims at providing a forum
for the presentation and discussion of recent
research in the following areas:\vspace{-1cm}
\begin{itemize}\begin{center}
\item[] \bf Proof theory of type systems \\
\item[] \bf Logic and type systems \\
\item[] \bf Typed lambda calculi as models of
(higher order) computation \\
\item[] \bf Semantics of type systems \\
\item[] \bf Proof verification via type systems \\
\item[] \bf Type systems of programming languages \\
\item[] \bf Typed term rewriting systems
\end{center}
\end{itemize}
\bigskip
\begin{minipage}[t]{8.5cm}
{\large \bf Program}
\smallskip
The program of TLCA will consist of about 30
selected presentations in plenary sessions.
The program committee for TLCA is
chaired by M.~Dezani and has the following
members: \smallskip
{\bf H.~Barendregt}~(Catholic University of Nijmegen) \\
{\bf M.~Dezani}~(Chairperson, University of Turin) \\
{\bf J-Y.~Girard}~(University of Marseilles) \\
{\bf R.~Hindley}~(University of Swansea) \\
{\bf F.~Honsell}~(University of Udine) \\
{\bf J.~W.~Klop}~(CWI) \\
{\bf G.~Longo}~(ENS) \\
{\bf A.~Meyer}~(MIT) \\
{\bf G.~Plotkin}~(University of Edinburgh) \\
{\bf P.~Scott}~(University of Ottawa) \\
{\bf J.~Smith}~(University of Gothenburg/Chalmers) \\
{\bf J.~Tiuryn}~(University of Warsaw) \\ \smallskip
{\large \bf Call for Papers}
\smallskip
Original contributions are solicited for TLCA;
they should be sent to the conference secretariat.
Electronic submission (PostScript only) is
preferred; hard copy (6 copies required) will
also be accepted. Papers should be clearly written
and allow the program committee to assess the
merits of the work. References and comparisons
with related work should be included.
Papers should not exceed 15 standard pages and
should be accompanied by a one-page abstract.
The deadline for submissions is September 8, 1994.
Authors will receive notification of acceptance by
November 12, 1994. Definitive versions of papers
will be due December 15, 1994.
\end{minipage} \hspace{1cm} \begin{minipage}[t]{8.5cm}
{\large \bf Proceedings}
\smallskip
It is intended to publish the accepted papers as a
volume of the Springer Verlag Lecture Notes in Computer
Science series.\smallskip\\
{\large \bf Organizing Committee}
\smallskip
{\bf G.~Cleland, P.~Gardner, M.~Lekuse,
G.~Plotkin} \\(University of Edinburgh) \\
{\large \bf Important Dates}
\smallskip
\vspace{-0.25cm}\begin{tabbing}
abcdefghijklmnop\=abcdefghijklmnop\kill
Sept. 8, 1994
\>Deadline for submissions \\
Nov. 12, 1994
\>Notification of acceptance \\
Dec. 15, 1994
\>Final version of paper \\
April 10, 1995
\>TLCA
\end{tabbing}
\vspace{0.1cm}\smallskip
{\large \bf TLCA Secretariat}
\smallskip
TLCA Secretariat \\
Professor M.~Dezani \\
Universit\'{a} di Torino \\
Dipartimento di Informatica \\
Corso Svizzera, 185\\
10149 Torino \\
ITALY\\
Tel: 39-11-7429232~~Fax: 39-11-751603\\
Email: dezani@di.unito.it \\
{\large \bf $\lambda$-Calculus Network Meeting}
\smallskip
Participants of TLCA are invited to attend a
$\lambda$-Calculus Network Meeting to be held
in the weekend before the conference.
\end{minipage}
\end{document}