Date: Wed, 2 Nov 1994 05:36:00 +0400 (GMT+4:00)
Subject: subobjects of free objects
Date: Mon, 31 Oct 1994 18:20:21 +0000
From: "Prof R. Brown"
What results of the form `A sub-X of a free X is free' are known?
I am aware of groups, magmas (= set with binary operation), and
modules over a principal ideal domain. I'd be interested to hear of
structures for which this is either known to be true, or examples
where it fails.
John Stell
There are a lot of counterexamples examples in the topological case. There
is also a lot of work on the profinite case (open subgroups of free
profinite groups are free profinite). Brown and Hardy proved open
subgroups of free topological groups are free topological (various
k_{\omega} conditions used) (JLMS (2)10 (1975) 431-440).Sid Morris has a
good survey in Categorical Topology (Proceedings Toledo 1983, ed HLBentley
et al). I have a paper in Proc AMS 52 (1975) 433-441 giving examples of
non projective closed subgroups of the free topological group on [a,b]
(e.g. the subgroup generated by {a} and x^2 for x \in [a,b], has \pi_0 =
Z_2, which is not free).
Ronnie Brown
Prof R. Brown Tel: +44 248 382474
School of Mathematics Fax: +44 248 355881
Dean St email: mas010@uk.ac.bangor
University of Wales
Bangor
Gwynedd LL57 1UT
UK
Date: Wed, 2 Nov 1994 05:39:20 +0400 (GMT+4:00)
Subject: Re: sub-structures of free structures
Date: Tue, 1 Nov 94 10:09:06 -0600
From: James Madden
The discussion and responses on sub-structures of free structures
got me thinking about a problem that bothered to me some time a go.
Suppose an equational class V has the following property:
(1) if A and B are FINITELY GENERATED V-agebras whose coproduct is
free, then A and B are both free.
Does this imply that V has the prorerty that
(2) if A and B are ANY V-agebras whose coproduct is free, then A and
B are both free?
I proved in 1983 that the variety of vector-lattices (= abelian
lattice-ordered groups with order-preserving action by positive real
numbers) has (1), using PL topology. (In the variety of
vector-lattices, projective does not imply free, so this result has
some content.) In fact, if V = vector-lattices, the following is
true:
(1a) if A and B are ANY V-agebras whose coproduct is FINITELY
GENERATED and free, then A and B are both free.
BUT, I was never able to show that the variety of vector-lattices has
(2).
Does (2) follow from (1) or from (1a) by any general theorems of
universal algebra, model-theory, etc.?
James Madden
Date: Wed, 9 Nov 1994 15:56:19 +0400 (GMT+4:00)
Subject: Fibrations<-->Adjunctions????
Date: Wed, 9 Nov 1994 19:10:37 +0100
From: Maura Cerioli
Hi,
I need to use the following result about the equivalence between the
existence of a fibration and the existence of a right adjoint to
an opportune functor between comma categories:
-----------------
Let A and B be categories and let U:A-->B be a
functor.
Let C denote the comma category A arrow (whose objects are the arrows
of A)
and
let D denote the comma category B over U (whose objects are arrows in B
from a generic object b into U(a), together with a).
Then U induces a functor V:C-->D, that basically is U (as both objects
and arrows in C are arrows in A too)
and is defined as follows:
* V(f:a-->a')=(U(f):U(a)-->U(a'),a') for each object
f:a-->a' in A;
* V(g,g')=(U(g),g') for each arrow
(g,g'):(f1:a1-->a'1)----->(f2:a2-->a'2) in A.
Then U is a fibration iff V has a right adjoint G:D-->C s.t.
G;V is the identity on D and the counit of the adjunction is
the identity natural transformation.
-----------------
Now, I know (or at least I believe) that the result holds, as
I have a proof for it; but a collegue said to me that this is
a known result and suggested to look at the works by Street
in the Sydney Category Seminar.
Unfortunately, being quite ignorant about 2categories, I find very
hard even to understand in which sense the result I want is there.
Does anybody know an easier reference, possibly not involving
2categories?
Thanks
Maura
Maura Cerioli
DISI - Dipartimento di Informatica e Scienze dell'Informazione
Viale Benedetto XV, 3
16132 Genova
ITALY
Date: Wed, 9 Nov 1994 15:51:53 +0400 (GMT+4:00)
Subject: New papers available by gopher & ftp
Date: 8 Nov 1994 20:51:40 GMT
From: Charles Wells
Three papers are newly available by gopher and by anonymous ftp
from Case Western Reserve University:
"The categorical theory generated by a limit sketch", by Michael
Barr and Charles Wells. This was formerly called "The category
of diagrams".
"Varieties of mathematical prose" by Atish Bagchi and Charles
Wells. This is not about category theory but was referred to in
our paper "The logic of sketches" (also available by gopher &
ftp).
"Extension theories for categories", by Charles Wells. This is
an old paper that was never submitted for publication. I have updated
the bibliography as far as I can, but would appreciate it if
anyone knows of other suitable references.
They are available by gopher in both DVI and Postscript form
from the host gopher.cwru.edu, path 1/class/mans/math/pub/wells.
Most www clients can get gopher files, and some of the can view
Postscript files on screen.
The files are also available by anonymous ftp from ftp.cwru.edu in
the directory math/wells, under the following filenames:
"Varieties of mathematical prose": MATHRITE.DVI, MATHRITE.PS
"Extension theories for categories": CATEXT.DVI, CATEXT.PS
"The categorical theory generated by a limit sketch": DIAGC.DVI,
DIAGC.PS
"The logic of sketches": LOGSTR.DVI, LOGSTR.PS
I would appreciate knowing if anyone has problems downloading
these files.
--
Charles Wells
Department of Mathematics, Case Western Reserve University
10900 Euclid Avenue, Cleveland, OH 44106-7058, USA
216 368 2893
Date: Thu, 10 Nov 1994 12:58:42 +0400 (GMT+4:00)
Subject: Re: Fibrations<-->Adjunctions????
Date: Wed, 9 Nov 1994 21:22:16 +0000 (GMT)
From: Dusko Pavlovic
The result goes back to Claude Chevalley's seminar. (One direction
does require the Axiom of Choice.) I think a simple formulation is in
J.Gray's paper on fibrations in the proceedings of La Yolla
conference, Springer 1965.
-- Dusko Pavlovic
Date: Thu, 10 Nov 1994 13:00:41 +0400 (GMT+4:00)
Subject: cat logic of interactions
Date: Wed, 9 Nov 1994 22:10:43 +0000 (GMT)
From: Dusko Pavlovic
I just remembered that I never announced this paper in which I was
trying to learn some concurrency theory. It depends on a note on
representation, that used to be its appendix. It will be available
soon.
The ps-file with A4-format is in papers/Pavlovic on
theory.doc.ic.ac.uk; the American format is in pub/pavlovic on
triples.math.mcgill.ca.
All the best,
-- Dusko
CATEGORICAL LOGIC OF CONCURRENCY AND INTERACTION I:
SYNCHRONOUS PROCESSES
by Dusko Pavlovic (August 1994)
Abstract.
This is a report on a mathematician's effort to understand some
concurrency theory. The starting point is a logical interpretation of
Nielsen and Winskel's account of the basic models of concurrency. Upon
the obtained logical structures, we build a calculus of relations
which yields, when cut down by bisimulations, Abramsky's interaction
category of synchronous processes. It seems that all interaction
categories arise in this way. The obtained presentation uncovers some
of their logical contents and perhaps sheds some more light on the
original idea of processes as relations extended in time.
The sequel of this paper will address the issues of asynchronicity,
preemption, noninterleaving and linear logic in the same setting.
Date: Thu, 10 Nov 1994 18:45:43 +0400 (GMT+4:00)
Subject: Announce paper: Cockett & Seely
Date: Wed, 9 Nov 94 22:38:25 EST
From: "Robert A. G. Seely"
The following paper has been placed on anonymous ftp at
triples.math.mcgill.ca, directory /pub/rags/wk_dist_cat
Weakly distributive categories
by J.R.B. Cockett and R.A.G. Seely
Abstract:
There are many situations in logic, theoretical computer science, and
category theory where two binary operations---one thought of as a (tensor)
``product'', the other a ``sum''---play a key role. In distributive and
*-autonomous categories these operations can be regarded as, respectively,
the and/or of traditional logic and the times/par of (multiplicative) linear
logic. In the latter logic, however, the distributivity of product over sum
is conspicuously absent: this paper studies a ``linearization'' of that
distributivity which is present in both case. Furthermore, we show that
this weak distributivity is precisely what is needed to model Gentzen's cut
rule (in the absence of other structural rules) and can be strengthened in
two natural ways to generate full distributivity and *-autonomous categories.
This is the journal version of the similarly named paper appearing in the
Proceedings of the Durham conference (1991):
M.P. Fourman, P.T. Johnstone, A.M. Pitts, eds., Applications of Categories
to Computer Science, London Mathematical Society Lecture Note Series 177
(1992) 45 - 65.
This version is to appear in the Journal of Pure and Applied Algebra.
The paper has been rewritten, including more details and several examples,
including shifted tensors, Span categories, and categories of modules of a
bialgebra.
Date: Thu, 10 Nov 1994 18:50:26 +0400 (GMT+4:00)
Subject: Announce paper: Mendler, Panangaden, Scott, & Seely
Date: Wed, 9 Nov 94 22:40:42 EST
From: "Robert A. G. Seely"
The following paper has been placed on anonymous ftp at
triples.math.mcgill.ca in directory (file) /pub/rags/ccp/mpss.*
A Logical View of Concurrent Constraint Programming
by
Nax Paul Mendler
Prakash Panangaden
P.J. Scott
R.A.G. Seely
Abstract;
The Concurrent Constraint Programming paradigm has been the subject of
growing interest as the focus of a new paradigm for concurrent computation.
Like logic programming it claims close relations to logic. In fact these
languages _are_ logics in a certain sense that we make precise in this
paper. In recent work it was shown that the denotational semantics of
determinate concurrent constraint programming languages forms a categorical
structure called a hyperdoctrine, which is used as the basis of the
categorical formulation of first order logic. What this connection shows
is the combinators of determinate concurrent constraint programming can be
viewed as logical connectives. In the present work we extend these ideas
to the operational semantics of these languages and thus make available
similar analogies for a much broader variety of languages including the
indeterminate concurrent constraint programming languages and concurrent
block-structured imperative languages.
\begin{BTW}
In the same directory you will find the earlier paper dealing with the
denotational semantics (psss*). This paper has appeared:
P. Panangaden, V. Saraswat, P. J. Scott, R. A. G. Seely,
A Hyperdoctrinal View of Concurrent Constraint Programming, in J.W. de Bakkee
et al, eds. Semantics: Foundations and Applications; Proceedings of
REX Workshop, Beekbergen, The Netherlands, June 1992. Springer Lecture
Notes in Comp. Science, 666 (1993) pp. 457 -- 476.
\end{BTW}
Date: Thu, 10 Nov 1994 18:54:05 +0400 (GMT+4:00)
Subject: Re: Fibrations<-->Adjunctions????
Date: Thu, 10 Nov 1994 09:00:42 -0500
From: Jim Otto
(the message being replied to is appended.)
dear Maura Cerioli
yes, the Street paper is hard to read. but he refers to a paper of
Gray's which has the result you mention. in fact Gray credits it to a
manuscript of Chevalley's which was lost in the mail.
while i didn't read your description of the result, the way i think of
it is as follows. you have a functor
p: E --> B
this induces a functor (with comma category B/p relative to id: B -->
B <-- E :p and with 2 the ordinal)
p.: E^2 --> B/p
which takes
`paths in E' to
`paths in B with the to end in E remembered'
then (modulo the axiom of choice) p is a fibration iff p. has a right
adjoint c. with identity couint. c. is then a cleavage. this unfolds
(viewing c. as terminal objects in comma categories) to the usual
elementary definition in terms of cartesian maps. Gray says p. is
rari, i.e. has a right adjoint right inverse. one can show that this
isn't weaker. as i recall, Street's definition is weaker in order to
be more invariant. (cod: B^2 --> B is an important example. then
c. is pull-back.)
actually i need fibrations in 2-categories of monoidal categories.
note that, in cat the 2-category of categories, E^2 is the comma
category E/E (relative to id: E --> E <-- E :id). further, still in
cat, E^2 is the cotensor 2 -o E. but in any 2-category, finite
weighted limits, including comma objects, can be built up from
cotensors with 2 and (2-) terminal objects and pull-backs.
to help you read Street, i now define cotensor with 2. 2-categories
have hom categories rather than hom sets. 2 -o E is defined by
isomorphisms
hom(W, 2 -o E) iso 2 -o hom(W, E)
(2-) natural in W. (sometimes such isomorphisms don't exist, but such
equivalences do.)
bon jour, Jim Otto
>Date: Wed, 9 Nov 1994 19:10:37 +0100
>From: Maura Cerioli
>
>Hi,
>I need to use the following result about the equivalence between the
>existence of a fibration and the existence of a right adjoint to
>an opportune functor between comma categories:
>-----------------
>Let A and B be categories and let U:A-->B be a
>functor.
>Let C denote the comma category A arrow (whose objects are the arrows
>of A)
>and
>let D denote the comma category B over U (whose objects are arrows in B
>from a generic object b into U(a), together with a).
>Then U induces a functor V:C-->D, that basically is U (as both objects
>and arrows in C are arrows in A too)
>and is defined as follows:
>* V(f:a-->a')=(U(f):U(a)-->U(a'),a') for each object
> f:a-->a' in A;
>* V(g,g')=(U(g),g') for each arrow
> (g,g'):(f1:a1-->a'1)----->(f2:a2-->a'2) in A.
>
>Then U is a fibration iff V has a right adjoint G:D-->C s.t.
>G;V is the identity on D and the counit of the adjunction is
>the identity natural transformation.
>-----------------
>Now, I know (or at least I believe) that the result holds, as
>I have a proof for it; but a collegue said to me that this is
>a known result and suggested to look at the works by Street
>in the Sydney Category Seminar.
>Unfortunately, being quite ignorant about 2categories, I find very
>hard even to understand in which sense the result I want is there.
>
>Does anybody know an easier reference, possibly not involving
>2categories?
Date: Fri, 11 Nov 1994 11:05:19 +0400 (GMT+4:00)
Subject: CTCS-6
Date: Fri, 11 Nov 1994 18:06:39 +1100
From: D.Pitt@mcs.surrey.ac.uk
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
Registration forms for the joint conference will be available nearer to the
date.
Dr. Peter Johnstone,
Department of Pure Mathematics and Mathematical Statistics,
16 Mill Lane,
Cambridge, CB2 1SB,
United Kingdom.
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: Sat, 12 Nov 1994 10:48:09 +0400 (GMT+4:00)
Subject: Colimits in categories of diagrams
Date: Fri, 11 Nov 1994 13:57:32 -0800
From: Y V Srinivas
Do (finite) colimits exist in categories of diagrams?
Here are the definitions of the terms used above.
A diagram of shape S in a category C is a functor D: S -> C.
A covariant diagram morphism from D1: S1 -> C to D2: S2 -> C is a pair
consisting a shape morphism (functor) sm: S1 -> S2 and a
natural transformation mu: D1 -> D2 o sm.
A contravariant diagram morphism is similar except that the direction
of the natural transformation is opposite.
We thus get two categories of diagrams in C (of all shapes).
Mac Lane calls these "super comma categories" (p.111).
Now, the question reads: given that (finite) colimits exist in C, do
(finite) colimits exist in the two categories of diagrams in C?
I haven't been able to come up with a construction or a proof that
colimits don't exist. I appreciate any help you can provide on this
matter. Also, I would like to know if there are related results, e.g.,
with limits.
- srinivas
========
Y. V. Srinivas E-mail: srinivas@kestrel.edu
Kestrel Institute Phone: (415) 493-6871
3260 Hillview Avenue Fax: (415) 424-1807
Palo Alto, CA 94304
Date: Sun, 13 Nov 1994 11:05:24 +0400 (GMT+4:00)
Subject: Re: Colimits in categories of diagrams
Date: Sat, 12 Nov 1994 21:13:19 -0400
From: Richard Wood
> Date: Fri, 11 Nov 1994 13:57:32 -0800
> From: Y V Srinivas
>
>
> Do (finite) colimits exist in categories of diagrams?
>
> Here are the definitions of the terms used above.
>
> A diagram of shape S in a category C is a functor D: S -> C.
>
> A covariant diagram morphism from D1: S1 -> C to D2: S2 -> C is a pair
> consisting a shape morphism (functor) sm: S1 -> S2 and a
> natural transformation mu: D1 -> D2 o sm.
>
> A contravariant diagram morphism is similar except that the direction
> of the natural transformation is opposite.
>
> We thus get two categories of diagrams in C (of all shapes).
> Mac Lane calls these "super comma categories" (p.111).
>
> Now, the question reads: given that (finite) colimits exist in C, do
> (finite) colimits exist in the two categories of diagrams in C?
>
> I haven't been able to come up with a construction or a proof that
> colimits don't exist. I appreciate any help you can provide on this
> matter. Also, I would like to know if there are related results, e.g.,
> with limits.
>
> - srinivas
In my thesis, Dalhousie 1976, I used a (2-)category of diagrams of
the kind that you describe, with C=set. The 2-functor cat--->CAT
which sends S to set^(S^op) gives rise to a fibration, say P:D_--->cat,
and the objects of D_ are evidently diagrams in set of variable shape.
If you regard such an object, D:S^op--->set, as a discrete fibration,
say D'--->S, then it is straightforward to describe a 2-fully faithful
2-functor, I:D_--->cat^2 . Now codomain:cat^2--->cat is itself a
fibration over cat and the inclusion I is a 2-functor over cat.
I has a left adjoint, L, that preserves finite products, from which it
follows that D_ is complete, cocomplete and cartesian closed, as a
2-category. By examining the nature of these constructions for my
D_ you should be able to find what you need of a general C to answer
your question.
Well, to continue somewhat, P above clearly preserves limits but it
also preserves colimits because the adjunction L-|I is an adjunction
over cat. This should help to get started on the general problem. In
fact, P preserves exponentiation too.
(Pseudo-)category objects in D_ are interesting. Necessarily, they
give rise to pseudo-category objects in cat. If, for example, V is a
monoidal category then P-over the "category object" VxV--->V<---1 in
cat are precisely the set^(V^op)-categories, where the monoidal
structure of set^(V^op) is Brian Day's (universal) convolution
structure. But there are many other "category objects" in cat that
can be constructed from V and its monoidal data. Assembling these
and looking at their inverse image in D_ allows one to construct a
variant of the Pare-Schumacher theory of indexed categories that
is useful when a given monoidal structure on the base for indexing
is needed for multiply indexed families.
RJ Wood
Date: Mon, 14 Nov 1994 17:15:37 +0400 (GMT+4:00)
Subject: papers on internal categories ???
Date: Mon, 14 Nov 1994 17:55:48 +0100 (MET)
From: Wojciech Zaborowski
Hi everyone in 'categories' !
I found only a few pages related in Johnstone's Topos theory'.
I am interested in serious introduction to 'internal categories'.
I am especially looking for:
1: full systematic internalization of all fundamental concepts of category
theory, including natural transformations, limits and adjoints
2: books, papers etc. developing classic theories on such abstract (internal)
level
Does anyone enjoy playing with 'internal' too ?
From rrosebru@nimble.mta.ca Tue Nov 15 10:28:54 1994
Date: Mon, 14 Nov 1994 18:39:26 -0400 (AST)
Subject: Re: papers on internal categories ???
Date: Tue, 15 Nov 1994 08:54:47 +1100
From: Ross Street
>I am interested in serious introduction to 'internal categories'.
Ross Street, Cosmoi of internal categories, Transactions American
Math. Soc. 258 (1980) 271-318; MR82a:18007
could be of interest.
--Ross
id AA17208; Tue, 15 Nov 1994 10:20:09 -0400
Date: Tue, 15 Nov 1994 10:17:39 -0400 (AST)
Subject: Re: papers on internal categories ???
Date: 15 Nov 1994 14:00:52 GMT
From: cxm7@po.cwru.edu
> Date: Mon, 14 Nov 1994 17:55:48 +0100 (MET)
> From: Wojciech Zaborowski
>
> Hi everyone in 'categories' !
>
> I found only a few pages related in Johnstone's Topos theory'.
> I am interested in serious introduction to 'internal categories'.
> I am especially looking for:
> 1: full systematic internalization of all fundamental concepts of category
> theory, including natural transformations, limits and adjoints
> 2: books, papers etc. developing classic theories on such abstract (internal)
> level
> Does anyone enjoy playing with 'internal' too ?
>
There is a lot in Johnstone's few pages. I also cover this, making
it look as much like naive category theory as I could, in chapter 20
of my book _Elementary categories, elementary toposes_ (Oxford 1992).
This book is due out in paperback soon.
And you should look at Benabou "Fibred categories and the
foundations of naive category theory" (Jour. Symbolic Logic 50,
1985, 10-37) and Johnstone and Pare _Indexed categories_, Springer
Lecture Notes in Math 661.
Colin McLarty
id AA27810; Tue, 15 Nov 1994 19:26:10 -0400
Date: Tue, 15 Nov 1994 19:23:31 -0400 (AST)
Subject: history question: Grothendieck universes
Date: Tue, 15 Nov 94 10:05:59 CST
From: Juergen Koslowski
Could someone please tell me where the term "Grothendieck universes"
comes from? Some books connect Grothendieck's name with this particular
approach to avoid set-theoretical difficulties, others don't.
What is the current status on these foundational matters anyway? Has anything
else emerged besides MacLanes one universe approach, or Feferman's use of
reflection principles?
best regards, J"urgen
--
J"urgen Koslowski | If I don't see you no more in this world
| I meet you in the next world
koslowj@math.ksu.edu | and don't be late!
nhabkosl@rrzn-user.uni-hannover.de | Jimi Hendrix (Voodoo Child)
id AA00424; Tue, 15 Nov 1994 21:42:14 -0400
Date: Tue, 15 Nov 1994 19:27:57 -0400 (AST)
Subject: Announcement
Date: Tue, 15 Nov 94 15:27:16 EST
From: Michael Makkai
This is to announce two papers,
"Avoiding the axiom of choice in general category theory"
and
"Generalized sketches as a framework for completeness theorems"
both by M. Makkai, McGill University.
Both papers are revised versions of ones with identical titles; the
original versions were produced about a year ago. Both papers will
appear in the Journal of Pure and Applied Algebra. Unfortunately, they
are not available electronically. If you are interested in obtaining
copies, please send your request to Makkai@triples.math.mcgill.ca .
The abstracts of the papers follow.
ABSTRACT of "Avoiding the axiom of choice in general category theory",
by M. Makkai, McGill University:
"The notion of anafunctor is introduced. An anafunctor is, roughly, a
"functor defined up to isomorphism". Anafunctors have a general
theory paralleling that of ordinary functors; they have natural
transformations, they form categories, they can be composed, etc.
Anafunctors can be saturated, to ensure that any object isomorphic to
a possible value of the anafunctor is also a possible value at the
same argument object. The existence of anafunctors in situations when
ordinarily one would use choice is ensured without choice; e.g., for a
category which has binary products, but not specified binary products,
the anaversion of the product functor is canonically definable, unlike
the ordinary product functor that needs the axiom of choice. When the
composition functors in a bicategory are changed into anafunctors, one
obtains anabicategories. In the standard definitions of bicategories
such as the monoidal category of modules over a ring, or the
bicategory of spans in a category with pullbacks, and many others, one
uses choice; the anaversions of these bicategories have canonical
definitions. The overall effect is an elimination of the axiom of
choice, and of non-canonical choices, in large parts of general
category theory. To ensure the Cartesian closed character of the
bicategory of small categories, with anafunctors as 1-cells, one uses
a weak version of the axiom of choice, which is related to A. Blass'
axiom of Small Violations of Choice ("Injectivity, projectivity, and
the axiom of choice", Trans. Amer. Math. Soc. 255(1979), 31-59)."
ABSTRACT of "Generalized sketches as a framework for completeness
theorems", by M. Makkai, McGill University:
"A generalized concept of sketch is introduced. Because of their role,
morphisms of (generalized) sketches are called sketch-entailments. A
sketch is said to satisfy a sketch-entailment if the former is
injective relative to the latter in the standard sense; the models of
a set R of sketch-entailments are the sketches satisfying all members
of R . R logically implies a sketch-entailment s if every model of R
is also a model of {s} . A deductive calculus is introduced in which
s is deducible from R iff R logically implies s (General Completeness
Theorem, GCT). A large number of examples of kinds of structured
category is presented showing that the structured categories are
selected from among the corresponding generalized sketches as the
models of a set of sketch-entailments. As a consequence, the
sketch-entailments satisfied by all structured categories of a given
kind are exactly the ones that are deducible from a certain, usually
finite, set of axioms. In the finitary case, which is the only one
considered in detail in the paper, the notion of deduction is
effective, and straightforwardly implementable on a computer. One
obtains Specific Completeness Theorems (SCT's), each of which asserts
that the exactness properties (certain kinds of sketch-entailments)
that hold in a specific class of structured categories coincide with
the ones that are deducible from a given set of axioms. Each of these
specific completeness theorems is deduced from the GCT, and a
particular Representation Theorem (RT); RT's are a well-known class of
results in categorical logic. The concepts of Compactness and of
Abstract Completeness are introduced, and shown to correspond to the
same-named concepts in logics in the usual symbolic form, via a
translation between the sketch-based syntax and semantics on the one
hand, and the Tarskian syntax and semantics on the other. The
sketch-based concepts are available for several logics defined
categorically for which there are no available symbolic
presentations."
id AA00518; Tue, 15 Nov 1994 21:44:59 -0400
Date: Tue, 15 Nov 1994 19:29:48 -0400 (AST)
Subject: Announcement
Date: Tue, 15 Nov 94 15:27:16 EST
From: Michael Makkai
This is to announce two papers,
"Avoiding the axiom of choice in general category theory"
and
"Generalized sketches as a framework for completeness theorems"
both by M. Makkai, McGill University.
Both papers are revised versions of ones with identical titles; the
original versions were produced about a year ago. Both papers will
appear in the Journal of Pure and Applied Algebra. Unfortunately, they
are not available electronically. If you are interested in obtaining
copies, please send your request to Makkai@triples.math.mcgill.ca .
The abstracts of the papers follow.
ABSTRACT of "Avoiding the axiom of choice in general category theory",
by M. Makkai, McGill University:
"The notion of anafunctor is introduced. An anafunctor is, roughly, a
"functor defined up to isomorphism". Anafunctors have a general
theory paralleling that of ordinary functors; they have natural
transformations, they form categories, they can be composed, etc.
Anafunctors can be saturated, to ensure that any object isomorphic to
a possible value of the anafunctor is also a possible value at the
same argument object. The existence of anafunctors in situations when
ordinarily one would use choice is ensured without choice; e.g., for a
category which has binary products, but not specified binary products,
the anaversion of the product functor is canonically definable, unlike
the ordinary product functor that needs the axiom of choice. When the
composition functors in a bicategory are changed into anafunctors, one
obtains anabicategories. In the standard definitions of bicategories
such as the monoidal category of modules over a ring, or the
bicategory of spans in a category with pullbacks, and many others, one
uses choice; the anaversions of these bicategories have canonical
definitions. The overall effect is an elimination of the axiom of
choice, and of non-canonical choices, in large parts of general
category theory. To ensure the Cartesian closed character of the
bicategory of small categories, with anafunctors as 1-cells, one uses
a weak version of the axiom of choice, which is related to A. Blass'
axiom of Small Violations of Choice ("Injectivity, projectivity, and
the axiom of choice", Trans. Amer. Math. Soc. 255(1979), 31-59)."
ABSTRACT of "Generalized sketches as a framework for completeness
theorems", by M. Makkai, McGill University:
"A generalized concept of sketch is introduced. Because of their role,
morphisms of (generalized) sketches are called sketch-entailments. A
sketch is said to satisfy a sketch-entailment if the former is
injective relative to the latter in the standard sense; the models of
a set R of sketch-entailments are the sketches satisfying all members
of R . R logically implies a sketch-entailment s if every model of R
is also a model of {s} . A deductive calculus is introduced in which
s is deducible from R iff R logically implies s (General Completeness
Theorem, GCT). A large number of examples of kinds of structured
category is presented showing that the structured categories are
selected from among the corresponding generalized sketches as the
models of a set of sketch-entailments. As a consequence, the
sketch-entailments satisfied by all structured categories of a given
kind are exactly the ones that are deducible from a certain, usually
finite, set of axioms. In the finitary case, which is the only one
considered in detail in the paper, the notion of deduction is
effective, and straightforwardly implementable on a computer. One
obtains Specific Completeness Theorems (SCT's), each of which asserts
that the exactness properties (certain kinds of sketch-entailments)
that hold in a specific class of structured categories coincide with
the ones that are deducible from a given set of axioms. Each of these
specific completeness theorems is deduced from the GCT, and a
particular Representation Theorem (RT); RT's are a well-known class of
results in categorical logic. The concepts of Compactness and of
Abstract Completeness are introduced, and shown to correspond to the
same-named concepts in logics in the usual symbolic form, via a
translation between the sketch-based syntax and semantics on the one
hand, and the Tarskian syntax and semantics on the other. The
sketch-based concepts are available for several logics defined
categorically for which there are no available symbolic
presentations."
id AA19746; Wed, 16 Nov 1994 18:50:04 -0400
Date: Wed, 16 Nov 1994 18:45:02 -0400 (AST)
Subject: Availability of new paper by ftp
Date: Wed, 16 Nov 94 16:56:03 +1100
From: Max Kelly
A new preprint "On localization and stabilization for factorization
systems", by Carboni, Janelidze, Kelly, and Pare', is available in our ftp
site at the address maths.su.oz.au (= 129.78.68.2), in the directory
sydcat/papers/kelly, under the titles cjkp.dvi or cjkp.ps; there is also
cjkp.tex, but that requires two macros - namely diagrams.tex and
kluwer.sty.
The paper contains new ideas, but also self-contained introductions to
several areas with which some may be unfamiliar: namely factorization
systems, descent theory, Galois theory, Eilenberg's monotone-light
factorization for maps between compact hausdorff spaces, hereditary
torsion theories for abelian categories, the category of finite families
of objects of a given category, and the (separable, purely-inseparable)
factorization for field extensions.
What ways are there of constructing a factorization system (E, M) on a
category C ? One simple one is to start with a full reflective subcategory
X of C, and to take E to consist of the maps inverted by the reflexion. Of
course, this (E, M) doesn't have E pullback-stable except in the special
case where X is a LOCALIZATION of C.
We examine another general process, which leads to an (E, M) with E stable
when it succeeds. We start from ANY factorization system (E, M), and
define new classes thus: a map lies in E' if EACH of its pullbacks lies in
E; and it lies in M* if SOME pullback of it along an effective descent map
lies in M. Note the connexion with Galois theory, in Janelidze's
categorical formulation of it: if the (E, M) we begin with arises as above
from a reflective full subcategory, the class M* consists of what
Janelidze calls the COVERINGS (or, in some contexts, the CENTRAL
EXTENSIONS).
It is not always the case that (E', M*) is a factorization system; we give
necessary and sufficient conditions for it to be so, and apply these to
three major examples: Eilenberg's factorization above, certain
factorizations connected to hereditary torsion theories, and a new
factorization system for finite-dimensional algebras over a field that
generalizes (separable, purely-inseparable) factorization for field
extensions.
Regards to all - Max Kelly.
ps:
For those without electronic access, a limited number of printed copies
will shortly be available; please request them soon, so that we can alert
the printer.
Max Kelly.
id AA29976; Thu, 17 Nov 1994 10:09:15 -0400
Date: Thu, 17 Nov 1994 10:06:54 -0400 (AST)
Subject: Re: history question: Grothendieck universes
Date: Wed, 16 Nov 94 10:44:44 EST
From: Ernie Manes
J"urgen: I don't remember for sure since it's been more than 20 years, but
I'm of the opinion that Grothendieck invented his universes to deal with functor
categories without antinomies. I would start with Grothendieck and Verdier,
Springer Lecture Notes 269-70, 1972 in articles by them mentioning the word
"topos".
egm
id AA00362; Thu, 17 Nov 1994 10:19:06 -0400
Date: Thu, 17 Nov 1994 10:16:59 -0400 (AST)
Subject: The categorical theory generated by a limit sketch
Date: Wed, 16 Nov 1994 15:20:51 -0500
From: Charles F. Wells
About two weeks ago I announced the availability of a paper
The categorical theory generated by a limit sketch
by Michael Barr and Charles Wells
by gopher from gopher.cwru.edu and by ftp from ftp.cwru.edu. I
have discovered that the copy I posted was not the latest
version. The latest version has now been posted. The
differences are correction of a few minor errors plus some
additional references.
--
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
id AA05200; Thu, 17 Nov 1994 14:22:24 -0400
Date: Thu, 17 Nov 1994 10:10:15 -0400 (AST)
Subject: Re: history question: Grothendieck universes
Date: Wed, 16 Nov 1994 11:20:42 -0500
From: Jim Otto
hi Juergen
it's good to see you're around. for some idea of what i'm up to you
might see
ftp://triples.math.mcgill.ca/pub/otto/home.html
here's some thoughts on
1. universes in practice
2. what is needed
3. the hierarchy paradox
1. one has functor
P: set^o --> set
X |-> 2^X
and adjunction
X --> P Y in set
-------------------
X x Y --> 2 in set
-------------------
Y --> P X in set
-------------------
P X --> Y in set^o
with unit
n: id --> P^2
thus one has meta-function
V: ordinals --> sets
by
1. V(0) = {}
2. n(V(i)): V(i) --> V(i+1) = P^2 V(i)
3. colimit at limit ordinals
then, for limit ordinals i > omega, the sets and functions in V(i)
form a topos with NNO. and, for (strongly) inaccessible cardinals i,
the V(i) form Grothendieck universes. e.g. see Makkai-Pare as well as
Jech or Kunen.
2. one needs big enough colimits to construct e.g. (weak) reflectors
to orthogonality and injectivity classes in categories of presheaves.
e.g. see Adamek-Rosicky as well as work by Makkai on sketches.
3. in Rose, subrecursion, one finds that n+1 nested `for' loops are
needed to reason deterministically about n > 1 nested `for' loops.
yet humans reason about themselves, and living creatures reproduce. i
conjecture, from work on interactive proof, that it takes probability
and residual error to resolve the hierarchy paradox.
bon jour, Jim Otto
id AA04898; Thu, 17 Nov 1994 14:08:37 -0400
Date: Thu, 17 Nov 1994 10:13:24 -0400 (AST)
Subject: Re: history question: Grothendieck universes
Date: Wed, 16 Nov 1994 11:41:49 -0500 (EST)
From: MTHISBEL@ubvms.cc.buffalo.edu
<>
I don't have the Grothendieck reference, but it is not attributed to him by
accident. Hopefully someone will supply particulars. I enter this to observe
(1) One other thing that has emerged is Blass' position, that it doesn't
matter (assuming we wish to do mathematics, not theory of languages). That is
clearly and effectively stated by Barr and Wells in the preface or whatever it
is to . Note further that this treatment of the
is in the spirit of Grothendieck. MacLane, sorry,
Mac Lane is in the spirit of Plato: the one real universe is out there and we
should be discovering its properties. It has more impressive adherents than
Plato, e.g. G"odel, but it is not viable. John Isbell
id AA09035; Thu, 17 Nov 1994 17:09:01 -0400
Date: Thu, 17 Nov 1994 17:05:17 -0400 (AST)
Subject: processes and irredundant trees
Date: Thu, 17 Nov 1994 16:28:43 +0000 (GMT)
From: Dusko Pavlovic
The promised companion to the paper I announced last week is now
available. The first version, which I gave to some people, actually
CONTAINED AN ERROR --- so please download this version if you have an
old copy.
The file is CCPS.ps, and can be downloaded either from
triples.math.mcgill.ca, or from theory.doc.ic.ac.uk.
Regards,
-- Dusko
CONVENIENT CATEGORIES OF PROCESSES AND SIMULATIONS
by Dusko Pavlovic
Abstract.
We show that irredundant trees, used by Dana Scott in the early
sixties, can be used as canonical representants of the bisimilarity
classes of automata (or of transition systems). Simulations then boil
down to tree morphisms. Along the same lines, the categories of
processes modulo the observational and the branching congruences, with
the suitable simulations as morphisms again, are shown to be
isomorphic with certain subcategories of the category of irredundant
trees.
id AA10129; Sat, 19 Nov 1994 12:37:18 -0400
Date: Sat, 19 Nov 1994 12:28:27 -0400 (AST)
Subject: whoops ...
Date: Fri, 18 Nov 94 19:39:36 EST
From: Michael Makkai
Today (November 18th), a certain (essentially unknown) number of
messages that have arrived since yesterday afternoon got erased from my
mailfile before I had a chance of reading them. So, if you have made a
request concerning the two papers I recently announced, and if you
have not received on e-mail an acknowledgement from me, then please repeat your
request. Sorry for the inconvenience. Cheers: Michael Makkai
id AA07757; Wed, 23 Nov 1994 22:30:27 -0400
Date: Wed, 23 Nov 1994 22:26:17 -0400 (AST)
Subject: TLCA '95 : Programme
---------- Forwarded message ----------
Date: Tue, 22 Nov 1994 11:28:12 +0000
Subject: TLCA '95 : Programme
\documentstyle{article}
\begin{document}
\newcommand{\Paper}[2] {{\it #1},$\;${#2}}
\title{Programme\\
International Conference on \\
Typed Lambda Calculi and Applications\\
{\normalsize Edinburgh, April 10th - 12th, 1995}}
\author{}\date{}
\maketitle
\begin{tabbing} {\bf MONDAY}\\
Morning Session Chaired by: M.~Dezani\\
{\bf Theory of Reduction and Conversion}\\
9.00 \Paper{Typed $\lambda$-calculi with explicit substitutions may not
terminate}
{P.A.~Mellies}\\
9.30 \Paper{Comparing $\lambda$-calculus translations in sharing graphs}
{A.~Asperti, C.~Laneve}\\
10.00 Coffee\\
10.30
\Paper{Typed operational semantics}{H.~Goguen}\\
11.00 \Paper{An explicit eta rewrite rule} {D. Briaud}\\
11.30 \Paper{$\beta\eta$-equality for coproducts} {N.~Ghani} \\
\\
12.00 Lunch \\
\\
Afternoon Session Chaired by: G.~Plotkin\\
{\bf Semantics I}\\
2.00 \= {\it A fully abstract translation between a $\lambda$-calculus
with reference types and }\\
\> {\it standard ML,} {E.~Ritter, A.M.~Pitts}\\
2.30 \Paper{Final semantics for untyped $\lambda$-calculus} {F.~Honsell,
M.~Lenisa} \\
3.00 Tea \\
{\bf Categorical Semantics}\\
3.30 \Paper{What is a categorical model of intuitionistic linear logic?}
{G.M.~Bierman} \\
4.00 \= {\it Categorical semantics of the call-by-value $\lambda$-calculus,}\\
\> {A.~Pravato, S.~Ronchi della Rocca, L.~Roversi}\\
4.30 \Paper{Categorical completeness results for the simply-typed
$\lambda$-calculus} {A.K.~Simpson} \\
\end{tabbing}
\newpage
\begin{tabbing}
\\
{\bf TUESDAY}\\
Morning Session Chaired by: H.~Barendregt\\
{\bf Type Theory I}\\
9.00 \Paper{Untyped $\lambda$-calculus with relative typing} {M.R.~Holmes}\\
9.30 \Paper{Basic properties of data types with inequational refinements}
{H.~Kondoh} \\
10.00 Coffee\\
10.30 \Paper{Extensions of pure type systems}
{G.~Barthe}\\
11.00 \Paper{A simple calculus of exception handling} {P.~de Groote}\\
{\bf Proof Theory}\\
11.30 \Paper{Strict functionals for termination proofs}
{J.~van de Pol, H.~Schwichtenberg} \\
\\
12.00 Lunch\\
\\
Afternoon Session Chaired by: F.~Honsell\\
{\bf Semantics II}\\
2.00 \Paper{A simplification of Girard's paradox} {A.J.~Hurkens}\\
2.30 \= {\it A realization of the negative interpretation of the Axiom of
Choice},\\
\> {S.~Berardi, M.~Bezem, T.~Coquand}\\
3.00 Tea\\
3.30 \= {\it A model for formal parametric polymorphism: a per
interpretation of}\\
\> {\it system $\cal R$}, {R.~Bellucci, M.~Abadi, P.L.~Curien}\\
4.00 \Paper{Expanding extensional polymorphism} {R.~Di Cosmo, A.~Piperno}\\
{\bf Discussion}\\
4.30 Open Problem Session, H. Barendregt\\
\end{tabbing}
\begin{tabbing}
\\
{\bf WEDNESDAY}\\
Morning Session Chaired by: J.~Smith\\
{\bf Machine Assisted Reasoning I}\\
9.00
\Paper{A verified typechecker}
{R.~Pollack}\\
9.30
\Paper{Higher-order abstract syntax in Coq}
{J.~Despeyroux, A.~Felty, A.~Hirschowitz}\\
10.00 Coffee\\
{\bf Type Theory II}\\
10.30
\Paper{Using subtyping in program optimization}
{S.~Berardi, L.~Boerio}\\
11.00
\Paper{A simple model for quotient types}
{M.~Hofmann}\\
11.30
\Paper{$\lambda$-calculus, combinators and comprehension systems}
{G.~Dowek}\\
\\
12.00 Lunch\\
\\
\end{tabbing}\newpage
\begin{tabbing}
Afternoon Session Chaired by: R.~Hindley\\
{\bf Machine Assisted Reasoning II}\\
2.00
\Paper{Extracting text from proof}
{Y.~Coscoy, G.~Kahn, L.~Thery}\\
2.30
\= {\it Termination proof of term rewriting system with the multiset path
ordering and}\\
\> {\it derivation length. A complete development in the Calculus of
Constructions},\\
\> {F.~Leclerc}\\
3.00 Tea\\
{\bf Decision Problems}\\
3.30
\Paper{Third-order matching in the presence of type constructors}
{J.~Springintveld}\\
4.00
\Paper{On equivalence classes of interpolation equations}
{V.~Padovani}\\
4.30
\Paper{Decidable properties of intersection type systems}
{T.~Kurata, M.~Takahashi}\\
\end{tabbing}
\end{document}
id AA07925; Wed, 23 Nov 1994 22:36:34 -0400
Date: Wed, 23 Nov 1994 22:27:12 -0400 (AST)
Subject: pssl in Aarhus, second announcement
---------- Forwarded message ----------
Date: Tue, 22 Nov 1994 14:28:55 +0100
From: Jaap van Oosten
The 56th Peripatetic Seminar on Sheaves and Logic will be held
in Aarhus, in the weekend of 3-4 December, 1994.
Should people still wish to register and avail themselves of
relatively cheap accomodation (around 25 British Pounds per night),
it is imperative that I receive their registrations before
MONDAY November 28, at noon.
Hoping to see you in Aarhus,
Jaap van Oosten
id AA09826; Thu, 24 Nov 1994 01:28:36 -0400
Date: Wed, 23 Nov 1994 22:30:19 -0400 (AST)
Subject: 11th ADT Workshop and 8th General Compass Meeting (ASCII & Latex)
Date: Wed, 23 Nov 1994 10:29:59 +0100
From: Magne.Haveraaen@ii.uib.no
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%ASCII%%%%%%%%%%%%%%%%%%%%%%%%%
11th ADT Workshop and 8th General Compass Meeting
September 19 1995 -- September 23 1995
Call for Participation
Workshop on Specification of Abstract Data Types and ESPRIT Compass Meeting
---------------------------------------------------------------------------
The two joint events will take place at Holmenkollen in Oslo. The
workshop starts just after lunch-time Tuesday September 19, and lasts till
Saturday evening September 23. Before the workshop a meeting of the IFIP
WG 14.3 (Foundations of Systems Specifications) will be held at the same
place starting just after lunch-time Monday September 18. The workshop
will provide an opportunity to meet colleagues, to present recent and
ongoing work and to discuss new ideas and future trends.
The workshop is organized by Olaf Owe and Ole-Johan Dahl from the
University of Oslo, and Magne Haveraaen from the University of Bergen.
The topics of the workshop include, but are not limited to:
- algebraic specifications;
- other approaches to formal specification;
- specification languages and methods;
- term rewriting and proof systems;
- specification development systems (concepts, tools, etc.).
It is planned to have a small number of invited talks.
The proceedings, consisting of a selection of the presented talks through
the usual referee process, will be published after the workshop, probably
in the Lecture Notes series of the Springer-Verlag (see e.g. the
Recent Trends in Data Type Specifications series, n. 332, 534, 655, 785,
...).
Please note:
as there is a limited number of slots for talks, REGISTER NOW!
We will accept speakers essentially in the order of arrival date of their
registrations (a corrective mechanism is organized in order to guarantee
visibility to every site). So if you plan to have a talk please let us
know as soon as possible (communication via e-mail or WWW is suggested).
Location
--------
The workshop will be held at the Soria Moria hotel at Holmenkollen in
Oslo. Even though the site is barely 12 km from downtown and 14 km from
the airport, the area has a hilly flavour, surrounded by quiet woods, an
excellent terrain for walking. The hotel itself is modern with excellent
conference facilities, including swimming pool and sauna.
Accommodation
-------------
According to the tradition, the workshop is planned on a residential base,
so participants are required to stay at the Soria Moria hotel.
Normal arrival is expected Tuesday September 19 after lunch, and departure
on Sunday September 24 after breakfast, with the possibility of extending
the stay in both directions. Participants to the IFIP WG 14.3 meeting are
expected to arrive Monday September 18 after lunch.
We have reserved a number of rooms, both single and double, and expect to
be able to accommodate everybody registering BEFORE JUNE 15. We will try
to accommodate people registering by July 31, depending on room
availability.
Deadline for registration is the 15th of June '95
Please note:
the single rooms will be assigned essentially following a FIFO principle;
thus if you want a single room, book it now.
Prices
We have an agreement with the hotel for a special price for full board
during the workshop. For a single room this amounts to 880 NOK per day,
and to 620 NOK per day per person in a double room.
For the whole workshop the prices in Norwegian Crowns amount to:
! WADT/COMPASS (Tue-Sun) ! WG14.3/WADT/COMPASS (Mon-Sun)
-----------------+-------------------------+------------------------------
single room ! 4400 NOK (ca. 530 ECU) ! 5280 NOK (ca. 640 EQU)
double room, p.p.! 3100 NOK (ca. 375 EQU) ! 3720 NOK (ca. 450 ECU)
-----------------+-------------------------+------------------------------
Note that the prices in ECU are obtained at the current rate (which could
be different next September). There is a small chance that the boarding
prices may be influenced by changes in the Norwegian taxation system. Such
changes, if any, will be decided before Christmas.
Registration fee
----------------
As usual a reasonable fee will be required at the registration desk, to
cover expenses like proceedings publication, social events and so on. The
precise amount has still to be established, depending on the real costs
and the funds that can be raised to cover them.
Travel Information
------------------
The Soria Moria hotel is easily reachable by bus and taxi from downtown
Oslo or directly from the Fornebu Airport in Oslo. The dates for the event
have been chosen so that participants can make use of reduced airfares
(PEX, APEX).
Other information
-----------------
More organizational details will follow, and registered participants will
be kept informed. Updated information will also be available on the
World-Wide Web (WWW) at URL:
http://www.ifi.uio.no/~adt95/
AS THERE IS A LIMITED NUMBER OF PLACES AVAILABLE FOR THE WORKSHOP,
REGISTER EARLY!
We will accept participants in the order of date of arrival of the
enclosed registration form
Please return the registration form (by e-mail or surface mail) to
the following address.
ADT'95 Organization
Institutt for informatikk e-mail: adt95@ifi.uio.no
Postboks 1080 Blindern phone: +47 22 85 24 10
0316 OSLO fax: +47 22 85 24 01
Norway WWW: http://www.ifi.uio.no/~adt95/
------------------------------------------------------------------------
11th ADT Workshop and 8th General Compass Meeting
Registration form
One form for each participant, please!
Family Name ........................................................
Christian Name ........................................................
Institution ........................................................
Mailing address ........................................................
........................................................
........................................................
........................................................
........................................................
E-mail ........................................................
Fax ........................................................
Telephone ........................................................
I will attend to the workshop ... yes ... no
I intend to give a talk ... yes ... no
If yes, provisional title ..............................................
........................................................
........................................................
I prefer ... single room ... double room
I would like to share the room with ................................
Special meal requirements (please specify): ............................
I will arrive ..........................
I will depart ..........................
I am a member of IFIP WG 14.3 ... yes ... no
Name of accompanying non-participants ..................................
for which I need ...... additional single rooms and
...... additional double rooms
Signature .............................................................
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%LATEX%%%%%%%%%%%%%%%%%%%%%%%%%
\documentstyle{article}
\topmargin - 21mm
\oddsidemargin -11mm
\evensidemargin -11mm
\textheight 256mm
\textwidth 180mm
\renewcommand{\arraystretch}{1.5}
\catcode`\<=\active\global\chardef~126
%\newcommand{\printtilde}{\verb+~+}
\pagestyle{empty}
\title{{\LARGE\bf 11th ADT Workshop and 8th General Compass Meeting}}
\author{{\Large\bf September 19 1995 -- September 23 1995}}
\date{{\large\bf Call for Participation}}
\begin{document}
\maketitle
\thispagestyle{empty}
\subsection*{Workshop on specification of Abstract Data Types and ESPRIT
Compass Meeting}
The two joint events will take place at Holmenkollen in Oslo. The
workshop starts just after lunch-time Tuesday September 19, and lasts till
Saturday evening September 23. Before the workshop a meeting of the IFIP
WG 14.3 (Foundations of Systems Specifications) will be held at the same
place starting just after lunch-time Monday September 18.
\\
The workshop will provide an opportunity to meet colleagues, to present
recent and ongoing work and to discuss new ideas and future trends.
The workshop is organized by Olaf Owe and Ole-Johan Dahl from the
University of Oslo, and Magne Haveraaen from the University of Bergen.
The topics of the workshop include, but are not limited to:
\begin{itemize}
\item algebraic specifications;
\item other approaches to formal specification;
\item specification languages and methods;
\item term rewriting and proof systems;
\item specification development systems (concepts, tools, etc.).
\end{itemize}
It is planned to have a small number of invited talks.
The proceedings, consisting of a selection of the presented talks through
the usual referee process, will be published after the workshop, probably
in the Lecture Notes series of the Springer-Verlag (see e.g.\ the
Recent Trends in Data Type Specifications series, n. 332, 534, 655, 785,
\ldots).
\medskip
\noindent{\bf Please note:}
as there is a limited number of slots for talks, {\large\em register now!}
We will accept speakers essentially in the order of arrival date of their
registrations (a corrective mechanism is organized in order to guarantee
visibility to every site). So if you plan to have a talk please let us
know as soon as possible (communication via e-mail or WWW is suggested).
\subsection*{Location}
The workshop will be held at the Soria Moria hotel at Holmenkollen in
Oslo. Even though the site is barely 12 km from downtown and 14 km from
the airport, the area has a hilly flavour, surrounded by quiet woods, an
excellent terrain for walking. The hotel itself is modern with excellent
conference facilities, including swimming pool and sauna.
\subsection*{Accommodation}
According to the tradition, the workshop is planned on a residential base,
so participants are required to stay at the Soria Moria hotel.
Normal arrival is expected Tuesday September 19 after lunch, and departure
on Sunday September 24 after breakfast, with the possibility of extending
the stay in both directions. Participants to the IFIP WG 14.3 meeting are
expected to arrive Monday September 18 after lunch.
We have reserved a number of rooms, both single and double, and expect to
be able to accommodate everybody registering {\bf before June 15}. We
will try to accommodate people registering by July 31, depending on room
availability.
\begin{center}
\large\bf
\fbox{Deadline for registration is the 15th of June '95}
\end{center}
\medskip
\noindent{\bf Please note:}
the single rooms will be assigned essentially following a {\tt FIFO}
principle; thus if you want a single room, {\em book it now}.
\subsubsection*{Prices}
We have an agreement with the hotel for a special price for full board
during the workshop. For a single room this amounts to 880 NOK per day,
and to 620 NOK per day per person in a double room.
\noindent
For the whole workshop the prices in Norwegian Crowns amount to:
\smallskip
\begin{center}
\begin{tabular}{|l|c|c|}\hline
& Just WADT/COMPASS (Tue-Sun)
& IFIP WG 14.3 \& WADT/COMPASS (Mon-Sun)
\\ \hline
single room & 4400 NOK ($\approx$ 530 ECU) & 5280 NOK ($\approx$ 640 EQU) \\ \hline
double room, p.p. & 3100 NOK ($\approx$ 375 EQU) & 3720 NOK ($\approx$ 450 ECU) \\ \hline
\end{tabular}
\end{center}
\smallskip
Note that the prices in ECU are obtained at the current rate (which could
be different next September). There is a small chance that the boarding
prices may be influenced by changes in the Norwegian taxation system. Such
changes, if any, will be decided before Christmas.
\medskip
\subsection*{Registration fee}
As usual a reasonable fee will be required at the registration desk, to
cover expenses like proceedings publication, social events and so on. The
precise amount has still to be established, depending on the real costs
and the funds that can be raised to cover them.
\subsection*{Travel Information}
The Soria Moria hotel is easily reachable by bus and taxi from downtown
Oslo or directly from the Fornebu Airport in Oslo. The dates for the event
have been chosen so that participants can make use of reduced airfares
(PEX, APEX).
\subsection*{Other information}
More organizational details will follow, and registered participants will
be kept informed. Updated information will also be available on the World-Wide
Web (WWW) at URL:
\begin{center}
http://www.ifi.uio.no/~adt95/
\end{center}
\vspace{0.8cm}
\noindent{\Large
As there is a limited number of places available for the workshop,
register early! \ \ \ \ \ \
\noindent
We will accept participants in the order of date of arrival of the enclosed
registration form
\bigskip
\begin{center}
REGISTER NOW!
\end{center}
}
\vspace{0.8cm}
\noindent
Please return the registration form (by e-mail or surface mail) to the
following address.
\begin{center}
\begin{tabular}{lcll}
ADT'95 Organization &\makebox[3cm]{}& \\
Institutt for informatikk &&e-mail: &adt95@ifi.uio.no \\
Postboks 1080 Blindern &&phone: &+47 22 85 24 10 \\
0316 OSLO &&fax: &+47 22 85 24 01 \\
Norway &&WWW: &http://www.ifi.uio.no/~adt95/
\end{tabular}
\end{center}
\begin{center}
\pagebreak
{\Large\bf 11th ADT Workshop and 8th General Compass Meeting}
\smallskip
{\Large\bf Registration form}
{\bf One form for each participant, please!}
\end{center}
\addtolength{\baselineskip}{0.3cm}
\bigskip
\noindent
\makebox[3cm][l]{Family Name} \ \dotfill\ \\
\makebox[3cm][l]{Christian Name} \ \dotfill\ \\
\makebox[3cm][l]{Institution} \ \dotfill\ \\
\makebox[3cm][l]{Mailing address} \ \dotfill\ \\
\makebox[3cm]{} \ \dotfill\ \\
\makebox[3cm]{} \ \dotfill\ \\
\makebox[3cm]{} \ \dotfill\ \\
E-mail \dotfill\qquad
Fax \dotfill\qquad
Telephone \dotfill\\
\bigskip
\noindent
\begin{tabular}{lll}
I will attend to the workshop & $\Box$ yes & $\Box$ no\\
I intend to give a talk & $\Box$ yes & $\Box$ no\\
\end{tabular}
\hspace{1cm}If yes, provisional title \dotfill\\
\makebox[3cm]{}\dotfill\\
\bigskip
\noindent
I prefer\hspace{2cm} $\Box$ single room\hspace{2cm}$\Box$ double
room\\
\hspace{1cm}I would like to share the room with\ \dotfill\\
\bigskip
\noindent
Special meal requirements (please specify): \dotfill\\
\bigskip
\noindent
I will arrive \dotfill\\
I will depart \dotfill\\
I am a member of IFIP WG 14.3 \ \ \ $\Box$ yes \ \ $\Box$ no\\
\bigskip
\noindent
\begin{tabular}{@{}lll}\multicolumn{3}{@{}l@{}}{\hspace*{\textwidth}}\\[0em]
Name of accompanying non-participants &\multicolumn{2}{l@{}}{\dotfill} \\
\multicolumn{1}{r}{for which I need} &\ldots\ldots\ldots& additional single rooms and \\
&\ldots\ldots\ldots& additional double rooms
\end{tabular}
\vfill
\hspace{5cm}Signature \dotfill
\end{document}
id AA10047; Mon, 28 Nov 1994 15:10:03 -0400
Date: Mon, 28 Nov 1994 15:05:18 -0400 (AST)
Subject: 57th PSSL
Date: Mon, 28 Nov 1994 09:39:51 UTC+0200
From: damphous@univ-tours.fr
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%% TEX SOURCE OF THE ANNOUNCEMENT BELOW %%%%
%%%% TEX SOURCE OF THE ANNOUNCEMENT BELOW %%%%
%%%% PLAIN TEX PLAIN TEX PLAIN TEX %%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%&tex
%A4
\font\BF=cmbx12 scaled\magstep3
\font\RM=cmr12
\font\SC=cmcsc10 scaled\magstep1
\font\SL=cmsl12
\font\TT=cmtt12
\baselineskip=16pt
\narrower
%%%%%%%%%%%%
\RM
$$\hbox{\BF 57th PERIPATETIC SEMINAR}$$
$$\hbox{\BF ON SHEAVES AND LOGIC}$$
\vskip1.6cm
\setbox25=\hbox{Dear Colleagues,}\dimen25=\wd25
\noindent\box25\par\medbreak
\noindent\kern\dimen25%
This is the announcement of
%
$$\hbox{\SC THE 57th PERIPATETIC SEMINAR ON SHEAVES AND LOGIC}$$
%
This PSSL is to be held in Tours on the 18-19th of february. As usual,
talks on topics in logic, category theory and related areas in mathematics
and computer science are welcome. Please publicize this meeting amongst your
colleagues. At the time of the meeting, {\SC Jiri Rosicky\/} will be a guest
at the university {\SL Fran\c cois Rabelais\/}.
The meeting will be supported by the university for a fixed amount (not
known yet), so that what the fees are to be is not even known by the
organizer. At this time of the academic year, housing in the halls of
residence is impossible. However, the {\SL Centre R\'egional des Oeuvres
Universitaires\/}, has now a splendid {\SL petit h\^otel particulier\/},
(this is the modest local name for private small ch\^ateaux that rich
families owned along the Loire river) where we will have the 57th PSSL.
It has 33 bedrooms, lecture rooms, a nice and huge garden for mathematical
meditation\dots\ Meals will be served on the site. The cost is 210FF
per night with breakfast, plus 85FF per meal. The place is rated ***;
the cost is however inferior to a plain **-hotel. The fees will be equal to
$$\hbox{(total cost - money from the university)/(the number of participants)}.$$
If there is a need for more than 33 bedrooms, arrangements will be made for
a hotel. So registering as early as possible (if you intend to come) is going
to make the organisation easier.
As usual, participants will arrive on friday night or on saturday morning.
Lectures will start (probably) at 9.30 on staurday and will finish on sunday
morning at noon. It will be possible to have diner there on friday and lunch
on sunday. I will send all registered mathematicians complete details on the
location of {\SL La croix montoire\/}, the name of this ``petit h\^otel
particulier''. It is in Tours on the north shore of the Loire river, and can
be reached by urban busses from the train station.
\vfill\eject
$$\hbox{\SC Please return as soon as possible}$$
$$\hbox{e-mail: {\TT damphous@univ-tours.fr\/}}$$
$$\hbox{$\matrix{\hbox{\SL Pierre Damphousse}\hfill\cr
\hbox{\SL D\'epartement de Math\'ematiques}\hfill\cr
\hbox{\SL Facult\'e des Sciences}\hfill\cr
\hbox{\SL Parc de Grandmont}\hfill\cr
\hbox{\SL Tours 37200, FRANCE}\hfill\cr}$}$$
\vskip1.5cm
\noindent I would like to attend the 57th PSSL:\par\smallbreak
Name:\par\smallbreak
Return Address:\par\smallbreak
\vskip3cm
email:\par
\bigbreak
\noindent I wish to give a talk entitled:\par\smallbreak
of 20/30/45 minutes (specify):\par
\bigbreak
\noindent I wish to book accomodation
from ..................... to ................;\par\smallbreak
I will have diner on friday night (not included in the fees) (Yes/No):\par\smallbreak
I will have lunch on sunday (not included in the fees) (Yes/No):\par\smallbreak
%
\bye