From MAILER-DAEMON Wed Mar 12 19:50:15 2008
Date: 12 Mar 2008 19:50:15 -0300
From: Mail System Internal Data
Subject: DON'T DELETE THIS MESSAGE -- FOLDER INTERNAL DATA
Message-ID: <1205362215@mta.ca>
X-IMAP: 1201902028 0000000057
Status: RO
This text is part of the internal format of your mail folder, and is not
a real message. It is created automatically by the mail system software.
If deleted, important folder data will be lost, and it will be re-created
with the data reset to initial values.
From rrosebru@mta.ca Fri Feb 1 17:17:25 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 01 Feb 2008 17:17:25 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JL35I-0002nU-EG
for categories-list@mta.ca; Fri, 01 Feb 2008 17:06:04 -0400
From: Gaucher Philippe
Subject: categories: cogenerator of k-spaces
Date: Fri, 1 Feb 2008 14:27:23 +0100
MIME-Version: 1.0
Content-Disposition: inline
To: categories@mta.ca
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 1
Dear All,
Does the category of k-spaces (i.e. colimits of compact Hausdorff spaces) have
a cogenerator ? Note that these spaces are not necessarily normal because
they are not necessarily Hausdorff. Otherwise [0,1] would have work without
any additional argument.
Thanks in advance. pg.
From rrosebru@mta.ca Fri Feb 1 17:17:25 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 01 Feb 2008 17:17:25 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JL36P-00030I-Kl
for categories-list@mta.ca; Fri, 01 Feb 2008 17:07:13 -0400
From: "Noson"
To:
Subject: categories: Alex Heller
Date: Fri, 1 Feb 2008 15:28:16 -0500
MIME-Version: 1.0
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 2
It is with great sadness that I inform you of the passing of Alex
Heller.
He passed away yesterday after a short illness.
Details to follow.
From rrosebru@mta.ca Sat Feb 2 09:56:30 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sat, 02 Feb 2008 09:56:30 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JLIlr-00042H-ES
for categories-list@mta.ca; Sat, 02 Feb 2008 09:51:03 -0400
From: Dana Scott
To: categories@mta.ca
Content-Type: text/plain; charset=US-ASCII; format=flowed
Content-Transfer-Encoding: 7bit
Subject: categories: Re: Alex Heller
Date: Fri, 1 Feb 2008 13:39:20 -0800
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 4
On Feb 1, 2008, at 12:28 PM, Noson wrote:
> It is with great sadness that I inform you of the passing of
> Alex Heller. He passed away yesterday after a short illness.
> Details to follow.
Sad, sad, sad news indeed.
I have to relay a story Alex told me not so many years ago when
we sat next to each other at a conference dinner.
I asked him about the last illness of Eilenberg, which was long
and difficult. Alex visited him often, and after a stroke Sammy
could not talk. On the last time he saw him, as Alex was getting
up to leave, he saw Sammy wanted something. Then he realized he
wanted a farewell hug. Anyone who remembers Sammy will recall
he was one of the world's prime skeptics and not much into hugging.
Alex gave him the hug, and just imagining the scene brings tears
to my eyes.
Dana & Irene Scott
1149 Shattuck Avenue
Berkeley, CA 94707-2609
------
Tel: (510) 527-5287
From rrosebru@mta.ca Sat Feb 2 09:56:30 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sat, 02 Feb 2008 09:56:30 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JLInI-00047K-K9
for categories-list@mta.ca; Sat, 02 Feb 2008 09:52:32 -0400
Date: Fri, 1 Feb 2008 19:42:47 -0500 (EST)
From: Michael Barr
To: Categories list
Subject: categories: Alex Heller
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 5
The younger category theorists will have had little knowledge of the great
contributions Alex made in the early days. Not research in category
theory per se, but an early promoter, supporter, and consumer of category
theory in algebraic topology. See his paper in the La Jolla volume. I
believe that he was also one of the organizers of that meeting.
When I arrived in Urbana in the fall of 1964, there was an active seminar
in category theory. Alex, Jon Beck, Max Kelly, John Gray and I were the
main participants along with graduate students. Mac Lane's invitation to
the five of us to spend a weekend in Chicago constituted the first
mid-west category meeting. Then came the La Jolla meeting.
Unfortunately, at the end of that year, Alex went off to CUNY, Jon to
Cornell, Max back to Sydney and John and I were left alone.
Alex was really the third established mathematician (after Eilenberg and
Mac Lane, of course) to embrace category theory in that way. We mourn his
passing.
From rrosebru@mta.ca Sat Feb 2 09:56:30 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sat, 02 Feb 2008 09:56:30 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JLIo7-00049X-6y
for categories-list@mta.ca; Sat, 02 Feb 2008 09:53:23 -0400
Date: Fri, 1 Feb 2008 20:37:23 -0600 (CST)
From: Gabor Lukacs
To: categories@mta.ca
Subject: categories: Re: cogenerator of k-spaces
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 6
Dear Philippe,
You wrote "colimits of compact Hausdorff spaces." In what category? There
is both a Hausdorff and a non-Hausdorff notion for k-spaces. The earlier
is certainly easier to define.
You may wish to look at Chapter 1 of my thesis:
http://at.yorku.ca/p/a/a/o/41.htm
I discuss there both notions, and provide some reference to the
literature, so it might be a good starting point. Spaces where points can
be distinguished by continuous real-valued functions are often referred to
as "functionally Hausdorff."
T. Ishii gives an example of a regular k-space that is not functionally
Hausdorff in his paper "On the Tychonoff functor and $w$-compactness" that
appeared in Topology Appl., 11(2):173--187, 1980. (See Lemma 3.1.) (I can
send you the paper if you are interested.) This, of course, means that
even for Hausdorff k-spaces you cannot use [0,1] as a cogenerator.
Now, as I am writing this, I wonder what you mean by 'cogenerator': An
object such that morphisms into that object can distinguish between
morphisms in the category (i.e., generalized points), or something that
every space in your category admits an __embedding__ to some power of this
object?
The notion of "embedding" already requires some kind of factorization
system, though.
For the earlier, however, {0,1} equipped with the anti-discrete topology
(i.e., only the set itself and the emptyset are open) does what you want.
It is certainly a k-space (albeit non-Hausdorff).
Best wishes,
Gabi
On Fri, 1 Feb 2008, Gaucher Philippe wrote:
> Dear All,
>
> Does the category of k-spaces (i.e. colimits of compact Hausdorff spaces) have
> a cogenerator ? Note that these spaces are not necessarily normal because
> they are not necessarily Hausdorff. Otherwise [0,1] would have work without
> any additional argument.
>
> Thanks in advance. pg.
>
From rrosebru@mta.ca Sat Feb 2 14:09:26 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sat, 02 Feb 2008 14:09:26 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JLMhu-0000zk-GD
for categories-list@mta.ca; Sat, 02 Feb 2008 14:03:14 -0400
Date: Sat, 02 Feb 2008 16:52:09 +0000
From: Eike Ritter
MIME-Version: 1.0
To: categories@mta.ca
Subject: categories: Midlands Graduate School in the Foundations of Computing Science 14-18 April 2008
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 7
Call for Participation
Midlands Graduate School in Computer Science
14-18 April 2008
School of Computer Science, University of Birmingham
The Midlands Graduate School (MGS) in the Foundations of Computing
Science provides an intensive course of lectures on the Mathematical
Foundations of Computing. It has run annually since 1999, and is
hosted by the Universites of Birmingham, Leicester, and Nottingham in
rotation. The lectures are aimed at PhD students, typically in their
first or second year of study. However, the school is open to anyone
who is interested in learning more about the mathematical foundations
of computing, and all such participants are warmly welcomed. We also
very much welcome students from abroad. We gratefully acknowledge
financial support by ESPRC.
The following courses will be offered:
Basic Courses:
Category Theory (Neil Ghani, University of Nottingham)
Operational Semantics (Roy Crole, University of Leicester)
Typed Lambda Calculus (Paul Levy, University of Birmingham)
Advanced Courses:
The Mathematical Structure of Information Flow, in Physics, Geometry,
Logic and Computation. (Samson Abramsky, University of Oxford)
Coq (Thorsten Altenkirch, University of Nottingham)
Denotational Semantics (Martin Escardo, University of Birmingham)
Games for Software Verification (Dan Ghica, University of Birmingham)
Proof Theory (Peter Hancock, University of Nottingham)
Algebraic Methods (Georg Struth, University of Sheffield)
LOCATION
The school will be held in the School of Computer Science,
University of Birmingham. Birmingham is centrally located in the UK,
and is easily reachable by road, rail and air (Birmingham
International Airport).
REGISTRATION
The deadline for registration is 8 March 2008, and the registration
fee is 350 UK pounds, including accomodation. We also have a
number of free places for UK-based PhD students. The deadline for
applying for these free places is 15 February 2008. The number of places
is limited, so early registration is advised.
FURTHER DETAILS
Google search - MGS 2008
Web page - http://events.cs.bham.ac.uk/mgs2008
--
------------------------------------
Dr Eike Ritter Tel.: (+44) 121 41 44772
School of Computer Science Sec.: (+44) 121 41 43711
The University of Birmingham Fax.: (+44) 121 41 44281
Edgbaston Email: E.Ritter@cs.bham.ac.uk
BIRMINGHAM, B15 2TT Web: http://www.cs.bham.ac.uk
England
------------------------------------
From rrosebru@mta.ca Sun Feb 3 10:02:26 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 03 Feb 2008 10:02:26 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JLfHT-0006L8-T4
for categories-list@mta.ca; Sun, 03 Feb 2008 09:53:11 -0400
From: "Noson"
To:
Subject: categories: Alex Heller
Date: Sat, 2 Feb 2008 21:15:39 -0500
MIME-Version: 1.0
Content-Type: text/plain; charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 8
Alex Heller, who was 82, died Jan. 31st, at St. Vincent's Hospital,
where he was taken after collapsing in his home the previous day.=A0=20
His wife, Grace, said it was a torn aorta. They did emergency surgery
on him, though he succumbed about eighteen hours later.
Condolences can be sent to:
Mrs. Grace Heller
29 West 10th Street
New York, NY 10011
He will truly be missed.
Noson=20
From rrosebru@mta.ca Sun Feb 3 10:02:26 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 03 Feb 2008 10:02:26 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JLfGH-0006HY-0n
for categories-list@mta.ca; Sun, 03 Feb 2008 09:51:57 -0400
From: John Duskin
To: categories@mta.ca
Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes
Content-Transfer-Encoding: 7bit
Subject: categories: Alex
Date: Sat, 2 Feb 2008 13:17:47 -0500
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 9
There is a marvelous picture of Saunders and Alex chairing the Coimbra
CT99 conference. Everyone who knows them should see it.
From rrosebru@mta.ca Sun Feb 3 16:28:20 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 03 Feb 2008 16:28:20 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JLlO6-0006O0-Nh
for categories-list@mta.ca; Sun, 03 Feb 2008 16:24:26 -0400
From: John Duskin
To: categories@mta.ca
Subject: categories: Re: Alex
Date: Sun, 03 Feb 2008 13:17:51 -0500
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 10
Curiously, Fred's marvelous pictures do not include the one I have of Saund=
ers and Alex (taken by the conference photographer). I don't know how to pu=
t it on the web.
From rrosebru@mta.ca Sun Feb 3 16:28:20 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 03 Feb 2008 16:28:20 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JLlMl-0006HG-Qj
for categories-list@mta.ca; Sun, 03 Feb 2008 16:23:03 -0400
Date: Sun, 03 Feb 2008 11:16:07 -0500
From: "Fred E.J. Linton"
To:
Subject: categories: Re: Alex
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 11
[Note from moderator: Jack may refer to a nice picture linked from:
http://www.mat.uc.pt/~ct99/ ]
Jack Duskin wrote, recently, without being terribly specific,
> There is a marvelous picture of Saunders and Alex chairing the Coimbra
> CT99 conference. Everyone who knows them should see it.
A few neat, if low-res, pictures of Alex (and Saunders) at Coimbra =
may be found as the jpegs
http://home.att.net/~b.mikolajewska/booknook/titles/Symposium/Sym-03.jpg
http://home.att.net/~b.mikolajewska/booknook/titles/Symposium/Sym-25.jpg
or on the book pages
http://home.att.net/~b.mikolajewska/booknook/titles/Symposium/S-06.htm
http://home.att.net/~b.mikolajewska/booknook/titles/Symposium/S-19.htm
and those before and after. While these may well NOT be the images =
Jack meant, they may do until he provides more specific references.
Of course, I, like all who had the privilege of coming to know Alex
and Grace, mourn the passing of this cosmopolitan gentleman, quiet
scholar, and supportive enthusiast for category theory. Would that I
might know how to support Grace in these terrible hours: my heart goes
out to her, as also to his children, both biological and mathematical.
-- Fred
From rrosebru@mta.ca Mon Feb 4 11:16:55 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 04 Feb 2008 11:16:55 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JM2sb-0003qp-Lg
for categories-list@mta.ca; Mon, 04 Feb 2008 11:05:05 -0400
From: John Duskin
To: categories@mta.ca
Mime-Version: 1.0 (Apple Message framework v915)
Subject: categories: Saunders and Alex'spicture
Date: Mon, 4 Feb 2008 01:00:14 -0500
Content-Type: text/plain;charset=US-ASCII;format=flowed;delsp=yes
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 12
Thanks to the moderator and Fred, the picture of the pair of them that
I was referring to is on the collection of pics from the Coimbra CT99
conference:
...Note from moderator: Jack may refer to a nice picture linked from:
http://www.mat.uc.pt/~ct99/ ]...
Its the one with them smiling, sitting behind the conference poster.
From rrosebru@mta.ca Mon Feb 4 11:16:55 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 04 Feb 2008 11:16:55 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JM2tN-0003xt-IT
for categories-list@mta.ca; Mon, 04 Feb 2008 11:05:53 -0400
Mime-Version: 1.0 (Apple Message framework v753)
Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed
Content-Transfer-Encoding: quoted-printable
From: Dan Ghica
Subject: categories: GaLoP 2008 : Submission Deadline Extended
Date: Mon, 4 Feb 2008 10:31:15 +0000
To: types-announce@lists.seas.upenn.edu, categories@mta.ca
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 13
Dear all,
The submission deadline for the Games for Logic and Programming =20
Languages III workshop (ETAPS 2008, March 29 - April 6, 2008, =20
Budapest, Hungary) has been extended to February 14. The call for =20
submissions is attached below.
GAMES FOR LOGIC AND PROGRAMMING LANGUAGES III
ETAPS 2008, March 29 - April 6, 2008, Budapest, Hungary
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
*The submission deadline has been extended to February 14.*
The submission site is open:
http://www.easychair.org/conferences/?conf=3Dgalop08
Introduction
GaLoP is an annual international workshop on game-semantic models for =20=
logics and programming languages and their applications. This is an =20
informal workshop that welcomes work in progress, overviews of more =20
extensive work, programmatic or position papers and tutorials as well =20=
as contributed papers and invited talks.
Contributions are invited on all pertinent subjects, with particular =20
interest in compositional game-semantic models. Typical but not =20
exclusive areas of interest are:
* categorical aspects;
* algorithmic aspects;
* programming languages and full abstraction;
* semantics of logics and proof systems;
* proof search;
* higher-order automata;
* program verification and model checking;
* program analysis;
* security;
* theories of concurrency;
* probabilistic models.
Publication
This is intended to be an informal workshop without widely =20
distributed proceedings. We therefore ask for submission both of =20
short abstracts outlining what will be presented at the workshop and =20
of longer papers describing completed work, either published or =20
unpublished, in the relevant areas.
A special issue of the journal Annals of Pure and Applied Logic =20
associated with the workshop will be discussed at the workshop.
Important dates
# Submission: February 14
# Notification: March 1
# Workshop: April 5-6
Invited speakers
# Gabriel Sandu, Helsinki
# Paul-Andr=E9 Melli=E8s, PPS
Program committee
# Dan Ghica (co-chair), Birmingham
# Russ Harmer (co-chair), PPS
# Martin Hyland, Cambridge
# Pierre Hyvernat, Savoie
# Jim Laird, Bath
# John Longley, Edinburgh
# Andrzej Murawski, Oxford
# Andrea Schalk, Manchester
---
Dr. Dan Ghica, Lecturer
School of Computer Science
University of Birmingham
Birmingham B15 2TT
tel: +44 121 414 8819
mailto:D.R.Ghica@cs.bham.ac.uk
http://www.cs.bham.ac.uk/~drg
From rrosebru@mta.ca Mon Feb 4 14:47:34 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 04 Feb 2008 14:47:34 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JM6HU-0001LG-UU
for categories-list@mta.ca; Mon, 04 Feb 2008 14:43:00 -0400
From: Thomas Streicher
Subject: categories: Colloquium Logicum 2008, September 10-12
To: categories@mta.ca
Date: Mon, 4 Feb 2008 17:02:33 +0100 (CET)
MIME-Version: 1.0
Content-Transfer-Encoding: 7bit
Content-Type: text/plain; charset=US-ASCII
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 14
---------------------------------------------------------------
Colloquium Logicum 2008, September 10-12, TU Darmstadt, Germany
---------------------------------------------------------------
The biennial meeting of the German Society for Mathematical Logic (DVMLG),
Colloquium Logicum 2008, will be held at the Technische Universitaet
Darmstadt, September 10-12, 2008.
The scientific programme comprises
* Herbrand Centenary Lecture: Georg Kreisel, F.R.S., Salzburg
* invited plenary lectures by
* Hans Adler (Leeds)
* Sergei Goncharov (Novosibirsk)
* Joel David Hamkins (New York)
* Robert Lubarsky (Florida)
* Nicole Schweikardt (Frankfurt)
* Michiel van Lambalgen (Amsterdam)
plus a PhD Colloquium with the presentation of selected recent
PhD Theses in Logic as well as contributed talks.
Further details about the meeting, registration, etc. will be published on
the meeting's homepage in the near future:
www.mathematik.tu-darmstadt.de/fbereiche/logik/events/collogicum/.
-------
From rrosebru@mta.ca Tue Feb 5 14:34:19 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Tue, 05 Feb 2008 14:34:19 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JMSQI-0001kt-HN
for categories-list@mta.ca; Tue, 05 Feb 2008 14:21:34 -0400
Date: Tue, 5 Feb 2008 19:11:21 +0200
From: Doron Peled
To:
Subject: categories: CFP: 5th Workshop on Model Checking and AI
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 15
- Call for Papers -
Fifth Workshop on
MODEL CHECKING and ARTIFICIAL INTELLIGENCE (MoChArt-2008)
At ECAI-2008 - Patras, Greece, July 2008
http://www.csc.liv.ac.uk/~mjw/mochart/
INTRODUCTION
Model checking is the process of determining whether or not a formula
of some logic is satisfied by a model for the logic. For many logics
of interest -- particularly temporal and modal logics -- model
checking procedures can be efficiently automated. This has led to
widespread interest in the use of model checking as a technique for
verifying properties of systems, and the development of a number of
widely used model checking tools (e.g., Carnegie-Mellon's SMV,
Cadence-SMV, and AT&T's SPIN).
The success of model checking in the computer aided verification
community has led to a growth of interest in the use of model checking
in AI. The MOCHART workshop brings together both researchers in AI
with an interest in model checking, and researchers in model checking
who are interested in AI techniques.
Previous editions of the workshop were held in Riva del Garda, Italy
in 2006 (as satellite workshops of ECAI), San Francisco in 2005 (as
satellite workshop of Concur), Acapulco in 2003 (as satellite workshop
of IJCAI03), and Lyon in 2002 (as satellite workshop of ECAI02). We
are exploring the possibility of publishing a formal proceedings after
the event with Springer-Verlag.
TOPICS OF INTEREST
Topics of interest include (but are not limited to):
- Application of model checking techniques to AI problems.
- planning as model checking
- model checking for multi-agent systems
- diagnosis and model checking
- model checking versus theorem proving
- Model Checking and AI logics.
- model checking for combined modal/temporal logics
- model checking for logics of common sense reasoning
- Relations between different techniques used in the two fields for
similar purposes (e.g., reducing state explosion).
- New model checking techniques specifically for AI problems.
- Exploitation of AI techniques in model checking.
- AI approaches to the state explosion problem
- heuristics for model checking
- AI approaches to automatic abstraction
- Software tools for model checking in AI.
- languages and software platforms for AI model checking
- model checking symbolic reasoning systems & languages
- Model checking for verification of AI systems.
- automated verification of AI systems
- case studies & experience with model checking in AI
Preliminary papers and papers on applications are strongly encouraged.
IMPORTANT DATES
Deadline for submissions: April 10th, 2008
Notification: May 10th, 2008
Workshop: July 21st-22nd, 2008
SUBMISSION PROCEDURES
Submissions must be formatted according to Springer-Verlag's "Lecture
Notes in Computer Science" styles, and must be no more than 15 pages
in length. Papers must be submitted through the EasyChair web-based
conference management system: follow the link from the workshop web
page. All papers will be peer reviewed, and evaluated on the basis of
relevance, technical quality, significance, evaluation, and
presentation.
PARTICIPATION
The workshop forms part of the ECAI-2008 workshop programme, and as
such delegates must register for the ECAI conference. For full
information about ECAI-2008, including travel & accomodation, see:
ORGANISING COMMITTEE
* Doron Peled
Department of Computer Science
Bar-Ilan University
Ramat Gan, 52900 Israel
mailto:doron.peled@gmail.com
* Michael Wooldridge
Department of Computer Science
University of Liverpool
Liverpool L69 7ZF, United Kingdom
mailto:mjw@liv.ac.uk
PROGRAM COMMITTEE
* Rajeev Alur (USA)
* Massimo Benerecetti (Italy)
* Rafael Bordini (UK)
* Kousha Etessami (UK)
* Michael Fisher (UK)
* Gerard Holzmann (USA)
* Hadas Kress-Gazit (USA)
* Orna Kupferman (Israel)
* Alessio Lomuscio (UK)
* Ron van de Meyden (Australia)
* Peter Niebert (France)
* Charles Pecheur (USA)
* Wojciech Penczek (Poland)
* Franco Raimondi (UK)
* Mark Ryan (UK)
* Farn Wang (China)
From rrosebru@mta.ca Wed Feb 6 15:15:21 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 06 Feb 2008 15:15:21 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JMpVq-0002kj-Cc
for categories-list@mta.ca; Wed, 06 Feb 2008 15:00:50 -0400
Date: Wed, 06 Feb 2008 13:31:38 -0500
From: Jacques Carette
MIME-Version: 1.0
To: categories
Subject: categories: Looking for some categorical PhD theses
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 16
In particular I cannot seem to find these:
D.S. Rajan, "Differentiation and Integration of the Combinatorial
Species of Joyal", PhD Thesis, Dept. of Mathematics, SUNY at Buffalo.
Yeong-Nan Yeh, "On the Combinatorial Species of Joyal", PhD Thesis,
Dept. of Mathematics, SUNY at Buffalo.
Electronic versions would be extremely welcome. If only paper versions
exist (but you have a copy!), contact me by email and we can work out an
appropriate method of duplication+transmission.
Jacques
From rrosebru@mta.ca Wed Feb 6 15:15:22 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 06 Feb 2008 15:15:22 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JMpVB-0002f6-8W
for categories-list@mta.ca; Wed, 06 Feb 2008 15:00:09 -0400
To: categories@mta.ca
Subject: categories: second call for papers
From: Myriam Quatrini
Date: Wed, 6 Feb 2008 10:59:14 +0100
Content-Transfer-Encoding: quoted-printable
Content-Type: text/plain;charset=ISO-8859-1;format=flowed
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 17
SECOND CALL FOR PAPERS
Workshop on Symmetric calculi and Ludics for the semantic=20
interpretation (http://iml.univ-mrs.fr/~quatrini/ESSLLI2008.html)
August 4-8, 2008
organized as part of the European Summer School on Logic, Language and
Information ESSLLI 2008 (http://www.illc.uva.nl/ESSLLI2008/), 4-15
August, 2008 in Hamburg, Germany
Workshop Organizers:
Alain Lecomte (SFL - Paris 8), Alain.Lecomte@upmf-grenoble.fr
Myriam Quatrini (IML Marseille), quatrini@iml.univ-mrs.fr
Workshop Purpose and topics:
In recent years there have been some important new developments of=20
methods of dealing with semantic and pragmatic phenomena in=20
Linguistics, inspired by developments in Logic and Theoretical Computer=20=
Science. Among these developments, Continuation Theory, Symmetric=20
calculi and Ludics play an important role. Continuation theory dates=20
back from the early seventies (cf. Reynolds, 93) and was at the heart=20
of Programming Languages like Scheme. More recently, a logical account=20=
was given to it, by extending the Curry-Howard homomorphism (Griffin,=20
1990),. This led to several calculi like such as Parigot's=20
lambda-mu-calculus, Curien-Herbelin's lambda-mu-mu-tilde-calculus,=20
Wadler's dual calculus and so on. These calculi are based on the core=20
idea that programs and contexts are dual entities and this is reflected=20=
in the symmetry of the "classical" sequents. These systems were=20
prefigured by the so called Lambek-Grishin calculus (Grishin, 83), a=20
calculus extending the Lambek calculus by taking classical sequents=20
into account. Following Curien-Herbelin (Bernardi and Moortgat, 2007)=20
focuses on the connection between Lambek-Grishin calculus with=20
lambda-mu-tilde-calculus and hence with continuation semantics.
Classical linear logic (Girard, 87, 95) gives another viewpoint, where=20=
the co-product is realized by an authentic parallelisation connective.=20=
Linguistic applications have been given since around 2000, particularly=20=
by C. Barker (Barker, 2002), K. Chung-chieh Shan (Chung-chieh Shan,=20
2002) and P. de Groote (de Groote, 2001) who exploited the advantages=20
of these systems in the task of giving several readings of an ambiguous=20=
sentence. De Groote (de Groote, 2007) also shows that we gain a new=20
dynamical logic which enables us to elegantly treat phenomena of=20
discourse like anaphora resolution. M. Moortgat and R. Bernardi=20
(Moortgat & Bernardi, 2007) shows how moving to a symmetric categorial=20=
grammar, namely Lambek Grishin calculus, helps accounting for=20
discontinous phenomena that are not captured by the asymmetric Lambek=20
calculus. Independently, linear logic was intensively studied in=20
particular by Girard himself who invented "Ludics" as a new conception=20=
of logic, where the dualism between syntax and semantics is abolished :=20=
the meaning of rules is in the rules themselves. This conception has=20
some similarities with more traditional "Game Semantics" (Lorenz,=20
Lorenzen, Hintikka...) but it is dynamic, in the sense that=20
"strategies" are replaced by interacting processes. Moreover, a new=20
step in abstraction is provided, which consists in stating rule=20
schemata which are only expressed in terms of loci (that we may see as=20=
memory cells).
The two approaches in this workshop are connected, basically because=20=
of their common root : explorations in the meaning of Logics and in=20
particular reflections on one of the symmetrical systems, namely linear=20=
logic. Linguistic applications of Ludics remain very embryonic, but=20
some authors have already emphasized that it is suitable for giving a=20
framework in which it is possible to study speech acts and dialogue=20
(Livet, 2007, Troncon, 2006). Other authors have pointed out=20
similarities of the Ludics' philosophy with Wittgenstein's views on=20
language games (Pietarinen, 2006). This workshop will provide an=20
opportunity to study these questions. It will accept several kinds of=20
contributions : theoretical works on continuation theory, symmetric=20
calculi and ludics, applied works of these theory concerning linguistic=20=
topics (semantics, pragmatics) and philosophical investigations.
Submission Details:
Authors are invited to submit an anonymous, extended abstract.=20
Submissions should not exceed 7 pages, including references.=20
Submissions should be in PDF format. Please send your submission=20
electronically using the interface EasyChair. The submissions will be=20
reviewed by the workshop's programme committee.
Workshop format:
The workshop is part of ESSLLI and is open to all ESSLLI participants.=20=
It will consist of five 90-minute sessions held over five consecutive=20
days in the first week of ESSLLI. There will be 2 slots for paper=20
presentation and discussion per session. On the first day the workshop=20=
organisers will give an introduction to the topic.
Invited Speakers:
Philippe de Groote, LORIA, France.
Additional invited speaker to be confirmed
Workshop Programme Committee:
Raffaella Bernardi (Bolzano)
Claire Beyssade (Institut Jean Nicod, Paris)
Marie-Ren=E9e Fleury (IML - Marseille)
Philippe de Groote (LORIA - Nancy)
Hugo Herbelin (Paris)
Jean-Baptiste Joinet (Paris 1)
Greg Kobele (Humboldt Universitat zu Berlin)
Alain Lecomte (SFL - Paris 8)
Pierre Livet (Aix en Provence)
Richard Moot (LABRI - Bordeaux)
Sylvain Pogodalla (LORIA - Nancy)
Carl Pollard (Ohio University)
Myriam Quatrini (IML Marseille)
Christian Retor=E9 (LABRI - Bordeaux)
Laurent Roussarie (SFL - Paris 8)
Sylvain Salvati (LABRI - Bordeaux)
Important Dates:
Submission Deadline: March 8, 2008
Notification: April 21, 2008
Preliminary Program: April 24, 2008
ESSLLI Early Registration: May 1, 2008
Final Papers for Proceedings: May 17, 2008
Final Program: June 21, 2008
Workshop Dates: August 11-15, 2008
Local Arrangements:
All workshop participants including the presenters will be required to
register for ESSLLI. The registration fee for authors presenting a
paper will correspond to the early student/workshop speaker
registration fee. There will be no reimbursement for travel costs and
accommodation.
Further Information:
About the workshop: http://iml.univ-mrs.fr/~quatrini/ESSLLI2008.html
About ESSLLI: http://www.illc.uva.nl/ESSLLI2008/
From rrosebru@mta.ca Thu Feb 7 17:22:21 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 07 Feb 2008 17:22:21 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JNDzY-0003pl-Hj
for categories-list@mta.ca; Thu, 07 Feb 2008 17:09:08 -0400
Date: Thu, 7 Feb 2008 20:05:47 +0000 (GMT)
From: Paul B Levy
To: categories@mta.ca
Subject: categories: question about monoidal categories
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 18
Let F be a functor from a monoidal category M to a category S.
We are given
beta(p,a) : F(p) --> F(p*a)
natural in p,a in M.
If I tell you that, in addition to naturality, beta is "monoidal", I'm
sure you will immediately guess what I mean by this, viz.
(a) for any p,a,b in M
beta(p,a) ; beta(p*a,b) = beta(p,a*b) ; F(alpha(p,a,b))
(b) for any p in M
beta(p,1) = F(rho(p))
Yet I cannot see any reason for giving the name "monoidality" to (a)-(b).
It doesn't appear to be a monoidal natural transformation in the official
sense. There are no monoidal functors in sight.
Can somebody please justify my usage?
Paul
From rrosebru@mta.ca Fri Feb 8 15:00:05 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 08 Feb 2008 15:00:05 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JNYPB-0004d5-BI
for categories-list@mta.ca; Fri, 08 Feb 2008 14:56:57 -0400
Mime-Version: 1.0 (Apple Message framework v753)
Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed
Content-Transfer-Encoding: 7bit
From: Sam Staton
Subject: categories: Re: question about monoidal categories
Date: Fri, 8 Feb 2008 09:51:09 +0000
To: categories@mta.ca
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 19
Hello, here is an answer to Paul's question: The data (F,beta)
defines a (lax?) functor between "monoidal categories with right
units but not left units" [henceforth MR-categories].
Every pointed category can be considered as an MR-category, in fact a
strict one. The tensor product is left projection. The right unit is
the point of the category (although every object of the category
behaves like a right unit for this category.)
In particular, the category S in Paul's email, with point F(1), can
be seen as an MR-category. Of course, every monoidal category,
including M, is an MR-category too.
The data for a lax MR-functor M->S consists of a functor F:M->S, a
morphism F(i)->F(i), which we can take as identity, and a natural
transformation
F(p)*F(a) --> F(p*a)
which in this case amounts to a map
beta:F(p) --> F(p*a)
A monoidal functor must satisfy three coherence conditions,
for associativity, left identity and right identity.
For an MR-functor, there are only axioms for associativity and right
identity, and these are exactly the axioms that Paul gave.
Hope that makes sense! All the best, Sam.
On 7 Feb 2008, at 20:05, Paul B Levy wrote:
>
>
>
> Let F be a functor from a monoidal category M to a category S.
>
> We are given
>
> beta(p,a) : F(p) --> F(p*a)
>
> natural in p,a in M.
>
> If I tell you that, in addition to naturality, beta is "monoidal", I'm
> sure you will immediately guess what I mean by this, viz.
>
> (a) for any p,a,b in M
>
> beta(p,a) ; beta(p*a,b) = beta(p,a*b) ; F(alpha(p,a,b))
>
> (b) for any p in M
>
> beta(p,1) = F(rho(p))
>
> Yet I cannot see any reason for giving the name "monoidality" to
> (a)-(b).
>
> It doesn't appear to be a monoidal natural transformation in the
> official
> sense. There are no monoidal functors in sight.
>
> Can somebody please justify my usage?
>
> Paul
>
>
From rrosebru@mta.ca Fri Feb 8 15:00:05 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 08 Feb 2008 15:00:05 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JNYOU-0004YU-Ji
for categories-list@mta.ca; Fri, 08 Feb 2008 14:56:14 -0400
Mime-Version: 1.0 (Apple Message framework v752.2)
Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed
To: categories@mta.ca
Content-Transfer-Encoding: 7bit
From: Marco Grandis
Subject: categories: Re: question about monoidal categories
Date: Fri, 8 Feb 2008 09:31:58 +0100
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 20
Dear Paul,
Let us forget about the monoidal unit and fix (a).
You define a strict semi? monoidal structure on S letting x*y = x.
Then your pair (F, beta) is a lax monoidal functor M --> S. Your
condition (a) is the hexagon of consistency with alpha, which here
reduces to:
F(p) = F(p)
|| |
F(p) F(p*a)
| |
F(p*(a*b) --> F((p*a)*b)
(a single | stands for a downward beta)
Now, to fix also (b), I guess you should add to S a new object which
is a strict identity for the tensor and work out things.
However, if your problem is only about terminology and you do not
want to use the tensor on S in the sequel (eg to compose F with other
monoidal functors), you might not bother about that.
Best regards
Marco
From rrosebru@mta.ca Fri Feb 8 15:00:05 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 08 Feb 2008 15:00:05 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JNYNc-0004QF-Vg
for categories-list@mta.ca; Fri, 08 Feb 2008 14:55:21 -0400
Date: Thu, 7 Feb 2008 18:58:47 -0500 (EST)
From: Jeff Egger
Subject: categories: Re: question about monoidal categories
To: categories@mta.ca
MIME-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 21
Hi Paul,=20
I think that I have written previously to the list about the=20
possibility of a monoidal functor acting on a mere functor,=20
and what you have is an instance of this notion. =20
Here the monoidal functor is the unique functor M ---> T,
where T is the terminal (monoidal) category. Your beta is=20
a right action of this guy on F.
In general, a right action of monoidal A --U--> C on mere=20
P --F--> S requires a right action of A on P and a right=20
action of C on S as well as a natural transformation=20
F(p)*U(a) --beta(p,a)--> F(p*a)=20
satisfying the appropriate associativity and unit axioms.
In your case S is equipped with the trivial right T-action=20
(x*1=3Dx), and M with its canonical right M-action (a*b=3Da*b). =20
The axioms are identical.
Cheers,
Jeff.
--- Paul B Levy wrote:
>=20
>=20
>=20
> Let F be a functor from a monoidal category M to a category S.
>=20
> We are given
>=20
> beta(p,a) : F(p) --> F(p*a)
>=20
> natural in p,a in M.
>=20
> If I tell you that, in addition to naturality, beta is "monoidal", I'm
> sure you will immediately guess what I mean by this, viz.
>=20
> (a) for any p,a,b in M
>=20
> beta(p,a) ; beta(p*a,b) =3D beta(p,a*b) ; F(alpha(p,a,b))
>=20
> (b) for any p in M
>=20
> beta(p,1) =3D F(rho(p))
>=20
> Yet I cannot see any reason for giving the name "monoidality" to (a)-(b=
).
>=20
> It doesn't appear to be a monoidal natural transformation in the offici=
al
> sense. There are no monoidal functors in sight.
>=20
> Can somebody please justify my usage?
>=20
> Paul
>=20
>=20
>=20
Be smarter than spam. See how smart SpamGuard is at giving junk ema=
il the boot with the All-new Yahoo! Mail. Click on Options in Mail and s=
witch to New Mail today or register for free at http://mail.yahoo.ca=20
From rrosebru@mta.ca Fri Feb 8 15:00:05 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 08 Feb 2008 15:00:05 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JNYMo-0004Ix-RO
for categories-list@mta.ca; Fri, 08 Feb 2008 14:54:30 -0400
Date: Thu, 7 Feb 2008 22:36:24 +0000 (GMT)
From: Richard Garner
To: categories@mta.ca
Subject: categories: Re: question about monoidal categories
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 22
Dear Paul,
Here is one possible answer to your question.
One has a notion of action of a monoidal category V on an
arbitrary category X, which generalises that of action by a
monoid on a set; thus we have a functor
(-) * (-): X x V --> X
together with natural isomorphisms x * I ~ x and x * (v * w)
~ (x * v) * w satisfying pentagon and triangle axioms.
Formally, one may define an action of V on X to be a strong
monoidal functor V --> [X, X], where the latter is equipped
with its compositional monoidal structure.
If we are given two categories X and Y equipped with an
action by V, then we have a notion of equivariant morphism
between them; namely a functor F: X --> Y together with
natural morphisms
m_{x, v} : F(x) * v --> F(x * v)
obeying axioms like those for a monoidal functor. This is
what one might call a lax equivariant morphism; if the m_{x, v}'s
are all invertible we should rather call it strong,
whilst if they point in the opposite direction then what we
have is an oplax morphism.
The situation you have described is a special case of an lax
equivariant morphism. You have a monoidal category M, and a
functor F : M --> S. Now, M has a canonical action on itself
induced by tensoring on the right (the "right regular
representation"); and it has a trivial action on S given by
s * m = s for all s and m. Your natural transformation beta
can now be written as
beta(p, a) : F(p) * a --> F(p * a),
and your two axioms are precisely the axioms required for
beta to equip F with the structure of a lax equivariant
morphism.
This whole area of monoidal actions is slightly folklorish
but a useful source is:
George Janelidze and Max Kelly, "A note on actions of a
monoidal category", TAC Vol. 9, No. 4
Also worth mentioning is the work of Paddy McCrudden who has
studied actions by a symmetric monoidal V under the name
"V-actegories".
Hope this is of some help,
Richard
--On 07 February 2008 20:05 Paul B Levy wrote:
>
>
>
> Let F be a functor from a monoidal category M to a category S.
>
> We are given
>
> beta(p,a) : F(p) --> F(p*a)
>
> natural in p,a in M.
>
> If I tell you that, in addition to naturality, beta is "monoidal", I'm
> sure you will immediately guess what I mean by this, viz.
>
> (a) for any p,a,b in M
>
> beta(p,a) ; beta(p*a,b) = beta(p,a*b) ; F(alpha(p,a,b))
>
> (b) for any p in M
>
> beta(p,1) = F(rho(p))
>
> Yet I cannot see any reason for giving the name "monoidality" to (a)-(b).
>
> It doesn't appear to be a monoidal natural transformation in the official
> sense. There are no monoidal functors in sight.
>
> Can somebody please justify my usage?
>
> Paul
>
>
>
From rrosebru@mta.ca Fri Feb 8 20:49:31 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 08 Feb 2008 20:49:31 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JNdjV-0002M2-Ux
for categories-list@mta.ca; Fri, 08 Feb 2008 20:38:18 -0400
Date: Fri, 8 Feb 2008 20:03:46 +0000 (GMT)
From: Richard Garner
To: categories@mta.ca
Subject: categories: Re: question about monoidal categories
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 23
As an addendum to the interesting answers that have been
given so far to Paul's question, it is perhaps worth pointing
out that using an old result of Max Kelly's, the situation
Paul describes can be expressed purely in terms of a strong
monoidal functor.
Given a monoidal category M and functor F : M --> S as in
Paul's message, we define a strict monoidal category {F, F}
as follows. Its objects are triples (G, H, a) fitting into a
diagram of functors and natural transformations
G
M -----> M
| |
| a |
F | => | F
| |
v v
S -----> S
H
Its morphisms (G, H, a) --> (G', H', a') are pairs of natural
transformations b : G => G', c : H => H' satisfying the
obvious compatibility condition with a and a'. The tensor
product is given by pasting squares next to each other
horizontally.
There are strict monoidal functors p_1 : {F, F} -> [M, M]
and p_2 : {F, F} -> [S, S] sending (G, H, a) to G and H
respectively; and as in my previous message we have strong
monoidal functors
R : M ---> [M, M]
m |--> (-) * m
T : M ---> [S, S]
m |--> id_S
corresponding to the right regular action of M on itself,
and to the trivial action of M on S.
Now to give the natural transformation beta of Paul's
message, satisfying his "monoidality" conditions, is
precisely to give a strong monoidal functor B: M --> {F, F}
rendering the diagram
_ {F, F}
.| |
. |
B . | (p_1, p_2)
. |
. v
M --------> [M, M] x [S, S]
(R, T)
commutative.
I believe this technique originates in the paper
"Coherence theorems for lax algebras and for distributive
laws", G.M. Kelly, LNM 420.
A good place to learn more about it is in Section 2 of
"On property-like structures", G.M. Kelly and S. Lack, TAC Vol. 3, No. 9
Richard
--On 07 February 2008 20:05 Paul B Levy wrote:
>
>
>
> Let F be a functor from a monoidal category M to a category S.
>
> We are given
>
> beta(p,a) : F(p) --> F(p*a)
>
> natural in p,a in M.
>
> If I tell you that, in addition to naturality, beta is "monoidal", I'm
> sure you will immediately guess what I mean by this, viz.
>
> (a) for any p,a,b in M
>
> beta(p,a) ; beta(p*a,b) = beta(p,a*b) ; F(alpha(p,a,b))
>
> (b) for any p in M
>
> beta(p,1) = F(rho(p))
>
> Yet I cannot see any reason for giving the name "monoidality" to (a)-(b).
>
> It doesn't appear to be a monoidal natural transformation in the official
> sense. There are no monoidal functors in sight.
>
> Can somebody please justify my usage?
>
> Paul
>
>
>
From rrosebru@mta.ca Sun Feb 10 20:54:05 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 10 Feb 2008 20:54:05 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JOMiw-0000iu-Cb
for categories-list@mta.ca; Sun, 10 Feb 2008 20:40:42 -0400
Date: Sun, 10 Feb 2008 11:03:59 -0500 (EST)
From: Jeff Egger
Subject: categories: Uniformity via Cauchy filters?
To: categories@mta.ca
MIME-Version: 1.0
Content-Type: text/plain; charset=iso-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 24
Dear categorists,
One of my current research projects has drifted into the realm=20
of uniform locales, which is not exactly my forte. As I went=20
to re-familiarise myself with the assorted definitions, I found
myself wondering whether one could define a uniform locale as a=20
locale equipped with a designated set of Cauchy filters, instead=20
of uniform covers, or entourages. Does anyone know whether this=20
idea has already been pursued, either for locales or for spaces? =20
Cheers,
Jeff.
=20
Looking for the perfect gift? Give the gift of Flickr!=20
http://www.flickr.com/gift/
From rrosebru@mta.ca Mon Feb 11 10:41:14 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 11 Feb 2008 10:41:14 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JOZi9-00022E-61
for categories-list@mta.ca; Mon, 11 Feb 2008 10:32:45 -0400
Date: Mon, 11 Feb 2008 11:32:53 +0100
From: Lutz Schroeder
MIME-Version: 1.0
To: categories
Subject: categories: AMAST'08 Final Call-For-Papers
Content-Type: text/plain; charset=ISO-8859-15
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 25
[Apologies for multiple copies.]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% The 12th International Conference on %
% Algebraic Methodology and Software Technology %
% AMAST 2008 %
% %
% July 28-31, 2008 %
% University of Illinois %
% Urbana-Champaign, Illinois, USA %
% %
% http://amast08.cs.uiuc.edu %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
SCOPE AND AIMS
==============
The major goal of the AMAST conferences is to promote research towards
setting software technology on a firm, mathematical basis. Work towards
this goal is a collaborative, international effort with contributions
from both academia and industry. The envisioned virtues of providing
software technology developed on a mathematical basis include
(a) correctness, which can be proved mathematically,
(b) safety, so that developed software can be used in the implementation
of critical systems,
(c) portability, i.e., independence from computing platforms and
language generations, and
(d) evolutionary change, i.e., the software is self-adaptable and
evolves with the
problem domain.
The previous conferences were held in: Iowa City, Iowa, USA (1989,
1991 and 2000); Twente, The Netherlands (1993); Montreal, Canada
(1995); Munich, Germany (1996); Sydney, Australia (1997); Manaus,
Amazonia, Brazil (1998); Reunion Island, France (2002); Stirling, UK
(2004, colocated with MPC' 04); Kuressaare, Estonia (2006, colocated
with MPC '06).
Topics of interest include, but are not limited to, the following:
SOFTWARE TECHNOLOGY:
- systems software technology
- application software technology
- concurrent and reactive systems
- formal methods in industrial software development
- formal techniques for software requirements, design
- evolutionary software/adaptive systems
PROGRAMMING METHODOLOGY:
- logic programming, functional programming, object paradigms
- constraint programming and concurrency
- program verification and transformation
- programming calculi
- specification languages and tools
- formal specification and development case studies
ALGEBRAIC AND LOGICAL FOUNDATIONS:
- logic, category theory, relation algebra, computational algebra
- algebraic foundations for languages and systems, coinduction
- theorem proving and logical frameworks for reasoning
- logics of programs
- algebra and coalgebra
SYSTEMS AND TOOLS (for system demonstrations or ordinary papers):
- software development environments
- support for correct software development
- system support for reuse
- tools for prototyping
- component based software development tools
- validation and verification
- computer algebra systems
- theorem proving systems
INVITED SPEAKERS
================
Rajeev Alur (confirmed)
Edmund M. Clarke
Jayadev Misra (confirmed)
Teodor Rus (confirmed)
AMAST steering committee
========================
Michael Johnson Macquarie University (chair)
Egidio Astesiano Universita degli Studi di Genova
Robert Berwick MIT
Zohar Manna Stanford University
Michael Mislove Tulane University
Anton Nijholt University of Twente
Maurice Nivat Universite Paris 7
Charles Rattray University of Stirling
Teodor Rus University of Iowa
Giuseppe Scollo Universita degli Studi di Catania
Michael Sintzoff Universite Catholique de Louvain
Jeannette Wing Carnegie Mellon University
Martin Wirsing Ludwig-Maximilians-Universitat Munchen
PROGRAM COMMITTEE
=================
Gilles Barthe France INRIA Sophia-Antipolis
Michel Bidoit France INRIA Saclay - Ile-de-France
Manfred Broy Germany Technische Universitat Munchen
Roberto Bruni Italy University of Pisa
Mads Dam Sweden Royal Institute of Technology (KTH),
Stockholm
Razvan Diaconescu Romania Institute of Mathematics (IMAR)
Jose Fiadeiro UK University of Leicester
Rob Goldblatt New Zealand Victoria University
Bernhard Gramlich Austria Vienna University of Technology
Radu Grosu USA State University of New York at Stony Brook
Anne Haxthausen Denmark Technical University of Denmark
Rolf Hennicker Germany Ludwig-Maximilians-Universitat Munchen
Michael Johnson Australia Macquarie University
Helene Kirchner France INRIA Loria, Nancy
Paul Klint The Netherlands CWI and Universiteit van
Amsterdam
Gary T. Leavens USA University of Central Florida
Narciso Marti-Oliet Spain Universidad Complutense de Madrid
Jose Meseguer (co-chair) USA University of Illinois at Urbana-Champaign
Michael Mislove USA Tulane University
Ugo Montanari Italy University of Pisa
Larry Moss USA Indiana University
Till Mossakowski Germany DFKI Bremen
Peter Mosses UK Swansea University
Fernando Orejas Spain Technical University of Catalonia,
Barcelona
Dusko Pavlovic USA Kestrel Institute and Oxford University
Grigore Rosu (co-chair) USA University of Illinois at Urbana-Champaign
Jan Rutten The Netherlands CWI and Vrije Universiteit
Amsterdam
Lutz Schroeder Germany DFKI Bremen/Universitat Bremen
Wolfram Schulte USA Microsoft Research
Giuseppe Scollo Italy Universita di Catania
Henny Sipma USA Stanford University
Doug Smith USA Kestrel Institute
Carolyn Talcott USA SRI International
Andrzej Tarlecki Poland Warsaw University
Varmo Vene Estonia University of Tartu
Martin Wirsing Germany Ludwig-Maximilians-Universitat Munchen
Uwe Wolter Norway University of Bergen
LOCAL ORGANIZATION
==================
(all at the University of Illinois Urbana-Champaign)
Jose Meseguer
Mark Hills
Grigore Rosu
Ralf Sasse
IMPORTANT DATES
===============
* Submission of abstracts: 1 March 2008
* Submission of full papers: 8 March 2008
* Notification of authors: 20 April 2008
* Camera-ready version: 15 May 2008
SUBMISSION
==========
Two kinds of submissions are solicited for this conference: technical
papers and system demonstrations. Papers may report academic or
industrial progress, and papers which deal with both are especially
well-regarded.
Submission is in two stages. Abstracts (plain text) must be submitted
by 1 March 2008. Full papers (pdf) adhering to the llncs style and not
longer than 15 pages (6 pages for system demonstrations) must be
submitted by 8 March 2008.
Submissions will be open soon.
Papers must report previously unpublished work and not be submitted
concurrently to another conference with refereed proceedings. Accepted
papers must be presented at the conference by one of the authors.
All papers will be refereed by the programme committee, and will be
judged based on their significance, technical merit, and relevance to
the conference.
The proceedings of AMAST '08 will be published in the Lecture Notes in
Computer Science series of Springer-Verlag.
From rrosebru@mta.ca Mon Feb 11 19:38:44 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 11 Feb 2008 19:38:44 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JOi8k-0003tl-A2
for categories-list@mta.ca; Mon, 11 Feb 2008 19:32:46 -0400
Date: Mon, 11 Feb 2008 08:13:42 -0800 (PST)
From: Bill Rowan
To: categories@mta.ca
Subject: categories: Re: Uniformity via Cauchy filters?
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 26
Hi Jeff,
I don't know about locales, but I worked on issues surrounding taking a
uniform space, and forgetting the uniformity but keeping the set of cauchy
filters. This turns out to be a nontrivial amount of forgetting. I liked
the result because the resulting category, which I call the category of
completable spaces, can be used as a base category and, for example, if
you have a commutative ring, you can look at the compatible
completabilities on it (making it a completable space with the
discrete completability) and they generalize the valuations on a field.
Bill Rowan
On Sun, 10 Feb 2008, Jeff Egger wrote:
> Dear categorists,
>
> One of my current research projects has drifted into the realm
> of uniform locales, which is not exactly my forte. As I went
> to re-familiarise myself with the assorted definitions, I found
> myself wondering whether one could define a uniform locale as a
> locale equipped with a designated set of Cauchy filters, instead
> of uniform covers, or entourages. Does anyone know whether this
> idea has already been pursued, either for locales or for spaces?
>
> Cheers,
> Jeff.
>
>
>
> Looking for the perfect gift? Give the gift of Flickr!
>
> http://www.flickr.com/gift/
>
>
>
>
From rrosebru@mta.ca Mon Feb 11 19:38:44 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 11 Feb 2008 19:38:44 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JOi9t-000413-OE
for categories-list@mta.ca; Mon, 11 Feb 2008 19:33:57 -0400
Date: Mon, 11 Feb 2008 11:59:32 -0800
From: Toby Bartels
To: categories@mta.ca
Subject: categories: Re: Uniformity via Cauchy filters?
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 27
Jeff Egger wrote in part:
>one could define a uniform locale as a
>locale equipped with a designated set of Cauchy filters
This can be done, although you get a more general notion:
a _Cauchy_space_ (or locale, but spaces have a bigger literature).
Note that a uniform space is a Cauchy space with extra ~structure~;
there is no way, in a mere Cauchy space,
to compare sizes of neighbourhoods of different points.
For the basic definition, you could do worse than the English Wikipedia:
< http://en.wikipedia.org/wiki/Cauchy_space >.
I had some references (monographs) that I liked too,
but I can't find them now; perhaps I can find them tomorrow.
--Toby
From rrosebru@mta.ca Tue Feb 12 10:20:12 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Tue, 12 Feb 2008 10:20:12 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JOvna-0005CJ-Ve
for categories-list@mta.ca; Tue, 12 Feb 2008 10:07:51 -0400
From: Aleks Nanevski
To: categories@mta.ca
Date: Mon, 11 Feb 2008 17:24:15 +0000
Subject: categories: IMLA'08: Call for Papers
Content-Type: text/plain; charset="us-ascii"
Content-Transfer-Encoding: quoted-printable
MIME-Version: 1.0
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 28
Fourth Internation Workshop on
Intuitionistic Modal Logic and Applications
(IMLA'08)
(http://www.cs.bham.ac.uk/~vdp/IMLA08.html)
A LICS'08 affiliated workshop
Pittsburgh, Pennsylvania, June 23, 2008
Constructive modal logics and type theories are of increasing foundational =
and practical relevance in computer science. Applications are in type disci=
plines for programming languages, and meta-logics for reasoning about a var=
iety of computational phenomena.
Theoretical and methodological issues center around the question of how the=
proof-theoretic strengths of constructive logics can best be combined with=
the model-theoretic strengths of modal logics. Practical issues center aro=
und the question which modal connectives with associated laws or proof rule=
s capture computational phenomena accurately and at the right level of abst=
raction.
This workshop will bring together designers, implementers, and users to dis=
cuss all aspects of intuitionistic modal logics and type theories. Topics =
include, but are not limited to:
* applications of intuitionistic necessity and possibility
* monads and strong monads
* constructive belief logics and type theories
* applications of constructive modal logic and modal type theory to formal =
verification, foundations of security, abstract interpretation, and program=
analysis and optimization
* modal types for integration of inductive and co-inductive types, higher-o=
rder abstract syntax, strong functional programming
* models of constructive modal logics such as algebraic, categorical, Kripk=
e, topological, and realizability interpretations
* notions of proof for constructive modal logics
* extraction of constraints or programs from modal proofs
* proof search methods for constructive modal logics and their implementati=
ons
The workshop continues a series of previous LICS-affiliated workshops, whic=
h were held as part of FLoC'99, Trento, Italy and of FLoC'02,
Copenhagen, Denmark.
We solicit submissions on work in progress and on more mature results. Subm=
issions should be extended abstracts of 5-10 pages sent in
PostScript or PDF format to the program co-chair at aleksn@microsoft.com.
IMPORTANT DATES:
Submission: April 25, 2008
Notification: May 23, 2008
Final papers due: June 7, 2008
Workshop Date: June 23, 2008
It is planned to publish workshop proceedings as Electronic Notes in Theore=
tical Computer Science (ENTCS) or in CEURS, to be decided. Authors please u=
se the generic ENTCS macro package at http://www.math.tulane.edu/~entcs.
PROGRAM COMMITTEE:
Gavin Bierman (Microsoft, UK)
Valeria de Paiva (PARC, USA)
Michael Mendler (Bamberg, DE)
Aleks Nanevski (Microsoft, UK)
Brigitte Pientka (McGill, CA)
Eike Ritter (Birmingham, UK)
INVITED SPEAKERS:
Frank Pfenning (CMU, USA)
Torben Brauner (Roskilde, RK)
CONTACTS
Valeria de Paiva Aleks Nanevski
PARC, Palo Alto Research Center Microsoft Research
paiva@parc.xeroc.com aleksn@microsoft.com
From rrosebru@mta.ca Tue Feb 12 10:20:12 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Tue, 12 Feb 2008 10:20:12 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JOvoO-0005Jj-BE
for categories-list@mta.ca; Tue, 12 Feb 2008 10:08:40 -0400
Date: Tue, 12 Feb 2008 11:06:09 +0100 (MET)
From: Patrik Eklund
To: categories@mta.ca
Subject: categories: Re: Uniformity via Cauchy filters?
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 29
Might be interesting to note that Cauchy and filters with convergence
etc can be described now in more generality involving underlying
(partially ordered) monads.
See e.g.
http://books.google.com/books?id=EoJGeBZVOaQC&pg=PA65&lpg=PA65&dq=%22partially+ordered+monad%22+eklund&source=web&ots=Jg6-Pbj-z5&sig=lFHkMQ-_VjvQMxHMfTryuHprKPQ#PPA102,M1
http://sevein.matap.uma.es/~aciego/mat-es/patrik.pdf
Cheers,
Patrik
On Mon, 11 Feb 2008, Toby Bartels wrote:
> Jeff Egger wrote in part:
>
>> one could define a uniform locale as a
>> locale equipped with a designated set of Cauchy filters
>
> This can be done, although you get a more general notion:
> a _Cauchy_space_ (or locale, but spaces have a bigger literature).
> Note that a uniform space is a Cauchy space with extra ~structure~;
> there is no way, in a mere Cauchy space,
> to compare sizes of neighbourhoods of different points.
>
> For the basic definition, you could do worse than the English Wikipedia:
> < http://en.wikipedia.org/wiki/Cauchy_space >.
> I had some references (monographs) that I liked too,
> but I can't find them now; perhaps I can find them tomorrow.
>
>
> --Toby
>
>
From rrosebru@mta.ca Wed Feb 13 20:36:25 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 13 Feb 2008 20:36:25 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JPRvI-0001nZ-BS
for categories-list@mta.ca; Wed, 13 Feb 2008 20:25:56 -0400
Date: Tue, 12 Feb 2008 16:34:09 -0800
From: Toby Bartels
To: categories@mta.ca
Subject: categories: Re: Uniformity via Cauchy filters?
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 30
I wrote in part:
>I had some references (monographs) that I liked too,
>but I can't find them now; perhaps I can find them tomorrow.
I've (re-)found this one:
Eva Lowen-Colebunders (1989).
Function Classes of Cauchy Continuous Maps.
Dekker, New York, 1989.
This has many pretty diagrams of various categories of spaces,
all included in one another by bireflections and the like.
The whole subject seems messy, as point-set topology can be,
(there are too many categories around to keep track of),
and probably needs to be cleaned up somewhat
before outsiders (including me) can get a grasp on it;
in particular, perhaps locales would be a better approach.
OTOH, my reference is nearly 20 years old,
and perhaps the situation has improved.
Indeed, perhaps this is what Paul Ekland's references are doing;
I haven't looked at them carefully yet.
--Toby
From rrosebru@mta.ca Wed Feb 13 20:36:25 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 13 Feb 2008 20:36:25 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JPRtz-0001ar-RB
for categories-list@mta.ca; Wed, 13 Feb 2008 20:24:35 -0400
Date: Tue, 12 Feb 2008 18:15:06 +0100
From: =?ISO-8859-15?Q?Bernhard_M=F6ller?=
MIME-Version: 1.0
To: Verborgene_Empfaenger:;
Subject: categories: Call for Participation RELMICS10/AKA5
Content-Type: text/plain; charset=ISO-8859-15; format=flowed
Content-Transfer-Encoding: quoted-printable
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 31
[Apologies for multiple copies.]
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% %
% Call for Participation %
% %
% RELATIONS AND KLEENE ALGEBRA IN COMPUTER SCIENCE %
% %
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
10th International Conference on
Relational Methods in Computer Science (RelMiCS10)
joint with
5th International Conference on
Applications of Kleene Algebra (AKA5)
7-11 April 2008
Frauenw=F6rth (near Munich), Germany
http://www.uni-augsburg.de/rel_aka
The RelMiCS Conference is the main forum for the relational
calculus as a conceptual and methodological tool. The AKA
Conference is a meeting on topics related to Kleene algebras.
As in previous years, the two events are co-organised; they
have a joint programme committee and joint proceedings.
Registration deadline: 15 March 2006
PROGRAMME: The conference features 2 invited talks and 26
contributed papers. In addition, there is a PhD programme
with 3 invited tutorial and 8 contributed talks; participation
is open for everyone.
Invited Talks:
Marc Pauly (Standford)
Formal Methods and the Theory of Social Choice
Gunther Schmidt (Munich)
Relations Making Their Way From Logics
to Mathematics and Applied Sciences
The full programme as well as registration details are available
at the conference website. For further inquiries please contact
the local organisers under
rel_aka08@informatik.uni-augsburg.de.
SPONSORS:
ARIVA.DE AG (Kiel)
CrossSoft (Kiel)
Deutsche Forschungsgemeinschaft DFG
HSH Nordbank AG (Kiel)
COMMITTEES:
General Chair:
Rudolf Berghammer, Kiel, Germany
Bernhard Moeller, Augsburg, Germany
Local Organisation:
Bernhard Moeller, Augsburg, Germany
Roland Glueck, Augsburg, Germany
Peter Hoefner, Augsburg, Germany
Iris Kellner, Augsburg, Germany
Ulrike Pollakowski, Kiel, Germany
Programme Committee:
Rudolf Berghammer, Kiel, Germany
Harrie de Swart, Tilburg, The Netherlands
Jules Desharnais, Laval, Canada
Marcelo Frias, Buenos Aires, Argentina
Hitoshi Furusawa, Kagoshima, Japan
Peter Jipsen, Chapman, USA
Wolfram Kahl, McMaster, Canada
Yasuo Kawahara, Kyushu, Japan
Bernhard Moeller, Augsburg, Germany
Carroll Morgan New South Wales, Australia
Manuel Ojeda Aciego, M=E1laga, Spain
Ewa Orlowska, Warsaw, Poland
Susanne Saminger, Linz, Austria
Gunther Schmidt, Munich, Germany
Renate Schmidt, Manchester, UK
Giuseppe Scollo, Catania, Italy
Georg Struth, Sheffield, UK
Andrzej Szalas, Link=F6ping, Sweden
Johan van Benthem, Amsterdam, The Netherlands
Michael Winter, Brock U., Canada
--=20
Prof. Dr. Bernhard M=F6ller |
http://www.informatik.Uni-Augsburg.DE/~moeller/
Institut f=FCr Informatik | Tel: ++49-821-598-2164
Universit=E4t Augsburg | Fax: ++49-821-598-2274
Universit=E4tsstr. 14, D-86135 Augsburg, Germany
From rrosebru@mta.ca Thu Feb 14 22:59:36 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 14 Feb 2008 22:59:36 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JPqc4-0001pE-Rb
for categories-list@mta.ca; Thu, 14 Feb 2008 22:47:44 -0400
Date: Thu, 14 Feb 2008 15:06:49 -0500
From: PETER EASTHOPE
Subject: categories: A small cartesian closed concrete category
To: categories@mta.ca
MIME-version: 1.0
Content-type: text/plain; charset=us-ascii
Content-language: en
Content-transfer-encoding: 7bit
Content-disposition: inline
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 32
Is there a cartesian closed concrete category which
is small enough to write out explicitly? It would be
helpful in learning about map objects, exponentiation,
distributivity and etc. Can such a category be made
with binary numbers for instance?
Thanks, ... Peter E.
http://carnot.yi.org/
From rrosebru@mta.ca Fri Feb 15 10:43:09 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 15 Feb 2008 10:43:09 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JQ1hV-0006Xq-7n
for categories-list@mta.ca; Fri, 15 Feb 2008 10:38:05 -0400
Date: Thu, 14 Feb 2008 22:46:44 -0500
From: "Fred E.J. Linton"
Subject: categories: Re: A small cartesian closed concrete category
To:
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 33
On Thu, 14 Feb 2008 10:07:27 PM EST, PETER EASTHOPE
asked:
> Is there a cartesian closed concrete category which
> is small enough to write out explicitly? =
How about the full category of finite sets? Or, =
if that's not small enough, and you really fancy an example
> ... made with binary numbers for instance ,
try the skeletal version of the full category of "sets of cardinality < 2=
"
having as only objects the ordinal numbers 0 and 1.
Here 0 x A =3D 0, 1 x A =3D A, 0^1 =3D 0, 0^0 =3D 1, 1^A =3D 1.
In other words, B x A =3D min(A, B), B^A =3D max(1-A, B).
Happy Valentines's Day! -- Fred
From rrosebru@mta.ca Fri Feb 15 10:43:09 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 15 Feb 2008 10:43:09 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JQ1i2-0006co-PZ
for categories-list@mta.ca; Fri, 15 Feb 2008 10:38:38 -0400
Mime-Version: 1.0 (Apple Message framework v624)
Content-Type: text/plain; charset=US-ASCII; format=flowed
Content-Transfer-Encoding: 7bit
From: Paul Taylor
Subject: categories: Re: A small cartesian closed concrete category
Date: Fri, 15 Feb 2008 08:18:57 +0000
To: categories@mta.ca
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 34
Peter Easthope asked,
> Is there a cartesian closed concrete category which
> is small enough to write out explicitly? It would be
> helpful in learning about map objects, exponentiation,
> distributivity and etc. Can such a category be made
> with binary numbers for instance?
How about finite sets and functions?
Not just a CCC but an elementary topos.
I'm not sure what you mean by "binary numbers", but the powerset
of n is 2^n (I wonder why Cantor introduced this notation?),
and the subsets of n are n-digit binary numbers.
As for more general function spaces, maybe it's worth an
undergraduate exercise to see whether there's a neat
representation.
NBB: You don't need even to have heard of domain theory
to find examples of CCCs!
Paul Taylor
From rrosebru@mta.ca Fri Feb 15 15:23:16 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 15 Feb 2008 15:23:16 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JQ64W-0003yi-Ed
for categories-list@mta.ca; Fri, 15 Feb 2008 15:18:08 -0400
Date: Fri, 15 Feb 2008 13:08:11 -0600
From: "Matt Hellige"
Subject: categories: Re: A small cartesian closed concrete category
To: categories@mta.ca
MIME-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 35
On Thu, Feb 14, 2008 at 9:46 PM, Fred E.J. Linton wrote:
> On Thu, 14 Feb 2008 10:07:27 PM EST, PETER EASTHOPE
> asked:
>
> > Is there a cartesian closed concrete category which
> > is small enough to write out explicitly?
>
> try the skeletal version of the full category of "sets of cardinality < 2"
> having as only objects the ordinal numbers 0 and 1.
>
> Here 0 x A = 0, 1 x A = A, 0^1 = 0, 0^0 = 1, 1^A = 1.
> In other words, B x A = min(A, B), B^A = max(1-A, B).
>
Or, in case that's too small, what about any short chain? For
instance, let S = {0,1,2,3} and say there exists a morphism a -> b iff
a < b. I believe this is cartesian closed, and I believe it can easily
be understood as concrete. This should be enough to give non-trivial
product and exponentiation, but you can still draw the whole diagram.
Matt
--
Matt Hellige / matt@immute.net
http://matt.immute.net
From rrosebru@mta.ca Fri Feb 15 15:23:16 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 15 Feb 2008 15:23:16 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JQ63Z-0003qF-JD
for categories-list@mta.ca; Fri, 15 Feb 2008 15:17:09 -0400
Date: Fri, 15 Feb 2008 18:25:19 +0000
From: "Jamie Vicary"
To: categories@mta.ca
Subject: categories: Finite limits in a category of free modules over a semiring
MIME-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Content-Disposition: inline
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 36
Dear category theorists,
Given a commutative semiring R, construct the category that has
nonnegative integers as objects, and matrices with entries in R as
morphisms, such that the hom-set from N to M consists of matrices with M
rows and N columns. This is then just the category of finitely-generated
free R-modules. It admits a symmetric monoidal structure given by tensor
product of modules, and has finite biproducts, with the induced
CMon-enrichment agreeing with addition in R. Is there a nice way to
characterise the semirings R for which this category has binary equalisers,
and hence all finite limits?
Note that the category is equal to its opposite, identifying each matrix
with its transpose, and so it will have finite colimits iff it has finite
limits. Also, we assume that our semiring has a 0 and a 1, is distributive,
and that x.0=0.x=0 for all x in R.
Jamie.
PS: There was a interesting discussion of this towards the end of this page:
http://golem.ph.utexas.edu/category/2007/11/geometric_representation_theor_13.html
From rrosebru@mta.ca Fri Feb 15 21:24:51 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 15 Feb 2008 21:24:51 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JQBer-00034b-Ja
for categories-list@mta.ca; Fri, 15 Feb 2008 21:16:01 -0400
Date: Sat, 16 Feb 2008 01:17:24 +0100
From: Andrej Bauer
MIME-Version: 1.0
To: categories@mta.ca
Subject: categories: Re: A small cartesian closed concrete category
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 37
PETER EASTHOPE wrote:
> Is there a cartesian closed concrete category which
> is small enough to write out explicitly? It would be
> helpful in learning about map objects, exponentiation,
> distributivity and etc. Can such a category be made
> with binary numbers for instance?
A Heyting algebra, viewed as a category (every poset is a category), is
a CCC. If you take a small Heyting algebra, e.g. the topology of a
finite topological space, you can write it out explicitly.
If you would like a CCC made from n-bit binary numbers, here is how you
can do it:
The two-point lattice B = {0, 1} is a Boolean algebra with the usual
logical connectives as the operations. Because B is a poset with 0<=1,
it is also a category (with two objects 0, 1 and a morphism between
them). Since every Boolean algebra is a Heyting algebra, B is cartesian
closed, with the following structure:
- 1 is the terminal object
- the product X x Y is the conjuction X & Y
- the exponential Y^X is the implicatoin X => Y
The product of n copies of B is the same thing as n-tuples of bits,
i.e., the n-bit numbers. This is again a CCC (with coordinate-wise
structure).
At this late hour I cannot see what can be said about finite CCC's which
are not (eqivalent to) posets.
Andrej
From rrosebru@mta.ca Sat Feb 16 10:19:51 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sat, 16 Feb 2008 10:19:51 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JQNhT-0004PF-5l
for categories-list@mta.ca; Sat, 16 Feb 2008 10:07:31 -0400
To: categories@mta.ca
From: Thorsten Altenkirch
Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes
Content-Transfer-Encoding: 7bit
Subject: categories: Re: A small cartesian closed concrete category
Date: Sat, 16 Feb 2008 12:21:01 +0000
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 38
On 16 Feb 2008, at 00:17, Andrej Bauer wrote:
> PETER EASTHOPE wrote:
>> Is there a cartesian closed concrete category which
>> is small enough to write out explicitly? It would be
>> helpful in learning about map objects, exponentiation,
>> distributivity and etc. Can such a category be made
>> with binary numbers for instance?
>
> A Heyting algebra, viewed as a category (every poset is a category),
> is
> a CCC. If you take a small Heyting algebra, e.g. the topology of a
> finite topological space, you can write it out explicitly.
>
> If you would like a CCC made from n-bit binary numbers, here is how
> you
> can do it:
>
> The two-point lattice B = {0, 1} is a Boolean algebra with the usual
> logical connectives as the operations. Because B is a poset with 0<=1,
> it is also a category (with two objects 0, 1 and a morphism between
> them). Since every Boolean algebra is a Heyting algebra, B is
> cartesian
> closed, with the following structure:
> - 1 is the terminal object
> - the product X x Y is the conjuction X & Y
> - the exponential Y^X is the implicatoin X => Y
>
> The product of n copies of B is the same thing as n-tuples of bits,
> i.e., the n-bit numbers. This is again a CCC (with coordinate-wise
> structure).
>
> At this late hour I cannot see what can be said about finite CCC's
> which
> are not (eqivalent to) posets.
Indeed, are there any at all? If you have coproducts you can define
the infinite collection of objectss 0,1,2,... and if you identify any
of those you get equational inconsistency. A similar construction
should also work for CCCs. In the simply typed lambda calculus with
one base type o you can iterpret n as o^n -> o and you get equational
inconsistency if you identify any two finite types. This carries over
to a finite collection of base types, and hence there cannot be a
finite CCC which isn't a preorder. I am sure there must be a more
elegant proof of this.
Cheers,
Thorsten
From rrosebru@mta.ca Sat Feb 16 10:19:51 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sat, 16 Feb 2008 10:19:51 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JQNg9-0004Jn-W7
for categories-list@mta.ca; Sat, 16 Feb 2008 10:06:10 -0400
From: Colin McLarty
To: categories@mta.ca
Date: Fri, 15 Feb 2008 20:51:48 -0500
MIME-Version: 1.0
Subject: categories: Re: A small cartesian closed concrete category
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 39
Every finite category with binary products is a preorder: any two
objects A,B have at most one arrow A-->B. Otherwise the successive
powers of B would have unboundedly many arrows from A.
This is Peter Freyd's proof that small complete categories are
preorders. Andrei would have thought of it at a more reasonable hour.
Colin
From rrosebru@mta.ca Sun Feb 17 15:48:36 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 17 Feb 2008 15:48:36 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JQpIe-0001F3-Pp
for categories-list@mta.ca; Sun, 17 Feb 2008 15:35:44 -0400
Date: Sat, 16 Feb 2008 20:55:45 -0500
From: "Fred E.J. Linton"
To:
Subject: categories: Re: Finite limits in a category of free modules over a semiring
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 40
Greetings. On Fri, 15 Feb 2008 02:30:45 PM EST,
"Jamie Vicary" wrote:
> Given a commutative semiring R, construct the category that has
> nonnegative integers as objects, and matrices with entries in R as
> morphisms, such that the hom-set from N to M consists of matrices with =
M
> rows and N columns. This is then just the category of finitely-generate=
d
> free R-modules. It admits a symmetric monoidal structure given by tenso=
r
> product of modules, and has finite biproducts, with the induced
> CMon-enrichment agreeing with addition in R. Is there a nice way to
> characterise the semirings R for which this category has binary equalis=
ers,
> and hence all finite limits?
> =
> Note that the category is equal to its opposite, identifying each
matrix
> with its transpose, and so it will have finite colimits iff it has fini=
te
> limits. ...
While I offer no answer, I will point out that coequalizers here =
(and, by the same token, equalizers) need not look like what you
might expect. For example, when the commutative semiring R is the
ordinary ring of integers, so that the category of R-matrices "is" =
the full category of f.-g. free abelian groups, the coequalizer of
the pair of 1x1 matrices (2): 1 --> 1 and (0): 1 --> 1 exists and
is !: 1-->0 , with the "expected" coequalizer value of Z/2Z being =
"unavailable here."
So: beware! Cheers, -- Fred
From rrosebru@mta.ca Mon Feb 18 11:16:19 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 18 Feb 2008 11:16:19 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JR7az-0005H5-EB
for categories-list@mta.ca; Mon, 18 Feb 2008 11:07:53 -0400
From: Martin Escardo
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
Date: Mon, 18 Feb 2008 00:17:02 +0000
To: categories@mta.ca
Subject: categories: a monad
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 41
Have you come across the following strong monad?
Until I learn that it already has a name, I'll temporarily call it the
selection monad, and denote it by S = (S,mu,eta).
It is defined on an arbitrary cartesian closed category C after
choosing an object V of C. Probably a monoidal closed category will
do, but I haven't paused to consider this.
On objects, define SX = X^(V^X) = ((X -> V) -> X). (One can
contravariantly change the value object V, but I won't consider this
in this message.)
Think of elements of V^X as V-valued predicates, ranged over by p, and
of elements of SX as selection functionals, ranged over by epsilon
(like Hilbert's epsilon operator). Intuition: epsilon(p) picks an
element x of X (perhaps among elements of a subset A of X) such that
p(x) holds, if such an element exists.
On morphisms f : X -> Y, define Sf: SX -> SY, using the
lambda-calculus, with "\" as the notation for "lambda", and "o" for
composition:
Sf : SX -> SY
epsilon |-> \p.f(epsilon(p o f))
This is easily seen to be functorial. Intuition: if epsilon selects
elements among a subset A of X, then Sf(epsilon) selects elements
among the set f(A). To do that, we first find an element x in A such
that p(f(x)) holds, and then apply f to it.
For the unit, take
eta :: X -> SX
x |-> \p.x
Intuition: epsilon = eta(x) selects elements in the singleton set {x},
no matter which predicate p is given.
For multiplication, take
mu : S(S X) -> S X
E |-> \p. E(\epsilon. p(epsilon p)) p
Intuition: Given a selection operator E of selection operators, and
given a predicate p, we select a selection operator epsilon, among the
ones that E can select, such that epsilon selects an element x =
epsilon(p) with p(x), and then apply such a selection operator to p to
finally get such an element x.
The unit and associativity laws are easily (but a bit laboriously)
verified.
This monad is strong, with strength t = t_{X,Y} defined by
t : X x SY -> S(X x Y)
(x, epsilon) |-> \p.(x, epsilon(\y.p(x,y)))
Intuition: if epsilon selects elements among a subset B of Y,
then t(x,epsilon) selects elements among the set {x} x B.
This of course, using the monad structure and cartesian closedness,
extends to a map
times : SX x SY -> S(X x Y)
Intuition: if epsilon_X and epsilon_Y select elements among sets A and
B, then times(epsilon_X,epsilon_Y) selects among elements of A x B.
(I don't think the strength is commutative.)
Of course, one is familiar with the "continuation" monad QX=V^(V^X).
There is a monad morphism
SX -> QX
epsilon |-> \p. p(epsilon p)
My question is: have you come across the strong monad S (and its
relationship to the monad Q)? Of course, S has many interesting
submonads for particular choices of V, which correspond to submonads
of Q that have been considered.
I carry on a bit further.
Suppose our category C has a nno N=(N,s,0), and write x+1=sx.
Then we can define a natural isomorphism cons = cons_X
cons : X x X^N <---> X^N : (head,tail)
with head(alpha)=alpha(0) and tail(alpha)(n)=alpha(n+1). Then, as is
well known, the map (head,tail) is a final coalgebra for the functor
(-) -> X x (-).
I want to consider the composite mul = (S cons) o times,
mul : SX x S(X^N) -> S(X^N)
For a sequence alpha = epsilon_0, epsilon_1, epsilon_2 ... of epsilon
operators in SX, we may attempt to define the infinitely iterated
product
mul(epsilon_0, mul(epsilon_1, mul(epsilon_2, ...) ... ))
It turns out that, in particular categories of interest, with a
suitable choice of V, this exists. Moreover, there is a unique
functional that picks the product selection operator, given the
selection operators for the components:
prod : (SX)^N -> S(X^N)
prod(cons(epsilon,alpha)) = mul(epsilon, prod alpha)
or, equivalently,
prod o cons = mul o (id x prod)
and so this is a kind of algebra homomorphism. The odd thing is that
cons is the inverse of the final coalgebra, and, for this particular
situation, it is instead playing the role of an initial algebra with
respect to mul. (Of course, we are all familiar with odd situations
of this kind.)
There is no reason why such a unique morphism prod should exist in an
arbitrary ccc with a chosen V, and counter-examples are readily
obtained.
My original example of prod was constructed before I realized there
was a monad behind it, and was given by a construction that now can be
considered to be rather ad hoc, but that is readily seen to be
equivalent to the above formulation. So this message is a sort of
apology for overlooking obvious considerations.
The example was given in a ccc of computable higher-type functionals
(defined on continuous functionals), with V the booleans, and, the
point, was indeed, that prod is well defined and computable. I had
considered another (more efficient) product functional, based on
(seeing sequences as) binary trees. This also is explained, in very
much the same (and obvious) way, by the above considerations, but I
won't spell it down in this message, which is already long.
To compare it with the ad hoc algorithms, I have coded the above
categorical definitions in the higher-type programming language
Haskell, including the definition of prod derived from them, for both
sequences and trees. The performance in particular examples is the
same as that of the ad hoc previously given algorithms, apart from a
constant factor of approximately 1/2.
I could, in principle, have started from the categorical ideas of this
message and then derived the algorithms. I wish I had done that. In
any case, here are the algorithms as they are derived in this message
(including the tree-like product functional):
http://www.cs.bham.ac.uk/~mhe/papers/selection-monad.hs
MHE.
From rrosebru@mta.ca Tue Feb 19 16:44:31 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Tue, 19 Feb 2008 16:44:31 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JRZ4j-000055-TQ
for categories-list@mta.ca; Tue, 19 Feb 2008 16:28:25 -0400
From: Michael Mislove
To: mfpsmail@lax.math.tulane.edu, categories@mta.ca
Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes
Content-Transfer-Encoding: 7bit
Mime-Version: 1.0 (Apple Message framework v919.2)
Subject: categories: Clifford Lectures 2008
Date: Tue, 19 Feb 2008 11:23:55 -0600
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 42
Dear Colleagues,
This is an invitation to attend the 2008 Clifford Lectures, which
will be held at Tulane from March 12 through March 15, 2008. The
Clifford Lectures are annual series of lectures hosted by the Tulane
Math Department in honoring of A. H. Clifford, noted algebraist, who
was a long time member of the department. This year's Clifford
Lecturer is Samson Abramsky, and the topic of his lectures is,
"Information flow in physics, geometry, logic and computation". Samson
will deliver five lectures on this topic during the course of the
series. In addition, thirteen researchers are also giving one-hour
lectures on this topic as part of the series. You can find details
about the speakers, the titles and abstracts of their talks, the
program and registration information at the page http://www.math.tulane.edu/~mwm/clifford
Best regards,
Mike Mislove
===============================================
Professor Michael Mislove Phone: +1 504 862-3441
Department of Mathematics FAX: +1 504 865-5063
Tulane University URL: http://www.math.tulane.edu/~mwm
New Orleans, LA 70118 USA
===============================================
From rrosebru@mta.ca Tue Feb 19 16:44:31 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Tue, 19 Feb 2008 16:44:31 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JRZ3u-0007m7-Md
for categories-list@mta.ca; Tue, 19 Feb 2008 16:27:34 -0400
Date: Tue, 19 Feb 2008 17:58:14 +0200 (EET)
Subject: categories: pssl87 - final announcement
From: "Panagis Karazeris"
To: categories@mta.ca
MIME-Version: 1.0
Content-Type: text/plain;charset=iso-8859-7
Content-Transfer-Encoding: quoted-printable
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 43
Peripatetic Seminar on Sheaves and Logic 87
Honouring the 70th birthday of Anders Kock
Patras, 21-23 March 2008
The 87th Peripatetic Seminar on Sheaves and Logic will be held in Patras,
Greece, on 22-23 March 2008.
An extra session will be held in the afternoon of Friday 21 March,
celebrating the 70th birthday of Anders Kock.
A. Joyal, F. W. Lawvere and G. Reyes will participate honouring Anders.
Accommodation Information:
The University of Patras is located in the suburbs, 10 km NE of the
downtown area.
The participants have the options of either staying downtown or in one
of the hotels along the coast near the University.
In the first case they will have to use local transportation (bus or taxi=
).
In the second case they may choose to walk
(weather permitting) or get a ride by the people involved in the
organization. With the second option in mind, a number of rooms has been
reserved at Hotel Achaia Beach and will be available at the price of 69
Euros (single room) and 85 Euros (double room), provided that reservatio=
n
is confirmed before 15 January 2008.
The hotel is 2,5 km away from the PSSL venue and has the extra advantage
of being close to some fine restaurants and in walking distance from the
cafes, bars and restaurants of the coast of Rion, which starts getting
lively at that time of the year. A small number of rooms will be availabl=
e
until Friday 22 February 2008.
If you wish to book a hotel room yourself you may consult
http://www.tripadvisor.com/Hotels-g189488-Patras_Peloponnese-Hotels.html
Registration: You may register for PSSL87 by filling out the following fo=
rm
REGISTRATION FORM
Name: .......
Affiliation: .....
I wish to give a talk: YES/NO
Title: .....
Arrival Date: ....
Departure Date: ....
I wish to book a hotel room in Achaia Beach Hotel: YES/NO - SINGLE/DOUBLE
and submitting it to
pssl87@math.upatras.gr
Transportation Information:
Patras is located 220km W of the Athens airport. The best way to approach
it is to use the Athens Suburban Railway (Proastiakos) which stretches
west up to the town of Kiato, on the northern coast of the Peloponnese,
110km away from Patras. The idea is to arrange some private car or coach
rides from Kiato to Patras, according to the date and time of arrival of
most of you. Otherwise there is the option of getting on the (slow, narro=
w
gauge) train to Patras.
Further details as well as a list of participants appear in the
meeting's webpage
http://www.math.upatras.gr/~pssl87/
From rrosebru@mta.ca Wed Feb 20 17:23:05 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 20 Feb 2008 17:23:05 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JRwAd-0006Ci-B3
for categories-list@mta.ca; Wed, 20 Feb 2008 17:08:03 -0400
Date: Wed, 20 Feb 2008 19:41:43 +0100 (CET)
Subject: categories: position at Utrecht
From: moerdijk@math.uu.nl
To: categories@mta.ca
MIME-Version: 1.0
Content-Type: text/plain;charset=iso-8859-1
Content-Transfer-Encoding: quoted-printable
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 44
Dear colleagues,
I'd like to draw your attention to an opening for a tenure (track)
position at Utrecht, at the level of "universitair docent" (comparable
to Lecturer in the UK, Assistant Professor in the US or Maitre de
Conferences in France). The position is related to a large group grant
in the area between (and including) geometry/topology and mathematical
physics, which I'm sure will fit the interests of many readers of this
list.
For more information, see http://www.math.uu.nl/Main/Department/Positions=
/
It is vacancy #62800 on the list of four.
With best regards,
Ieke Moerdijk.
--=20
From rrosebru@mta.ca Sat Feb 23 11:14:26 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sat, 23 Feb 2008 11:14:26 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JSvsk-0002Gq-3O
for categories-list@mta.ca; Sat, 23 Feb 2008 11:01:42 -0400
Subject: categories: FM'08 -- CALL FOR PARTICIPATION
To: events@fmeurope.org
MIME-Version: 1.0
Content-Type: text/plain;charset=iso-8859-1
From: events-admin@fmeurope.org
Date: Fri, 22 Feb 2008 16:15:39 +0100 (CET)
Content-Transfer-Encoding: quoted-printable
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 45
*** Apologies if you receive multiple copies. ***
FM'08: 15TH INTERNATIONAL SYMPOSIUM ON FORMAL METHODS
May 26 - 30, 2008
=C5bo Akademi University
Turku, Finland
CALL FOR PARTICIPATION
http://www.fm2008.abo.fi/
It is our pleasure to invite you to FM'08, the premier international foru=
m
for practitioners and researchers applying mathematical methods to the
design of highly reliable computer systems.
FM'08 is the fifteenth in a series of symposia organized by Formal Method=
s
Europe, http://www.fmeurope.org, an independent association whose aim is
to stimulate the use of, and research on, formal methods for software
development. The symposia have been notably successful in bringing
together innovators and practitioners in precise mathematical methods for
software development, industrial users as well as researchers.
A program of five invited talks and 23 outstanding research papers
provides the opportunity to learn about the newest developments in the
theory and application of formal methods. The program covers a wide range
of topics, including real-time and concurrency, design, verification,
communication, runtime monitoring and analysis, constraint analysis,
programming language analysis, formal methods practice, and grand
challenge problems. As in the previous years, an Industry Day is dedicate=
d
for practitioners to share their experiences with industrial applications=
.
This year's Industry Day investigates telecommunications and embedded
systems, being supported by NOKIA. Speakers from five major industries
will address this year's theme, together with the Johnson Professor Arvin=
d
from MIT.
Tutorials are a central part of this year=92s FM symposium, as an effecti=
ve
way of disseminating emerging application areas, tools, and techniques.
This year we have seven tutorials, given by renowned experts in their
fields. The five co-located workshops address issues of specific formal
techniques as well as novel computational models and grand challenges. Th=
e
following list of tutorials and workshops are available:
Tutorials
=B7 Computational Systems Biology
=B7 Teaching formal methods to students in high school and
introductory university courses
=B7 Event-B and the Rodin Platform
=B7 Why formal verification remains on the fringes of commercial
development
=B7 Formal Methods and Signal Processing
=B7 Runtime Model Checking of Multithreaded C Programs using
Automated Instrumentation Dynamic Partial Order Reduction and Distributed
Checking
=B7 Formal modelling and analysis of real-time systems using UPPA=
AL
Workshops
=B7 Formal aspects of virtual organisations
=B7 Overture/VDM++
=B7 Refinement workshop
=B7 Pilot Projects for the Grand Challenge in Verified Software
=B7 Computational Models for Cell Processes
A Doctoral Symposium on all aspects of formal methods research is also
part of FM=9208, giving young researchers the opportunity to have their
ideas critically, but constructively examined by the community. A Poster
and Tool Exhibition of both research projects and commercial tools allows
researchers to engage in a dialogue with potential users in early phases
of their work. The submission date for the both the Doctoral Symposium an=
d
the Poster and Tool Exhibition is March 7.
Registration to all types of events will open during week 8, with the
possibility of early registration until March 25. Important dates for
submitting papers to the workshops should be identified via the own
homepages of these events, reachable from above or from the FM=9208 websi=
te.
Generally, workshop papers should be submitted in March. The list of the
accepted papers to the technical symposium and the preliminary schedule o=
f
FM=9208 can already be retrieved via our website.
We hope you will enjoy a rewarding symposium program!
Kaisa Sere, General Chair
Jorge Cuellar, Tom Maibaum, Program Chairs
_______________________________________________
events mailing list
events@fmeurope.org
http://www.fmeurope.org/mailman/listinfo/events
From rrosebru@mta.ca Sat Feb 23 11:14:26 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sat, 23 Feb 2008 11:14:26 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JSvrP-0002By-7T
for categories-list@mta.ca; Sat, 23 Feb 2008 11:00:19 -0400
From: Michael Mislove
To: mfpsmail@linus.math.tulane.edu, categories@mta.ca
Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes
Content-Transfer-Encoding: 7bit
Mime-Version: 1.0 (Apple Message framework v919.2)
Subject: categories: MFPS Final Call for Papers
Date: Fri, 22 Feb 2008 08:25:38 -0600
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 46
Dear Colleagues,
This is the Final Call for Papers for MFPS 24. Details about the
meeting are given below. Submissions should be made to EasyChair at
the link http://www.easychair.org/conferences/?conf=mfps24 The
deadline for submissions of titles and brief abstracts is Friday,
March 7, and the deadline for full submissions is the following
Friday, March 14.
Thanks, and best regards,
Mike Mislove
===============================================
Professor Michael Mislove Phone: +1 504 862-3441
Department of Mathematics FAX: +1 504 865-5063
Tulane University URL: http://www.math.tulane.edu/~mwm
New Orleans, LA 70118 USA
===============================================
CALL FOR PAPERS
MFPS XXIV
http://www.math.tulane.edu/~mfps/mfps24.htm
Twenty-fourth Conference on the
Mathematical Foundations of
Programming Semantics
University of Pennsylvania
Philadelphia, PA USA
May 22 - 25, 2008
Partially Supported by US Office of Naval Research
The MFPS conferences are devoted to those areas of mathematics, logic,
and computer science which are related to models of computation, in
general, and to the semantics of programming languages, in particular.
The series has particularly stressed providing a forum where
researchers in mathematics and computer science can meet and exchange
ideas about problems of common interest. As the series also strives to
maintain breadth in its scope, the conference strongly encourages
participation by researchers in neighboring areas.
TOPICS include, but are not limited to, the following: biocomputation;
categorical models; concurrent and distributed computation;
constructive mathematics; domain theory; formal languages; formal
methods; game semantics; lambda calculus; logic; non-classical
computation; probabilistic systems; process calculi; program analysis;
programming-language theory; quantum computation; rewriting theory;
security; specifications; topological models; type systems; type
theory.
The Twenty-fourth Conference on the Mathematical Foundations of
Programming Semantics (MFPS XXIV) will take place on the campus of
University of Pennsylvania, Philadelphia, PA USA from Thursday, May 22
through Sunday, May 25, 2008.
The Organising Committee for MFPS consists of Stephen Brookes (CMU),
Achim Jung (Birmingham), Catherine Meadows (NRL), Michael Mislove
(Tulane), and Prakash Panangaden (McGill). The local arrangements for
MFPS XXIV are being overseen by Andre Scedrov (Penn).
The INVITED SPEAKERS for MFPS XXIV are
Samson Abramsky, Oxford
Luca Cardelli, Microsoft Research, Cambridge
Dusko Pavlovic, Kestrel Institute
Benjamin Pierce, Penn
Phil Scott, Ottawa
James Worrell, Oxford
In addition, there will be four special sessions:
- A session honoring Phil Scott on the occasion of his 60th birthday
year, which is being organized by Rick Blute (Ottawa) and Andre
Scedrov (Penn).
- A session on Systems Biology will be held in conjunction with Luca
Cardelli's plenaary talk. It is being organized by Jean Krivine (LIX).
- A third session will be devoted to Type Theory. It is being
organized by Benjamin Pierce and by Robert Harper (CMU) will be held
in conjunction with Benjamin Pierce's plenary talk.
- The fourth special session will be on Security, and will be
organized by Catherine Meadows (NRL) in conjunction with Dusko
Pavlovic's plenary talk.
Further, there will be a TUTORIAL DAY on May 21. The topic will be
Category Theory and Its Applications to Theoretical Computer Science.
It is being organized by Phil Scott (Ottawa); the speakers will be
announced at a later date. This event will be free to all those who
are interested in attending.
The remainder of the program will consist of papers selected by the
following PROGRAM COMMITTEE
Andrej Bauer (Ljubljana), CHAIR
Ulrich Berger (Swansea)
Lars Birkedal (Copenhagen)
Jens Blanck (Swansea)
Steve Brookes (CMU)
Bob Coecke (Oxford)
Karl Crary (CMU)
Martin Escardo (Birmingham)
Achim Jung (Birmingham)
Jean Krivine (LIX)
James Laird (Sussex)
Paul Levy (Birmingham)
Catherine Meadows (NRL)
Michael Mislove (Tulane)
Catuscia Palamidessi (INRIA)
Prakash Panangaden (McGill)
Alex Simpson (Edinburgh)
Christopher Stone (Harvey Mudd)
Thomas Streicher (Darmstadt)
James Worrell (Oxford)
from submissions received in response to this Call for Papers.
Submissions Now Open!
Authors can submit papers in response to this Call for Papers by
pointing their browser to
http://www.easychair.org/conferences/?conf=mfps24
The submission process requires registering as an author and
submitting the title and a short abstract for your paper by March 7,
2008. The deadline for submissions of full papers is one week later,
March 14, 2008. The other important dates are listed below.
Papers should be no more than 15 pages in LaTeX, and should be in the
form of either a PostScript file or a pdf file suitable for printing
on a generic printer. The accepted papers will appear in ENTCS, and
the required format for ENTCS can be used for submissions. The generic
ENTCS macro package can be found at this web site. There is no special
entcsmacro.sty file for this year's MFPS Proceedings as yet; authors
who use the ENTCS macros should just use the file that comes in the
generic package.
IMPORTANT DATES:
* Fri Mar 7: Paper registration deadline, with short abstracts.
* Fri Mar 14: Paper submission deadline.
* Fri Apr 7: Author notification.
* Fri Apr 21: Final versions for the proceedings.
From rrosebru@mta.ca Mon Feb 25 09:57:01 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 25 Feb 2008 09:57:01 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JTdbf-00038q-K6
for categories-list@mta.ca; Mon, 25 Feb 2008 09:42:59 -0400
Content-class: urn:content-classes:message
MIME-Version: 1.0
Subject: categories: REACHABILITY PROBLEMS (RP'08) Liverpool, 15-17 September 2008
Date: Sun, 24 Feb 2008 10:38:54 -0000
From: "Potapov, Igor"
To:
Content-Type: text/plain; charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 47
=20
2nd WORKSHOP ON REACHABILITY PROBLEMS, RP'08
(September 15-17, 2008, Liverpool, UK)
Deadline for submissions: 19 May, 2008
http://www.csc.liv.ac.uk/~rp2008/
=20
The Workshop on Reachability Problems will take place at=20
the University of Liverpool, Liverpool, UK on September=20
15-17, 2008. Papers presenting original contributions=20
related to reachability problems in different=20
computational models and systems are being sought.=20
The Reachability Workshop is specifically aimed at gathering=20
together scholars from diverse disciplines and backgrounds=20
interested in reachability problems that appear in
- Algebraic structures
- Computational models
- Hybrid systems
- Verification
=20
Invited Speakers:
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
- Ahmed Bouajjani, Paris, France=20
- Juhani Karhumaki, Turku, Finland=20
- Colin Stirling, Edinburgh, UK=20
- Wolfgang Thomas, Aachen, Germany=20
=20
Submissions:
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=20
Papers presenting original contributions related to=20
reachability problems in different computational models=20
and systems are being sought.=20
Topics of interest include (but are not limited to):=20
Reachability probelms in infinite state systems,=20
rewriting systems, dynamical and hybrid systems;=20
reachability problems in logic and verification;=20
reachability analysis in different computational=20
models, counter/ timed/ cellular/ communicating=20
automata; Petri-Nets; computational aspects of=20
algebraic structures (semigroups, groups and rings);=20
predictability in iterative maps and new=20
computational paradigms.=20
=20
Authors are invited to submit a draft of a full paper with=20
at most 12 pages (in standard LaTeX article style 11pt A4 paper)=20
via the conference web page http://www.csc.liv.ac.uk/~rp2008/ .=20
Proofs omitted due to space constraints must be put into an appendix=20
to be read by the program committee members at their
discretion. Submissions deviating from these guidelines risk=20
rejection. Electronic submissions should be formatted in=20
postscript or pdf. Simultaneous submission to other conferences=20
or workshops with published proceedings is not allowed.
=20
Important dates:
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
Submission deadline : May 19, 2008=20
Notification to authors: June 30, 2008=20
Final version: July 15, 2008=20
Workshop: September 15-17, 2008=20
=20
The proceedings of the workshop will appear in=20
Electronic Notes in Theoretical Computer Science (ENTCS).=20
ENTCS is published electronically on Science Direct,=20
Elsevier's main platform for electronic publication to=20
provide rapid publication and broad dissemination of the=20
volumes in the series. Selected papers will appear in a=20
special issue of a high quality journal.=20
=20
Program Committee:
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
- Parosh Aziz Abdulla , Uppsala=20
- Eugene Asarin , Paris=20
- Vincent Blondel, Louvain=20
- Olivier Bournez, Nancy=20
- Cristian S. Calude , Auckland=20
- Javier Esparza , Munchen=20
- Vesa Halava , Turku=20
- Oscar Ibarra , Santa Barbara=20
- Juhani Karhumaki, Turku=20
- Igor Potapov , Liverpool=20
- Colin Stirling, Edinburgh=20
- Wolfgang Thomas , Aachen=20
- Hsu-Chun Yen , Taipei=20
=20
Organizing Committee:
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
- Igor Potapov, Liverpool
- Vesa Halava, Turku
=20
Contact:=20
=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D
RP'08,=20
Department of Computer Science,
University of Liverpool,=20
Ashton Building,
Ashton Street,=20
Liverpool, L69 3BX
E-mail: rp2008 [at] csc.liv.ac.uk=20
Web: http://www.csc.liv.ac.uk/~rp2008/
From rrosebru@mta.ca Mon Feb 25 17:27:36 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 25 Feb 2008 17:27:36 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JTkku-0003C0-DC
for categories-list@mta.ca; Mon, 25 Feb 2008 17:21:00 -0400
Mime-Version: 1.0 (Apple Message framework v753)
Content-Type: text/plain; charset=US-ASCII; format=flowed
To: categories@mta.ca
Content-Transfer-Encoding: 7bit
From: Matthew Hennessy
Subject: categories: Postdoctoral Fellowhships
Date: Mon, 25 Feb 2008 14:42:37 +0000
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 48
Apologies for Multiple Postings
---------------------------------------------------
The Foundations of Global Computing - Trinity College Dublin
Two postdoctoral Research Fellowships
Applications are invited for TWO post-doctoral positions to
undertake research into the foundations of Global Computing. The
posts are within the Software Systems Lab of the Department of
Computer Science at Trinity College Dublin as part of a new SFI-funded
research project, under the direction of Matthew Hennessy, which seeks
to establish a firm mathematical and logical basis for the next
generation of widely distributed computing computing environments.
Applicants should have a PhD in Computer Science, or a closely related
discipline. Candidates with expertise in following areas are
particularly welcome:
- operational semantics
- concurrency theory
- model checking
- verification techniques
- type theory
- program logics
These posts are tenable from April 2008 at a salary commensurate with
the successful candidates' qualifications and experience. Appointments
will be made initially for a 24 month period, although there will be
scope for extension. Further particulars of the posts may be obtained
from the address below, and informal enquiries are also welcomed.
Applications should include
- detailed curriculum vitae, in pdf format
- copies of relevant publications, or url-pointers to them
- the names of two referees
- a statement outlining the applicant's suitability to the project.
Applications should be sent to:
Matthew Hennessy
Department of Computer Science
The O'Reilly Institute
Trinity College
Dublin 2
Ireland
email: matthew.hennessy@cs.tcd.ie
tel: +353 (01) 8962634
Trinity College is an equal opportunities employer.
From rrosebru@mta.ca Mon Feb 25 17:27:37 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Mon, 25 Feb 2008 17:27:37 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JTkm8-0003K1-DG
for categories-list@mta.ca; Mon, 25 Feb 2008 17:22:16 -0400
Date: Mon, 25 Feb 2008 14:21:25 -0500
From: Nath Rao
MIME-Version: 1.0
To: categories@mta.ca
Subject: categories: Language of an internal category?
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 49
Is there a version of Mitchell-Benabou language for internal categories
in toposes (with natural number objects)? What I have in mind is
something that will allow automatic translations of definitions and
proofs to internal categories that gives the expected results for
established notions. [I have glanced through "Relative set theories",
and the relevant chapters of Jacobs, "Categorical logic and type
theory"; they do not seem to what I am looking for, in the sense that
the primary focus is not on the properties of the internal category.]
Thanks in advance
Nath Rao
From rrosebru@mta.ca Tue Feb 26 15:36:29 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Tue, 26 Feb 2008 15:36:29 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JU5Pe-0005BA-Ud
for categories-list@mta.ca; Tue, 26 Feb 2008 15:24:26 -0400
Mime-Version: 1.0 (Apple Message framework v752.3)
Content-Transfer-Encoding: quoted-printable
Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed
To: types-list@lists.seas.upenn.edu, categories@mta.ca
From: Russ Harmer
Subject: categories: GALOP@ETAPS'08: Call for participation
Date: Tue, 26 Feb 2008 12:12:12 +0100
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 50
This is a Call for Participation to the
3rd International Workshop on Games for Logic and Programming =20=
Languages (GALOP3)
to be held at ETAPS, on 5--6 April 2008, in Budapest.
Invited speakers are:
# Gabriel Sandu (University of Helsinki): Independence between =20=
quantifiers
# Merlijn Sevenster (Universiteit van Amsterdam): Independence =20=
between modal operators
# Paul-Andr=E9 Melli=E8s (PPS, CNRS & Paris-Diderot): Game =
semantics as =20
string diagrams
More details about the workshop, including a list of accepted =20
contributions, can be found at:
http://www.cs.bham.ac.uk/~drg/galop.html
To register for the workshop, please use the following link:
http://etaps08.mit.bme.hu/
From rrosebru@mta.ca Wed Feb 27 13:09:23 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 27 Feb 2008 13:09:23 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JUPe6-0003bY-16
for categories-list@mta.ca; Wed, 27 Feb 2008 13:00:42 -0400
Date: Wed, 27 Feb 2008 12:03:53 +0100
From: Clemens Kupke
MIME-Version: 1.0
To: cmcs08@cwi.nl
Subject: categories: CMCS 08: final call for short contributions
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
Content-Transfer-Encoding: 7bit
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 51
----------------------------------------------------------------------
CMCS 08 : FINAL CALL FOR SHORT CONTRIBUTIONS
9th International Workshop on Coalgebraic Methods in Computer Science
http://www.cwi.nl/projects/cmcs08/
Budapest, Hungary
April 4-6, 2008
Key Note Speaker: Dexter Kozen
Invited Speakers: Stefan Milius and Dirk Pattinson
The workshop will be held in conjunction with the 11th European Joint
Conferences on Theory and Practice of Software ETAPS 2008
March 29 - April 6, 2008
Following the tradition of preceding workshops we invite short
contributions that will be collected in a technical
report of the Technical University of Braunschweig. They should be
no more than two pages and may describe work in progress, summarise
work submitted to a conference or workshop elsewhere, or in some
other way appeal to the CMCS audience. They should be submitted in
postscript or pdf form as attachments to an email to
cmcs08@cwi.nl.
Deadline for submission of short contributions: March 10, 2008.
Notification of acceptance of short contributions: March 17, 2008.
Jiri Adamek and Clemens Kupke
PC co-chairs
From rrosebru@mta.ca Wed Feb 27 20:23:08 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Wed, 27 Feb 2008 20:23:08 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JUWRs-0000oe-DN
for categories-list@mta.ca; Wed, 27 Feb 2008 20:16:32 -0400
From: Sam Staton
To: categories@mta.ca
Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes
Content-Transfer-Encoding: 7bit
Mime-Version: 1.0 (Apple Message framework v919.2)
Subject: categories: Mismatch in lcc pretoposes with W-types?
Date: Wed, 27 Feb 2008 19:07:21 +0000
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 52
Various people (including Moerdijk & Palmgren, Hyland & Gambino,
Abbott & Altenkirch & Ghani) have considered locally cartesian closed
pretoposes with W-types, ie initial algebras for generalized
polynomial functors, aka 'containers'. (These W-types are an
appropriate analysis of the fixed points of intensional constructions
and so these categories have been motivated as "constructive toposes",
as models of a particular version of Martin-Lof's type theory).
Lcc pretoposes are Heyting pretoposes. For any object X, consider
those monotone endofunctions on the class Sub(X) that can be
constructed from the pullback functors and their left and right
adjoints. By my calculations, in a topos, these monotone endofunctions
have least and greatest fixed points (by internalizing them and then
using Tarski's fixed point theorem).
It seems that, in general, these monotone endofunctions will not have
least or greatest fixed points in lcc pretoposes with W-types. (I
haven't proved this, though, and perhaps I have missed a neat trick.)
If I'm not mistaken, this is a mismatch. Lcc pretoposes let you work
both intensionally and extensionally, yet when it comes to W-types, we
only consider the intensional constructions. Is there a reason for
this?-- are these fixed points "non-constructive" or "impredicative"
in some sense?
Has anybody thought about these things before? Have I missed
something? All the best, Sam
[My example is bisimilarity for transition systems, as studied in
concurrency theory. This is conventionally calculated as a maximum
fixed point for a monotone endofunction on the lattice of binary
relations. I can define a 'constructive' version of bisimilarity using
W-types, and then take the image. This differs from the usual notion,
unless choice is assumed.]
From rrosebru@mta.ca Thu Feb 28 22:22:05 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 28 Feb 2008 22:22:05 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JUugd-0000z8-Gm
for categories-list@mta.ca; Thu, 28 Feb 2008 22:09:23 -0400
Mime-Version: 1.0 (Apple Message framework v752.3)
Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed
To: categories@mta.ca
Content-Transfer-Encoding: 7bit
From: Neil Ghani
Subject: categories: Re: Mismatch in lcc pretoposes with W-types?
Date: Thu, 28 Feb 2008 15:41:47 +0000
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 53
Hi All,
Since we have a semantic characterisation of containers, we can look
at Thorstens question
> Alternatively for containers: Every endofunctor which has an
> initial algebra is a container. Obviously, this will only hold in
> the syntax of Type Theory, i.e. the classifying predicative
> pretopos with W-types.
Surely, it must be the case that all syntactically definable
endofunctors are accessible.
And, being syntactic constructions, I'd not be too surprised if they
preserved connected limits ...
Unless I've got the wrong end of the stick which is entirely possible.
All the best
Neil
On 28 Feb 2008, at 15:32, Thorsten Altenkirch wrote:
> Hi Sam,
>
> the issue you address has to do with the question of predicative
> vs. impredicative, I think.
>
> As you say in a topos any monotone operator on the lattice of
> subsets of a given type has a least (and greatest fixpoint). In a
> predicative theory like Martin-Loef's Type Theory these fixpoints
> only exist if the monotone operator is defined in a *strictly*
> positive way.
>
> There seems to be no simple example of such a fixpoint because all
> simple examples turn out to be strictly positive. Here is the
> simplest one I can think of in the moment: Let (A,@) be a partial
> combinatory algebra, e.g. the natural number with an encoding of
> Turing machines. Then choose a subset R \subseteq A to define an
> antitone operator F on subsets of A by
>
> F P = { x:A | all y:A.P y -> R (x @ y) }
>
> Now clearly FF (do F twice) is monotone and hence will have a least
> fixpoint in a topos. However, by a proof-theoretic analysis (I
> think) we can show that the fixpoint cannot be constructed in
> Martin-Loef Type Theory. (It would be nicer to have a semantical
> argument).
>
> Btw this is just an encoding of Reynold's construction to show that
> there are no set-theoretic models of System F. In System F you get
> a fixpoint of (X -> 2) -> 2 which corresponds to choosing R to be
> an encoding of 2, e.g.
> R = {\xy.x,\xy.y}.
>
> There is a semantic characterisation of strictly positive operators
> on subsets which is similar to the concept of containers, I have
> used this in joint work with Andreas Abel a while ago (our JFP 2002
> paper and TYPES 99). It would be nice, if one could show that all
> operators which have fixpoints are one of those. Alternatively for
> containers: Every endofunctor which has an initial algebra is a
> container. Obviously, this will only hold in the syntax of Type
> Theory, i.e. the classifying predicative pretopos with W-types.
>
> I am not sure this mismatch is a problem: Do you ever need
> fixpoints of non-strict positive operators?
>
> Cheers,
> Thorsten
>
> On 27 Feb 2008, at 19:07, Sam Staton wrote:
>
>> Various people (including Moerdijk & Palmgren, Hyland & Gambino,
>> Abbott & Altenkirch & Ghani) have considered locally cartesian closed
>> pretoposes with W-types, ie initial algebras for generalized
>> polynomial functors, aka 'containers'. (These W-types are an
>> appropriate analysis of the fixed points of intensional constructions
>> and so these categories have been motivated as "constructive
>> toposes",
>> as models of a particular version of Martin-Lof's type theory).
>>
>> Lcc pretoposes are Heyting pretoposes. For any object X, consider
>> those monotone endofunctions on the class Sub(X) that can be
>> constructed from the pullback functors and their left and right
>> adjoints. By my calculations, in a topos, these monotone
>> endofunctions
>> have least and greatest fixed points (by internalizing them and then
>> using Tarski's fixed point theorem).
>>
>> It seems that, in general, these monotone endofunctions will not have
>> least or greatest fixed points in lcc pretoposes with W-types. (I
>> haven't proved this, though, and perhaps I have missed a neat trick.)
>>
>> If I'm not mistaken, this is a mismatch. Lcc pretoposes let you work
>> both intensionally and extensionally, yet when it comes to W-
>> types, we
>> only consider the intensional constructions. Is there a reason for
>> this?-- are these fixed points "non-constructive" or "impredicative"
>> in some sense?
>>
>> Has anybody thought about these things before? Have I missed
>> something? All the best, Sam
>>
>>
>> [My example is bisimilarity for transition systems, as studied in
>> concurrency theory. This is conventionally calculated as a maximum
>> fixed point for a monotone endofunction on the lattice of binary
>> relations. I can define a 'constructive' version of bisimilarity
>> using
>> W-types, and then take the image. This differs from the usual notion,
>> unless choice is assumed.]
>>
>>
>
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
From rrosebru@mta.ca Thu Feb 28 22:22:05 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Thu, 28 Feb 2008 22:22:05 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JUufJ-0000u8-4s
for categories-list@mta.ca; Thu, 28 Feb 2008 22:08:01 -0400
Mime-Version: 1.0 (Apple Message framework v753)
Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed
To: categories@mta.ca
Content-Transfer-Encoding: 7bit
From: Thorsten Altenkirch
Subject: categories: Re: Mismatch in lcc pretoposes with W-types?
Date: Thu, 28 Feb 2008 15:32:57 +0000
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: O
X-Status:
X-Keywords:
X-UID: 54
Hi Sam,
the issue you address has to do with the question of predicative vs.
impredicative, I think.
As you say in a topos any monotone operator on the lattice of subsets
of a given type has a least (and greatest fixpoint). In a predicative
theory like Martin-Loef's Type Theory these fixpoints only exist if
the monotone operator is defined in a *strictly* positive way.
There seems to be no simple example of such a fixpoint because all
simple examples turn out to be strictly positive. Here is the
simplest one I can think of in the moment: Let (A,@) be a partial
combinatory algebra, e.g. the natural number with an encoding of
Turing machines. Then choose a subset R \subseteq A to define an
antitone operator F on subsets of A by
F P = { x:A | all y:A.P y -> R (x @ y) }
Now clearly FF (do F twice) is monotone and hence will have a least
fixpoint in a topos. However, by a proof-theoretic analysis (I think)
we can show that the fixpoint cannot be constructed in Martin-Loef
Type Theory. (It would be nicer to have a semantical argument).
Btw this is just an encoding of Reynold's construction to show that
there are no set-theoretic models of System F. In System F you get a
fixpoint of (X -> 2) -> 2 which corresponds to choosing R to be an
encoding of 2, e.g.
R = {\xy.x,\xy.y}.
There is a semantic characterisation of strictly positive operators
on subsets which is similar to the concept of containers, I have used
this in joint work with Andreas Abel a while ago (our JFP 2002 paper
and TYPES 99). It would be nice, if one could show that all operators
which have fixpoints are one of those. Alternatively for containers:
Every endofunctor which has an initial algebra is a container.
Obviously, this will only hold in the syntax of Type Theory, i.e. the
classifying predicative pretopos with W-types.
I am not sure this mismatch is a problem: Do you ever need fixpoints
of non-strict positive operators?
Cheers,
Thorsten
On 27 Feb 2008, at 19:07, Sam Staton wrote:
> Various people (including Moerdijk & Palmgren, Hyland & Gambino,
> Abbott & Altenkirch & Ghani) have considered locally cartesian closed
> pretoposes with W-types, ie initial algebras for generalized
> polynomial functors, aka 'containers'. (These W-types are an
> appropriate analysis of the fixed points of intensional constructions
> and so these categories have been motivated as "constructive toposes",
> as models of a particular version of Martin-Lof's type theory).
>
> Lcc pretoposes are Heyting pretoposes. For any object X, consider
> those monotone endofunctions on the class Sub(X) that can be
> constructed from the pullback functors and their left and right
> adjoints. By my calculations, in a topos, these monotone endofunctions
> have least and greatest fixed points (by internalizing them and then
> using Tarski's fixed point theorem).
>
> It seems that, in general, these monotone endofunctions will not have
> least or greatest fixed points in lcc pretoposes with W-types. (I
> haven't proved this, though, and perhaps I have missed a neat trick.)
>
> If I'm not mistaken, this is a mismatch. Lcc pretoposes let you work
> both intensionally and extensionally, yet when it comes to W-types, we
> only consider the intensional constructions. Is there a reason for
> this?-- are these fixed points "non-constructive" or "impredicative"
> in some sense?
>
> Has anybody thought about these things before? Have I missed
> something? All the best, Sam
>
>
> [My example is bisimilarity for transition systems, as studied in
> concurrency theory. This is conventionally calculated as a maximum
> fixed point for a monotone endofunction on the lattice of binary
> relations. I can define a 'constructive' version of bisimilarity using
> W-types, and then take the image. This differs from the usual notion,
> unless choice is assumed.]
>
>
This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.
From rrosebru@mta.ca Fri Feb 29 09:40:35 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 29 Feb 2008 09:40:35 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JV5MN-0006a9-UV
for categories-list@mta.ca; Fri, 29 Feb 2008 09:33:11 -0400
From: "Ronnie"
To:
Subject: categories: preprints available
Date: Fri, 29 Feb 2008 12:12:43 -0000
MIME-Version: 1.0
Content-Type: text/plain;charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 55
The following are available from my preprint page, by me unless stated =
otherwise:=20
http://www.bangor.ac.uk/~mas010/brownpr.html
1) 08.04 Exact sequences of fibrations of crossed complexes, homotopy =
classification of maps, and nonabelian extensions of groups=20
ABSTRACT: The classifying space of a crossed complex generalises the =
construction of Eilenberg-Mac Lane spaces. We show how the theory of =
fibrations of crossed complexes allows the analysis of homotopy classes =
of maps from a free crossed complex to such a classifying space. This =
gives results on the homotopy classification of maps from a CW-complex =
to the classifying space of a crossed module and also, more generally, =
of a crossed complex whose homotopy groups vanish in dimensions between =
1 and n. The results are analogous to those for the obstruction to an =
abstract kernel in group extension theory.=20
2) 06.04 R. Brown, I. Morris, J. Shrimpton and C.D. Wensley=20
Graphs of morphisms of graphs=20
ABSTRACT: This is an account for the combinatorially minded reader of =
various categories of directed and undirected graphs, and their =
analogies with the category of sets. As an application, the =
endomorphisms of a graph are in this context not only composable, giving =
a monoid structure, but also have a notion of adjacency, so that the set =
of endomorphisms is both a monoid and a graph. We extend Shrimpton's =
(unpublished) investigations on the morphism digraphs of reflexive =
digraphs to the undirected case by using an equivalence between a =
category of reflexive, undirected graphs and the category of reflexive, =
directed graphs with reversal. In so doing, we emphasise a picture of =
the elements of an undirected graph, as involving two types of edges =
with a single vertex, namely `bands' and `loops'. Such edges are =
distinguished by the behaviour of morphisms with respect to these =
elements.
3) Possible connections between whiskered categories and groupoids, many =
object Lie algebras, automorphism structures and local-to-global =
questions=20
ABSTRACT: We define the notion of whiskered categories and groupoids and =
discuss potential applications and extensions, for example to a many =
object Lie theory, and to resolutions of monoids. This paper is more an =
outline of a possible programme or programmes than giving conclusive =
results.=20
4) A new higher homotopy groupoid: the fundamental globular =
$\omega$-groupoid of a filtered space=20
MSC Classification:18D10, 18G30, 18G50, 20L05, 55N10, 55N25.
KEY WORDS: filtered space, higher homotopy van Kampen theorem, cubical =
singular complex, free globular groupoid
ABSTRACT: We show that the graded set of filter homotopy classes rel =
vertices of maps from the $n$-globe to a filtered space may be given the =
structure of globular $\omega$--groupoid. The proofs use an analogous =
fundamental cubical $\omega$--groupoid due to the author and Philip =
Higgins. This method also relates the construction to the fundamental =
crossed complex of a filtered space, and this relation allows the proof =
that the crossed complex associated to the free globular =
$\omega$-groupoid on one element of dimension $n$ is the fundamental =
crossed complex of the $n$-globe.=20
Ronnie=20
From rrosebru@mta.ca Fri Feb 29 17:18:57 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Fri, 29 Feb 2008 17:18:57 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JVCW8-0006oa-H2
for categories-list@mta.ca; Fri, 29 Feb 2008 17:11:44 -0400
Date: Wed, 27 Feb 2008 08:11:02 -0500 (EST)
From: Michael Barr
To: Categories list
Subject: categories: Backup TeX editor
MIME-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 56
[Note from moderator: Please cc: any expressions of interest to
tac@mta.ca]
TAC has been in existence now for 13 years. For about the first half of
its existence, Bob did everything to get papers ready for publication. He
did consult with me if he had particular tex problems. About when I
retired, I took on the task of preparing papers (most of them) for
publication. However I am uncomfortable with being the only one who
really understands what is going on with tac.cls. I would like to find a
volunteer to back me up, with a view to eventually taking over when the
times comes, as it must, that I can no longer do the job.
The job is not onerous. We get about 20 papers a year. On average, a
paper takes a couple hours of preparation. Sometimes it is more, but
often there is essentially no prep time since the author has used tac.cls
and made no formatting errors.
I am not planning on stopping this any time soon, but I think it is past
time to prepare for the future.
Michael
From rrosebru@mta.ca Sun Mar 2 12:42:54 2008 -0400
Return-path:
Envelope-to: categories-list@mta.ca
Delivery-date: Sun, 02 Mar 2008 12:42:54 -0400
Received: from Majordom by mailserv.mta.ca with local (Exim 4.61)
(envelope-from )
id 1JVr2C-0002lN-Ve
for categories-list@mta.ca; Sun, 02 Mar 2008 12:27:33 -0400
Mime-Version: 1.0 (Apple Message framework v624)
Content-Type: text/plain; charset=US-ASCII; format=flowed
Content-Transfer-Encoding: 7bit
From: Paul Taylor
Subject: categories: Re: Backup TeX editor
Date: Fri, 29 Feb 2008 22:14:46 +0000
To: Categories list
Sender: cat-dist@mta.ca
Precedence: bulk
Message-Id:
Status: RO
X-Status:
X-Keywords:
X-UID: 57
[Note from moderator: To reiterate: expressions of interest in the backup
TeX editor position for TAC should be sent directly to Michael Barr,
, and not to this mailing list. Thanks for those
already sent. The TAC request that authors submit a single source file has
nothing to do with archiving. Its purpose is to simplify slightly the
editors' work.]
Dear Mike,
In response to your request for volunteers to take over the
TeXnical management of TAC, I would certainly consider taking
part in a committee to undertake this.
I believe that I am qualified for the job. TeX has an error message,
"Interwoven alignment preambles are not allowed", about which the
TeXbook (p299) says, "If you have been so devious as to get this
message, you will know what it means, and you will deserve no
sympathy". I got it in about 1992, developing my diagrams package,
and take it as my qualification to be a "TeXpert".
There is, however, a condition, namely that TAC's use of LaTeX be
brought up to date. In particular, macros should be separated
in a modular fashion from mathematics. You insist on their being
pasted in-line for the dubious reason of trying to archive papers
as single files, whereas anybody else would use a directory (folder).
Since I am making this offer in public, I would like to take the
opportunity to point out to users of my diagrams package that
version 3.91 has expired, and they should get a new one from
www.PaulTaylor.EU/diagrams
Also, even in V 3.91, the option "noPostScript" has been renamed
"UglyObsolete", as a further attempt to get people to stop using
the pre-1992 code that uses LaTeX-style diagonal lines.
Best wishes,
Paul Taylor