From rrosebru@mta.ca Sun Jun 4 12:08:10 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA04357 for categories-list; Sun, 4 Jun 2000 12:04:16 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: gmh@Cs.Nott.AC.UK Message-Id: <200006021351.KAA05476@mailserv.mta.ca> To: categories@mta.ca Subject: categories: Four lectureships in Nottingham Date: Fri, 2 Jun 2000 14:49:50 BST Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: ---------------------------------------------------------------------- THE UNIVERSITY OF NOTTINGHAM School of Computer Science and Information Technology Four lectureships Applications are invited for the above posts in a rapidly expanding School based at one of the UK's strongest research-led universities. The School was graded 4 in the 1996 Research Assessment Exercise and is now building up its research strengths for a further improvement in grade. These posts are part of a steady increase in the size of the School accompanied by a move to new purpose-built accommodation in September 1999. Although the successful candidates will have the opportunity of teaching within their specialist area at undergraduate and postgraduate level, there will also be a requirement to teach general computer science and information technology modules outside of any particular specialisation. Candidates should already have a PhD in computer science, or another closely related discipline, together with strong evidence of existing research work and the potential for future research at Grade 5 level. Outstanding candidates will be welcomed from any area of computer science. Salary will be within the range #17,238 - #30,065 per annum (under review), depending on qualifications and experience. Informal enquiries may be addressed to Professor P H Ford, tel: +44 (0)115 951 4251 or Email: Peter.Ford@Nottingham.ac.uk. Further information about the School is available on the WWW at: http://www.cs.nott.ac.uk. Further details and application forms are available from the Personnel Office, Highfield House, The University of Nottingham, University Park, Nottingham NG7 2RD, United Kingdom. Tel: +44 (0)115 951 5927. Fax: +44 (0)115 951 5205. Email: Carole.Matthews@Nottingham.ac.uk. Please quote ref. LEG/510. Closing date: 23rd June 2000. ---------------------------------------------------------------------- From rrosebru@mta.ca Sun Jun 4 12:08:11 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA08954 for categories-list; Sun, 4 Jun 2000 12:02:55 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3937F140.1C337FB@dcs.ed.ac.uk> Date: Fri, 02 Jun 2000 18:39:12 +0100 From: Samson Abramsky Organization: Dept. of Computer Science, University of Edinburgh X-Mailer: Mozilla 3.04 (X11; I; Linux 2.0.36 i686) MIME-Version: 1.0 To: categories@mta.ca Subject: categories: TLCA 2001 Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: ******************************************************** * * TLCA 2001 * * 5th International Conference on * Typed Lambda Calculi and Applications * May 2 -- 5, 2001 * Krakow, Poland * ******************************************************** * CALL FOR PAPERS ******************************************************** The TLCA series of conferences aims at providing a forum for the presentation and discussion of current research in a field which was originally rather restricted, but has now expanded considerably. Typical areas include, but are not limited to: Proof theory: Natural Deduction and Sequent Calculi, Cut elimination and Normalization, Computational interpretations of Classical Logic, Linear Logic and Proof Nets, Bounded systems capturing complexity classes Semantics: Denotational semantics, Operational semantics, Game semantics, Realizability, Categorical models, Logical Relations, Full Completeness Implementation: Abstract machines, Parallel execution, Optimal Reduction Types: Polymorphism, Dependent types, Intersection types, Subtypes Logical Foundations: Logical Frameworks, Pure Type Systems, Proof checking Programming: Foundational aspects of: Functional programming, Proof search and logic programming, Connections between and combinations of functional and logic programming, Type checking, Higher-order rewriting, Higher-order unification and matching Important Dates =============== Deadline for Submissions: October 9, 2000 Notification to Authors: December 18, 2000 Final Versions due: February 1, 2001 The accepted papers will be published as a volume of the Springer Lecture Notes in Computer Science. Information about LNCS can be found at: http://www.springer.de/comp/lncs/index.html Submission Guidelines ===================== Papers should not exceed 15 standard A4 or US quarto pages, and should allow the Programme Committee to assess the merits of the work: in particular, references and comparisons with related work should be included. Submission of material already published or submitted to other conferences with published proceedings is not allowed. If available, e-mail addresses and fax numbers of the authors should be included. Electronic submissions ====================== Electronic submissions are strongly encouraged. A gzipped Postscript version of the paper should be sent as an e-mail message to: tlca01@comlab.ox.ac.uk In addition, the following information in ASCII format should be sent to this address in a **separate** e-mail: Title; authors; communicating author's name, address, and e-mail address and fax number if available; abstract of paper. Hard-copy submissions ===================== If electronic submission is not possible, authors may submit five (5) hard copies of the paper by post to the following address: TLCA 2001 (Attention: S. Abramsky) Oxford University Computing Laboratory Wolfson Building Parks Road Oxford OX1 3QD United Kingdom Questions concerning submissions ================================ These should be addressed to the Program Chair, Samson Abramsky: samson@dcs.ed.ac.uk Program Committee ================= S. Abramsky (Edinburgh) (chair) P.-L. Curien (Paris) P. Dybjer (Goteborg) T. Ehrhard (Marseille) M. Hasegawa (Kyoto) F. Honsell (Udine) D. Leivant (Bloomington) S. Ronchi della Rocca (Turin) H. Schwichtenberg (Munich) P. Scott (Ottawa) J. Tiuryn (Warsaw) Organizing Committee ==================== M. Zaionc (chair) P. Urzyczyn TLCA 2001 web page ================== http://www.ii.uj.edu.pl/zpi/tlca2001/ From rrosebru@mta.ca Mon Jun 5 13:43:14 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id NAA27742 for categories-list; Mon, 5 Jun 2000 13:37:44 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200006051354.e55DsWp05231@paprika.inria.fr> To: categories@mta.ca Subject: categories: PhD grant at INRIA Sophia Antipolis Date: Mon, 05 Jun 2000 15:54:32 +0200 From: Yves Bertot MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 X-MIME-Autoconverted: from 8bit to quoted-printable by paprika.inria.fr id e55DsWp05231 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id KAA24843 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: See the second part of this message for a translation in English. Bourse de doctorat à l'INRIA Sophia Antipolis Projet Lemme le projet Lemme de l'INRIA Sophia Antipolis propose une bourse de doctorat centrée sur les méthodes formelles basées sur Coq et sur la description de langages de programmation adaptés aux cartes à puces. Cette thèse s'intègrera dans le cadre d'une collaboration avec GemPlus, entreprise à la pointe du développement des cartes à puces, Les techniques étudiées devront permettre de développer des vérificateurs de byte-code formellement certifiés pour des langages approximant le langage JavaCard. L'objectif à terme est de fournir un vérificateur de byte-code entièrement prouvé correct pour le langage JavaCard tel qu'il est défini par JavaSun. L'étudiant travaillant avec cette bourse doctorale aura l'occasion d'approfondir ses compétences dans un domaine à l'intersection des domaines théoriques les plus ambitieux de la logique et de l'informatique fondamentale et des champs d'applications les plus dynamiques de l'évolution récente des technologies de l'information et de la communication (authentification, sécurité sur les réseaux, commerce électronique...). Les candidats intéressés devront envoyer un curriculum vitae et une lettre de motivation à Yves Bertot (Yves.Bertot@sophia.inria.fr). Liens utiles: http://www-sop.inria.fr/lemme http://www-sop.inria.fr/lemme/Yves.Bertot http://www.gemplus.com ================== In a collaboration with GemPlus, a leading company in the realm of smartcards, the Lemme Project at INRIA Sophia Antipolis proposes a PhD. grant centered around formal methods based on the Coq proof system and the description of programming languages adapted to smartcards. The studied techniques should make it possible to develop formally certified bytecode verifiers for languages close to JavaCard. The long term objective is to provide a fully formalized bytecode verifier for the whole JavaCard language. The student working on this topic will have the opportunity to strengthen her or his competence in a domain at the frontier between theoretical computer science and the most recent and exciting evolution of information and communication technology. Applications should be sent with a curriculum vitae to Yves Bertot (Yves.Bertot@sophia.inria.fr). For more web links: http://www-sop.inria.fr/lemme http://www-sop.inria.fr/lemme/Yves.Bertot http://www.gemplus.com From rrosebru@mta.ca Mon Jun 5 13:43:22 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id NAA28023 for categories-list; Mon, 5 Jun 2000 13:36:17 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <036d01bfcf0a$d9fca8e0$5b63fea9@tmp-sabadini.fis.unico.it> From: "RFC Walters" To: Subject: categories: CT 2000 Call for Posters Date: Mon, 5 Jun 2000 18:26:17 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Priority: 3 X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook Express 4.72.3110.5 X-MIMEOLE: Produced By Microsoft MimeOLE V4.72.3110.3 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: CALL FOR POSTERS CATEGORY THEORY 2000 (CT 2000) July 16-22, 2000 Centro di Cultura Scientifica "Alessandro Volta" di Villa Olmo Como, Italy The programme of talks for the conference is now available at the web page for the conference http://www.disi.unige.it/conferences/ct2000/ POSTER SESSION We are now calling for submissions to a Poster Session. Abstracts of the posters will be collected with those of the talks in the form of a booklet to be distributed at the conference. Submissions for abstracts of posters should be made in the form of a TeX/LaTeX file, and sent to ct2000@disi.unige.it. The size limit is 10 pages. The DEADLINE for submission is 30th June 2000. ACCOMMODATION REMINDER Accommodation in Como may be booked through the Centro di Cultura Scientifica "A. Volta", Villa Olmo, at the web page http://www.disi.unige.it/conferences/ct2000/accomodation_form.html The deadline for such a booking is 12th June 2000. CONFERENCE PROCEEDINGS We are planning to publish proceedings of the conference in an international journal. Details will appear shortly. A. Carboni, G. Rosolini, R.F.C. Walters Organizing Committee, CT 2000 From rrosebru@mta.ca Wed Jun 7 14:43:39 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA02749 for categories-list; Wed, 7 Jun 2000 14:05:31 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Peter Williams MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Message-ID: <14653.2207.197521.439622@rsunx.crn.cogs.susx.ac.uk> Date: Tue, 6 Jun 2000 15:20:15 +0100 (BST) To: categories@mta.ca Subject: categories: Faculty post in foundations of computer science X-Mailer: VM 6.75 under 21.1 (patch 6) "Big Bend" XEmacs Lucid Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id LAA30976 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: UNIVERSITY OF SUSSEX SCHOOL OF COGNITIVE AND COMPUTING SCIENCES Lecturer/Senior Lecturer in Foundations of Computer Science (Ref 358) Applications are invited for a permanent faculty position within the Subject Group of Computer Science and Artificial Intelligence. The expected start date is 1 October 2000 or as soon thereafter as possible. The Subject Group currently has active research groups in the Semantics of Computation and in Software Systems and Networks. Candidates should be able to show evidence of significant research achievement related to these research areas. Ideally they should be able to mediate between the two research groups, facilitating and encouraging joint research activity. Applicants with research interests in programming language design for distributed systems, from either a practical or theoretical perspective, would be particularly welcome. Details of the School of Cognitive and Computing Sciences are available at http://www.cogs.susx.ac.uk The post can be discussed informally with Professor Matthew Hennessy, phone +44 1273 678101, email matthewh@cogs.susx.ac.uk. Salary will be in the range: £17,238 to £22,579 (Grade A) or £23,521 to £30,065 (Grade B) on the Lecturer scale, or £31,563 to £35,670 on the Senior Lecturer scale. The level of appointment will be appropriate to the achievements and potential of the successful candidate. Closing date: Friday 30 June 2000. Application details are available from and should be returned to the Staffing Services Office, Sussex House, University of Sussex, Falmer, Brighton, BN1 9RH; phone +44 1273 877324, fax +44 1273 877401, email Recruitment@sussex.ac.uk. Further particulars and application forms are also available at http://www.sussex.ac.uk/Units/staffing/personnl/vacs/ From rrosebru@mta.ca Wed Jun 7 15:28:50 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA15219 for categories-list; Wed, 7 Jun 2000 14:06:47 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 6 Jun 2000 16:06:08 +0200 (MET DST) Message-Id: <200006061406.QAA08437@disi.unige.it> Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" To: etaps2001@disi.unige.it From: etaps2001@disi.unige.it (Etaps 2001) Subject: categories: ETAPS 2001: FIRST ANNOUNCEMENT & CALL FOR SUBMISSIONS Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id LAA04484 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: ETAPS 2001 APRIL 2 - 6, 2001 GENOVA - ITALY The European Joint Conferences on Theory and Practice of Software (ETAPS) is a loose and open confederation of conferences and other events that has become the primary European forum for academic and industrial researchers working on topics relating to Software Science. http://www.disi.unige.it/etaps2001/ FIRST ANNOUNCEMENT & CALL FOR SUBMISSIONS ----------------------------------------------------------------------- 5 Conferences - Tutorials - Tool Demonstrations - 7 Satellite Events ----------------------------------------------------------------------- Conferences ----------------------------------------------------------------------- CC 2001: International Conference on Compiler Construction Chair: Reinhard Wilhelm ESOP 2001, European Symposium On Programming Chair: David Sands FASE 2001, Fundamental Approaches to Software Engineering Chair: Heinrich Hußmann FOSSACS 2001, Foundations of Software Science and Computation Structures Chair: Furio Honsell TACAS 2001, Tools and Algorithms for the Construction and Analysis of Systems Chairs: Tiziana Margaria and Wang Yi Prospective authors are invited to submit, before October 20, 2001, full papers in English presenting original research. Submitted papers must be unpublished and not submitted for publication elsewhere. In particular, simultaneous submission of the same contribution to multiple ETAPS conferences is forbidden. The proceedings of each main conference will be published as a separate volume in the Springer Verlag Lecture Notes in Computer Science series. Tutorials ----------------------------------------------------------------------- Proposals for half-day or full-day tutorials related to ETAPS 2001 are invited. Tutorial proposals will be evaluated on the basis of their assessed benefit for prospective participants to ETAPS 2001. Contact: Bernhard Rumpe, (Technische Universitaet Munchen, Germany) etaps2001-tut@forsoft.de Tool Demonstrations ----------------------------------------------------------------------- Demonstrations of tools presenting advances on the state of the art are invited. Submissions in this category should present tools having a clear connection to one of the main ETAPS conferences, possibly complementing a paper submitted separately. These should not be confused with contributions to TACAS, which emphasizes principles of tool design, implementation, and use, rather than focusing on specific domains of application. Contact: Don Sannella (University of Edinburgh) etaps2001-demo@dcs.ed.ac.uk Satellite Events ----------------------------------------------------------------------- Besides the five main conferences the following satellite events are planned for ETAPS 2001 CMCS: Co-algebraic Methods in Computer Science Contact: Ugo Montanari (Universita' di Pisa, Italy) ETI Day: Electronic Tool Integration platform Day Contacts: Tiziana Margaria (Universitaet Dortmund, Germany) and Andreas Podelski (MPI Saarbrucken, Germany) LDTA: Workshop on Language Descriptions, Tools and Applications Contact: Mark van den Brand (CWI Amsterdam, The Netherlands) PFM: Proofs For Mobility Contact: Davide Sangiorgi (INRIA-Sophia Antipolis, France) RelMiS: Relational Methods in Software Contact: Wolfram Kahl (Universitaet der Bundeswehr Munchen, Germany) UNIGRA: Uniform Approaches to Graphical Process Specification Techniques Contact: Julia Padberg (Technische Universitaet Berlin, Germany) WADT: Workshop on Algebraic Development Techniques Contact: Maura Cerioli (DISI-Universita' di Genova, Italy) Important Dates: ----------------------------------------------------------------------- October 20, 2000: Submissions Deadline for the Main Conferences, Demos and Tutorials December 15, 2000: Notification of Acceptance/Rejection January 15 2001: Camera-ready Version Due April 2-6, 2001: ETAPS 2001 in Genova March 31 - April 8, 2001: Satellite Events ----------------------------------------------------------------------- From rrosebru@mta.ca Thu Jun 8 10:33:29 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA26046 for categories-list; Thu, 8 Jun 2000 10:31:44 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <393F9794.D4FF8D6A@di.fc.ul.pt> Date: Thu, 08 Jun 2000 13:54:44 +0100 From: Nuno Barreiro X-Mailer: Mozilla 4.72 [en] (X11; I; Linux 2.0.36 i686) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: LINEAR Summer School (Last call) References: <390F9E04.B3035C9F@di.fc.ul.pt> <39247952.ED779DDC@di.fc.ul.pt> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Please forward. We apologize for any duplication of this message in your mailbox. Best regards, Nuno Barreiro ------------------------------------------------------------------ ================================ = = = Deadline for applications: = = = = = = JUNE 15th = = = ================================ The LINEAR International Summer School (Linear Logic and Applications) August 30 to September 7, 2000 Hotel Terra Nostra, S.Miguel, Azores, Portugal The Linear TMR research network (http://iml.univ-mrs.fr/LINEAR) is proud to announce its first International Summer School on Linear Logic and Applications. The school is directed to everyone doing postgraduate work in Computer Science or Mathematics with an interest in the field of Formal Logic and its applications. The school lasts one week and comprises both lectures and thematic sessions. The lectures are in the tradition of summer schools and cover one topic, from basic material to more advanced issues. The topics and lecturers are the following: Samson Abramsky --- Game Semantics Jean-Yves Girard -- Linear Logic and Ludics Stefano Guerrini -- Proof-Nets and Lambda-Calculus Yves Lafont ------- Phase Semantics and Decision Problems Phil Scott -------- Category Theory and Concrete Models The thematic sessions will cover state-of-the-art research in Linear Logic. Each session has an organiser responsible for inviting speakers who will talk about their work. The themes and organisers are the following: Andrea Asperti ---- Applications Vincent Danos ----- Proof Theory Thomas Ehrhard ---- Semantics Glynn Winskel ----- Concurrency The school will be held in the island of S.Miguel, Azores, amid luxurious vegetation and hot water springs. The entrance to the mythic kingdom of the Atlantis is believed to be located near Hotel Terra Nostra, some say at the bottom of its famous red and hot water swimming pool... Detailed information and application forms are available at http://linear.di.fc.ul.pt Don't forget to check it! From rrosebru@mta.ca Fri Jun 9 11:13:04 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA24650 for categories-list; Fri, 9 Jun 2000 11:10:10 -0300 (ADT) X-Authentication-Warning: bebop.math.ist.utl.pt: pmr owned process doing -bs Date: Thu, 8 Jun 2000 18:12:43 +0100 (WET DST) From: Pedro Manuel Resende To: categories@mta.ca Subject: categories: symmetric frame of a suplattice: question Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from QUOTED-PRINTABLE to 8bit by mailserv.mta.ca id OAA10498 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: The symmetric frame of a sup-lattice L is the frame freely generated by L with sups being preserved in the presentation. Classically (ie, with the truth value object being 2) it is easy to show that the injection of generators is 1-1. Does anyone know whether this also holds in an arbitrary topos? Thanks, ---------------------------------------------------------------------- Pedro Resende Departamento de Matemática Tel.: +351 218 417 149 Instituto Superior Técnico Fax: +351 218 417 048 / 598 Av. Rovisco Pais E-mail: pmr@math.ist.utl.pt 1049-001 Lisboa, Portugal WWW: http://www.math.ist.utl.pt/~pmr ---------------------------------------------------------------------- From rrosebru@mta.ca Mon Jun 12 13:13:13 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id NAA14831 for categories-list; Mon, 12 Jun 2000 13:10:20 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 12 Jun 2000 16:05:19 +0100 From: Paul Taylor Message-Id: <200006121505.QAA29030@koi-pc.dcs.qmw.ac.uk> To: categories@mta.ca Subject: categories: lifting and non-Artin gluing Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Non-Artin Gluing in Recursion Theory and Lifting in the Abstract Stone Duality for "Category Theory 2000", Como http://hypatia.dcs.qmw.ac.uk/author/TaylorP The analogy between `open' and `recursively enumerable' sets has long been a mainstay of theoretical computer science, but the traditional axiomatisation of general topology involving arbitrary unions is an obstacle to the formal unification of these disciplines. In particular, whilst Artin showed how to glue an open subspace to its closed complement using a comma square of frames, we give a diagonalisation argument to show that this representation fails for any recursively enumerable subset of $\mathbb N$ that is not decidable. Abstract Stone Duality is a re-axiomatisation based on the monadic adjunction between the dual categories of `frames' and `spaces'. Despite the failure of Artin gluing, we show in this formulation that the lift or scone, constructed using a comma square, still provides the classifier for partial maps with open domain of definition. As the axiomatisation is not given in terms of finite intersections and arbitrary unions, a careful study of the modular law is needed to prove this. I would very much like to receive comments and references to relevant work on * Artin gluing and the partial map classifier FOR LOCALES (not toposes), * modular lattices and the (Goursat?) equation ab=bab for idempotents. I will be preparing an abridged version for the Como proceedings during the last week in June, and submitting the paper to "Theory and Applications of Categories" at the same time. The first paper on "Abstract Stone Duality" has been with the TAC referees for nearly a year. Both can be found linked from my Hypatia page. Paul From rrosebru@mta.ca Wed Jun 14 12:52:42 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA01487 for categories-list; Wed, 14 Jun 2000 12:49:33 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <20000613075246.23146.qmail@web1801.mail.yahoo.com> Date: Tue, 13 Jun 2000 00:52:46 -0700 (PDT) From: besick dundua Subject: categories: ANNOUNCEMENT Tbilisi Summer School To: categories@mta.ca MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: ANNOUNCEMENT Tbilisi Summer School in Language, Logic, and Computation 29th August - 8 September 2000 Tbilisi, Georgia The Georgian Centre for Language, Logic, and Speech, based at the Tbilisi State University, will host Tbilisi Summer School, main purpose of which is to make the students and young scholars acquainted with the modern state of affairs in the mentioned fields of science, and - at the same time - to further contacts and scientific collaboration between Western and Eastern Scholars LECTURERS Jurij Apresjan, Moscow Matthias Baaz, Vienna Pascal Boldini, Paris Marina Glavinskaja, Moscow Michel Parigot, Paris Carl Vogel,Dublin Andrej Voronkov, Manchester COURSES - Foundations of linguistic semantics (Ju.Apresjan) - On the generalisation of proofs and calculations (M.Baaz) - Type theories for semantics and cognition (P.Boldini) - Semantics of aspect (M.Glavinskaja) - Proofs as programs (M.Parigot) - Cognitive constraints on linguistic theory. (C.Vogel) - Logical Foundations of deductive databases. (A.Voronkov). STUDENTS Besides local audience we shall be glad to see at the School foreign students also. Participants fee for such persons will amount to $120 (excursion, banquet, reprints, etc.). They could be comfortably accommodated at Georgian families (with two meals) - $40 per day. LOCATION AND SIGHTSEEING TOURS Georgia is the ancient country situated between Black and Caspian seas, Caucasus Mountains and Turkey. This is the country of Golden Fleece, myth of Argonauts, Jason and Medea, Promethee, chained to the Caucasus mountains. Tbilisi - capital of Georgia - has more than 1 million in habitant. It is situated some 100-150 km to the south of main Caucasus ridge, in the beautiful valley of the river Mtkvari, surrounded by the green slopes of the Caucasus spurs. The city has a long (1500 year) history and abounds in historical and cultural memorials. Georgia is famous for its high quality wines, exquisite cuisine and cordial hospitality. The main site of the Symposium, Tbilisi state University, is the chief centre of education in the country, and has several outstanding scholars in science, art and politics among its graduates. As a route of excursion is chosen the Georgian Military Road going via ancient capital of Georgia - Mtskheta, with its abundant architectural and historical monuments, crossing the main ridge of Caucasus by the Cross Pass and reaching the final point of supposed trip - mountain resort Kazbegi with its Trinity Church situated on the top of high peak facing the second (after Elbrus) mountain - peak of Caucasus - Mkinvarcveri (Glacier - mountain). TRAVEL INFORMATION The only real way of arrival in Tbilisi is by air. If direct flight from the point of your departure does not exist, the preferable ways are via Istambul, Frankfurt or Moscow. ORGANISING COMMITTEE: T.Khurodze (Chair, Pro-rector of Tbilisi State University) R.Asatiani (Institute of Oriental Studies) N.Chanishvili (Tbilisi State University) G.Chikoidze (Institute of Control Systems) K.Pkhakadze (Institute of Applied Mathematics) Kh.Rukhaja (Institute of Aplied Mathematics). For additional information, please, use the following addresses: www.geocities.com/summer_school_2000 www.risc.uni-linz.ac.at/people/tkutsia/summerschool/ or contact the organisation comitie: George Chikoidze Dept. of Language Modelling Inst. of Control Systems Georgian Academy of Sciences 34, K. Gamsakhurdia 380060 Tbilisi Georgia Phone: +995 32 382136 E-mail: chiko@contsys.acnet.ge Khimuri Rukhaia Institute of Applied Mathematics Phone:+995 32 316825 E-mail: rukhaia@viam.hepi.edu.ge Kote Pkhakadze Institute of Applied Mathematics Phone: +995 32 325929 E-mail: pkhakadz@viam.hepi.edu.ge Beso Dundua Institute of Applied Mathematics Phone: +995 32 325441 E-mail: b_dundua@yahoo.com __________________________________________________ Do You Yahoo!? Yahoo! Photos -- now, 100 FREE prints! http://photos.yahoo.com From rrosebru@mta.ca Wed Jun 14 12:52:46 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA18074 for categories-list; Wed, 14 Jun 2000 12:48:30 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <39451BD9.5C6EB5FD@cse.psu.edu> Date: Mon, 12 Jun 2000 13:20:25 -0400 From: Catuscia Palamidessi Organization: Penn State University X-Mailer: Mozilla 4.7 [en] (X11; U; SunOS 5.7 sun4u) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: CONCUR 2000: Call for Participation and Final Program Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: CALL FOR PARTICIPATION and FINAL PROGRAM CONCUR 2000 11th International Conference on Concurrency Theory State College, Pennsylvania, USA, August 22--25, 2000. URL: http://www.cse.psu.edu/concur2000/ E-mail: concur2000@cse.psu.edu (apologies for multiple copies) REGISTRATION It is now time to register for CONCUR 2000. See the above mentioned WWW pages for the registration procedure. Early registration ends on July 12, 2000. CONCUR The purpose of the CONCUR conferences is to bring together researchers, developers and students in order to advance the theory of concurrency, and promote its applications. PROGRAM ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Monday 21 August ---------------- 9:00 - 5:30 Satellite Workshop EXPRESS'00: 7th International Workshop on Expressiveness in Concurrency 9:00 - 5:30 Satellite Workshop GETCO 2000: 2nd Workshop on Geometric and Topological Methods in Concurrency Theory ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Tuesday 22 August ----------------- 8:45 - 9:00 OPENING 9:00 - 10:00 SESSION 1 Invited talk: Combining Theorem Proving and Model Checking through Symbolic Analysis by Natarajan Shankar 10:00 - 10:30 COFFEE BREAK 10:30 - 12:30 SESSION 2 Open Systems in Reactive Environments: Control and Synthesis by Orna Kupferman, P. Madhusudan, P.S. Thiagarajan, Moshe Y. Vardi Model Checking with Finite Complete Prefixes is PSPACE-complete by Keijo Heljanko Verifying Quantitative Properties of Continuous Probabilistic Timed Automata by Marta Kwiatkowska, Gethin Norman, Roberto Segala, Jeremy Sproston The Impressive Power of Stopwatches by Franck Cassez, Kim Larsen 12:30 - 2:00 LUNCH 2:00 - 3:30 SESSION 3 (parallel) Optimizing Buchi Automata by Kousha Etessami, Gerard Holzmann Generalized Model Checking: Reasoning about Partial State Spaces by Glenn Bruns, Patrice Godefroid Reachability Analysis for Some Models of Infinite-State Transition Systems by Oscar H. Ibarra, Tevfik Bultan, Jianwen Su 2:00 - 3:30 SESSION 4 (parallel) Process spaces by Radu Negulescu Failure Semantics for the Exchange of Information in Multi-Agent Systems by Frank S. de Boer, Rogier M. van Eijk, Wiebe van der Hoek, John-Jules Ch. Meyer Proof-Outlines for Threads in Java by E. Abraham-Mumm, F.S. de Boer 3:30 - 4:00 COFFEE BREAK 4:00 - 5:30 SESSION 5 (parallel) Tutorial: Programming Access Control: The Klaim Experience by Rocco De Nicola 4:00 - 5:30 SESSION 6 (parallel) Tutorial: Exploiting Hierarchical Structure for Efficient Formal Verification by Rajeev Alur 6:30 - 8:00 RECEPTION (at the Nittany Lion Inn) ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Wednesday 23 August ------------------- 9:00 - 10:00 SESSION 7 Invited talk: Verification is Experimentation! by Ed Brinksma 10:00 - 10:30 COFFEE BREAK 10:30 - 12:30 SESSION 8 Deriving Bisimulation Congruences for Reactive Systems by James J. Leifer, Robin Milner Bisimilarity Congruences for Open Terms and Term Graphs via Tile Logic by Roberto Bruni, David de Frutos-Escrig, Narciso Marti-Oliet, Ugo Montanari Process Languages for Rooted Eager Bisimulation by Irek Ulidowski, Shoji Yuen Action Contraction by Arend Rensink 12:30 - 2:00 LUNCH 2:00 - 9:00 SOCIAL EXCURSION AND DINNER ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Thursday 25 August ------------------ 9:00 - 10:00 SESSION 9 Invited talk: Compositional Performance Analysis using Probabilistic I/O Automata by Eugene W. Stark 10:00 - 10:30 COFFEE BREAK 10:30 - 12:30 SESSION 10 A Theory of Testing for Markovian Processes by Marco Bernardo, Rance Cleaveland Reasoning about probabilistic lossy channel systems by Parosh Abdulla, Christel Baier, Purushothaman Iyer, Bengt Jonsson Weak Bisimulation for Probabilistic Systems by Anna Philippou, Insup Lee, Oleg Sokolsky Nondeterminism and Probabilistic Choice: Obeying the Laws by Michael W. Mislove 12:30 - 2:00 LUNCH 2:00 - 3:30 SESSION 11 (parallel) Secrecy and Group Creation by Luca Cardelli, Giorgio Ghelli, Andrew D. Gordon On the reachability problem in cryptographic protocols by Roberto Amadio, Denis Lugiez Secure information flow for concurrent processes by Jan J\"urjens 2:00 - 3:30 SESSION 12 (parallel) LP Deadlock Checking Using Partial Order Dependencies by Victor Khomenko, Maciej Koutny Pomsets for Local Trace Languages: Recognizability, Logic & Petri Nets by D. Kuske, R. Morin Functorial Concurrent Semantics for Petri Nets with Read and Inhibitors arcs by Paolo Baldan, Nadia Busi, Andrea Corradini, Michele Pinna 3:30 - 4:00 COFFEE BREAK 4:00 - 5:30 SESSION 13 (parallel) Tutorial: From Process Calculi to Process Frameworks by Philippa Gardner 4:00 - 5:30 SESSION 14 (parallel) Tutorial: Verification using Tabled Logic Programming by C. R. Ramakrishnan ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Friday 26 August ---------------- 9:00 - 10:00 SESSION 15 Invited talk: Formal Models for Communication-based Design by Alberto Sangiovanni-Vincentelli 10:00 - 10:30 COFFEE BREAK 10:30 - 12:30 SESSION 16 The Control of Synchronous Systems by Luca de Alfaro, Thomas A. Henzinger, Freddy Y.C. Mang Typing Non-Uniform Concurrent Objects by Antonio Ravara, Vasco T. Vasconcelos An Implicitly-Typed Deadlock-Free Process Calculus by Naoki Kobayashi, Shin Saito, Eijiro Sumii Typed Mobile Objects by Michele Bugliesi, Giuseppe Castagna, Silvia Crafa 12:30 - 2:00 LUNCH 2:00 - 3:30 SESSION 17 Synthesizing distributed finite-state systems from MSCs by Madhavan Mukund, K Narayan Kumar, Milind Sohoni Emptiness is decidable for asynchronous cellular machines by Dietrich Kuske Revisiting safety and liveness in the context of failures by Bernadette Charron-Bost, Sam Toueg, Anindya Basu 3:30 - 4:00 COFFEE BREAK 4:00 - 5:30 SESSION 18 Well-Abstracted Transition Systems by Alain Finkel, Purushothaman Iyer, Gregoire Sutre A Unifying Approach to Data-independence by Ranko Lazic, David Nowak Chi Calculus with Mismatch by Yuxi Fu, Zhenrong Yang 5:30 - 5:40 CLOSING ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Saturday 26 August ---------------- 9:00 - 12:30 Satellite Workshop YOO: Why Object-Orientation 9:00 - 5:30 Satellite Workshop MTCS 2000: International Workshop on Models for Time-Critical Systems ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ ADDRESS Catuscia Palamidessi Dept. of Computer Science and Engineering FAX: (814) 865-3176 The Pennsylvania State University Email: catuscia@cse.psu.edu 325 Pond Laboratory Phone: (814) 863-3599 University Park, PA 16802-6106 USA http://www.cse.psu.edu/~catuscia From rrosebru@mta.ca Thu Jun 15 17:08:41 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id RAA28469 for categories-list; Thu, 15 Jun 2000 17:05:01 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <217F6DFA440ED111ACDA00A0C906B00601AAE1F6@arsenic.rcp.co.uk> From: Michael Abbott To: "'categories@mta.ca'" Subject: categories: Three questions about fibrations Date: Thu, 15 Jun 2000 18:02:23 +0100 MIME-Version: 1.0 X-Mailer: Internet Mail Service (5.5.2650.21) Content-Type: text/plain; charset="iso-8859-1" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: I am wondering if anyone can give references for three remarks Wesley Phoa makes in the chapter on fibrations of his paper "An introduction to fibrations, topos theory, the effective topos and modest sets". 1. Essentially Algebraic Theories In the footnote on page 7 Phoa comments: "[fibrations] are the models for a first-order, 'essentially algebraic' theory". I'm not quite sure what he means here, and this sounds like it must be a standard and well known connection. I'd be glad of a reference. 2. Splitting Fibrations At the bottom of page 14 Phoa observes: "Every fibration .. is equivalent to a split fibration (there is an elegant proof due to John Power). However, it's not clear how to extend this result to more complicated structures. This is the coherence problem ..." Now I know that any fibration is equivalent to a split fibration via the "fibred Yoneda lemma" (Borceux, "Handbook of Categorical Algebra 2", 8.2.7 and Jacobs, "Categorical Logic and Type Theory"), but I don't think that's the only splitting available, and I'm not sure that this correspondence helps very with coherence questions. I am aware of another, different, equivalent splitting, and I wonder if there are any references. In particular, can anyone guess what reference by John Power Phoa was referring to? In particular, I'd be very interested in any other observations on the "coherence problem". 3. Generalising the Definition In the footnote on page 12, in reference to the definition of a fibration, Phoa says: "If one really wants to take .. 2-categorical issues seriously, one needs .. a more sophisticated definition of 'fibration'." I can make some promising looking guesses. Any references? Many thanks. Michael Abbott From rrosebru@mta.ca Fri Jun 16 10:09:25 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA07378 for categories-list; Fri, 16 Jun 2000 10:08:07 -0300 (ADT) X-Authentication-Warning: triples.math.mcgill.ca: rags owned process doing -bs Date: Fri, 16 Jun 2000 00:43:33 -0400 (EDT) From: "Robert A.G. Seely" To: "categories@mta.ca" Subject: categories: Re: Three questions about fibrations In-Reply-To: <217F6DFA440ED111ACDA00A0C906B00601AAE1F6@arsenic.rcp.co.uk> Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: On Thu, 15 Jun 2000, Michael Abbott wrote: > I am wondering if anyone can give references for three remarks Wesley Phoa > makes in the chapter on fibrations of his paper "An introduction to > fibrations, topos theory, the effective topos and modest sets". At this point, I think your best bet is to get a copy of Bart Jacobs excellent book "Categorical Logic and Type Theory" - which (in spite of its title?) is all about fibrations (and logic and type theory - actually I think it is well-titled, though you might not have guessed it was what you needed from the title). (There is a review of this book on my web page, link below.) -= rags =- ================== R.A.G. Seely From rrosebru@mta.ca Fri Jun 16 16:18:02 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id QAA09679 for categories-list; Fri, 16 Jun 2000 16:17:23 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <394A7C1D.A0526AA2@math.ist.utl.pt> Date: Fri, 16 Jun 2000 19:12:29 +0000 From: Claudio Hermida Organization: CMA, IST X-Mailer: Mozilla 4.7 [en] (X11; I; Linux 2.2.12-20 i686) X-Accept-Language: en MIME-Version: 1.0 To: "categories@mta.ca" Subject: categories: Re: Three questions about fibrations References: <217F6DFA440ED111ACDA00A0C906B00601AAE1F6@arsenic.rcp.co.uk> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Michael Abbott wrote: > I am wondering if anyone can give references for three remarks Wesley Phoa > makes in the chapter on fibrations of his paper "An introduction to > fibrations, topos theory, the effective topos and modest sets". I think I can provide some meaningful answers to these questions, but of course, one should always take such (throwaway) remarks in an informal exposition with a pinch of black pepper. > > 1. Essentially Algebraic Theories > > In the footnote on page 7 Phoa comments: > "[fibrations] are the models for a first-order, 'essentially > algebraic' theory". > > I'm not quite sure what he means here, and this sounds like it must be a > standard and well known connection. I'd be glad of a reference. > Fibrations as finite-limit theories: This follows from the analysis in [S], that exhibits fibrations as (adjoint) pseudo-algebras in any 2-category with comma-objects. In particular, for any category B with pullbacks, the 2-category Cat(B) of internal categories in B admits them. > > 2. Splitting Fibrations > > At the bottom of page 14 Phoa observes: > "Every fibration .. is equivalent to a split fibration (there is an > elegant proof due to John Power). However, it's not clear how to extend > this result to more complicated structures. This is the coherence problem > ..." > > Now I know that any fibration is equivalent to a split fibration via the > "fibred Yoneda lemma" (Borceux, "Handbook of Categorical Algebra 2", 8.2.7 > and Jacobs, "Categorical Logic and Type Theory"), but I don't think that's > the only splitting available, and I'm not sure that this correspondence > helps very with coherence questions. > I am aware of another, different, equivalent splitting, and I wonder > if there are any references. In particular, can anyone guess what reference > by John Power Phoa was referring to? > In particular, I'd be very interested in any other observations on > the "coherence problem". > Split fibrations: Since fibrations are pseudo-algebras, it follows from Power's coherence theorem [P] (which applies in this situation) that every fibration is equivalent (over its base category) to a split one. The construction there does not appeal to Yoneda. Yet, given that fibrations are actually properties, that is adjoint pseudo-algebras, one can give a neat explicit description of the associated split one as follows: Given p:E->B, consider the free fibration over it, E/p -> B. The unit \eta: E -> E/p takes X |-> X,id_(pX). The right adjoint r: E/p -> E amounts to a choice of cartesian lifting: (Y,u:I->pY) |-> u*(Y). Thus we get a comonad \eta o r: E/p -> E/p. The resulting Kleisli category (E/p)_(\eta r) is fibred over B and gives the corresponding split fibration. The equivalence is given by the composite E -\eta-> E/p -J-> (E/p)_(\eta r). The above construction is a special case of the theory in [H], specially section 11. The paper and the references there in provide further material on coherence. > > 3. Generalising the Definition > > In the footnote on page 12, in reference to the definition of a fibration, > Phoa says: > "If one really wants to take .. 2-categorical issues seriously, one > needs .. a more sophisticated definition of 'fibration'." > > I can make some promising looking guesses. Any references? > Generalised fibrations: The only meaningful generalisation (in the categorical context) proposed so far in the literature is that of [S1], fibrations "up to equivalence". However I can see no impediment whatsoever at taking 2-category theory seriously with the standard (Grothendieck) notion of fibration, so I cannot guess what the author means. References: [S] R. Street, Fibrations and Yoneda Lemma in a 2-category, Category Seminar, LNM 420, 1973. [S1] R. Street, Fibrations in bicategories, Cahiers Top.Geom.Diff.Cat, 21, 1980. [P] A.J.Power, A general coherence result, JPAA, 57(2):165-173, 1989. [H] C. Hermida, From coherence structure to universal properties, (to appear JPAA) (available at http://www.cs.math.ist.utl.pt/s84.www/cs/claudio.html) Claudio Hermida From rrosebru@mta.ca Fri Jun 16 16:42:38 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id QAA22256 for categories-list; Fri, 16 Jun 2000 16:42:32 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: categories@mta.ca Subject: categories: Festival Workshop in Foundations and Computations Message-Id: From: Fairouz Kamareddine Date: Wed, 14 Jun 2000 19:50:03 +0100 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Festival Workshop in Foundations and Computations Heriot-Watt University, Edinburgh Sunday 16 July-Tuesday 18 July 2000 http://www.cee.hw.ac.uk/~fairouz/festival/workshop1/ This workshop is a part of a research festival at Heriot-Watt University, Edinburgh, during parts of the summer of 2000. During the festival, international and national researchers spend short/long time at Heriot-Watt during which a lively research environment will take place. There will be many seminars during the festival details of which are advertised separately. When the visits coincide with a particular theme, a workshop will be held on that theme. If you like to take part in the festival and/or give a talk, contact fairouz@cee.hw.ac.uk. Grants are available for parts or all of the registration fees and accommodation. Contact fairouz@cee.hw.ac.uk for details. The first workshop in the festival is a workshop on foundations and computations. If you have a relevant talk, submit a three page abstract to fairouz@cee.hw.ac.uk by 25 June 2000. You will be informed of acceptance by 5 July 2000. Speakers and Topics Gilles Dowek (INRIA-Rocquencourt, FR): About Folding-Unfolding Cuts Jan van Eijck(University of Amsterdam, NL): Dynamic First Order Logic Jacques Fleuriot (University of Edinburgh, UK): Automating Newton's calculus in Isabelle Therese Hardin (Paris 6 and INRIA-Rocquencourt, FR): The calculus of contexts of lambda-sigma Roger Hindley (University of Swansea, UK): The birth of lambda-calculus and combinatory logic Alan Mycroft (Cambridge University and AT&T Labs, UK): Type Based Decompilation Gopalan Nadathur (University of Chicago, USA): proof theory and procedures for fragments of intuitionistic logic Gopalan Nadathur (University of Chicago, USA): implementation of higher-order logic programming languages Iain Stewart (University of Leicester, UK): A programming approach to descriptive complexity theory Grants Grants cover part or all of the registration fee and accommodation. We strongly welcome applications from women researchers, researchers who work in industry, and researchers whose place of work is in a less-favoured region. If you are not sure about eligibility, send an email to fairouz@cee.hw.ac.uk. The form for application for funding can be found on the above URL. Deadline for receipt of grant applications is 30 June 2000. You will receive notification of acceptance/rejection by 5 July 2000. In order to guarantee accommodation, it is advisable that your application is sent as soon as possible. The summer is a very busy time in Edinburgh. From rrosebru@mta.ca Mon Jun 19 08:54:25 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id IAA09805 for categories-list; Mon, 19 Jun 2000 08:46:12 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Mime-Version: 1.0 X-Sender: street@hera.mpce.mq.edu.au Message-Id: Date: Mon, 19 Jun 2000 17:13:05 +1000 To: "categories@mta.ca" From: Ross Street Subject: categories: A question on: Content-Type: text/plain; charset="us-ascii" ; format="flowed" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: I thought the CatNet would be interested in the following question which appeared on . The letter was pointed out to me by a colleague at Macquarie. --Ross ************************************************* From: mathwft@math.canterbury.ac.nz (Bill Taylor) Newsgroups: sci.math Subject: Query about Category Theory. Date: 18 Jun 2000 05:36:30 GMT Organization: Department of Mathematics and Statistics, University of Canterbury, Christchurch, NewZealand Does anyone know of any cases where Category Theory (morphisms, functors & all that) has helped solve an unsolved problem? That is, a problem in some other branch of math, posed without reference to categorical ideas, and previously unsolved, that was first solved via Category T. I realize that CT provides a unifying framework for many seemingly disparate ideas in math, and that is a fine thing of course; but I was just wondering if it had this problem-solving capability. TIA for any helpful responses. ---------------------------------------------------------------------------- --- Bill Taylor W.Taylor@math.canterbury.ac.nz From rrosebru@mta.ca Wed Jun 21 12:43:39 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id MAA15149 for categories-list; Wed, 21 Jun 2000 12:39:08 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3950CFE5.579C8391@bangor.ac.uk> Date: Wed, 21 Jun 2000 15:23:33 +0100 From: Ronnie Brown X-Mailer: Mozilla 4.72 [en] (Win98; I) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: A question on: Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: I have a paper with Loday on calculating the third homotopy group of a suspension of a K(G,1) 51. (with J.-L. LODAY), ``Van Kampen theorems for diagrams of spaces'', {\em Topology} 26 (1987) 311-334. in terms of a new tensor product of non abelian groups. It would not be a sensible task to rewrite the paper without category theory (considered as a unifying principle, as a mode for efficient calculation in certain algebraic structures, and as a supplier of new algebraic structures). To go further back (and higher, of course) Grothendieck's extension of the Riemann-Roch Theorem uses category theory explicitly. In the 1950's people were trying to give algebraic proofs of this theorem, when AG came up with an algebraic proof of a vast generalisation. Then there is the categorical background to the proof of the Weil conjectures .... But the question is misplaced - in the early part of the 20th century, I expect some would ask if set theory was really necessary for a confirmed problem solver! The history of maths shows that maths greatest contribution to science, culture and technology has been in terms of expressive power, to give a language for intuitions which enables exact description, calculation, deduction. (Exam question: discuss the last statement, with an emphasis on particular examples!) It also allows for the *formulation* of new problems, which perhaps cause old interests to lapse as people perceive there are more exciting things to do. It is a narrow view to regard `important maths' as necessarily that which solves well known problems, and so leave evaluation as akin to a sports league table: how old is the problem? who has worked on it? etc, etc. The progress of maths is much more complicated and interesting than that! It won't help the public image of maths if it is seen that mathematicians believe the most important aspect of their subject is a (to the public) bizarre set of problems which seem to interest no one else. However, it is important that these questions be asked, together with questions on modes for evaluating `good maths'. As AG remarked in a letter, maths was held back for centuries for lack of the `trivial' concept of zero! For more discussion, look at http://www.bangor.ac.uk/ma/CPM/cdbooklet/knots-m.html knots2.html So let the debate be broadened and continued! Ronnie Brown (will someone please forward this to the newsgroup?) PS I am trying to trace a combinatorics problem solved in the 1950s using categories of paths, and which was at the time held up as the sort category theory could not do! Maybe my memory is failing! But the question put on the newsgroup is an old war horse! -------- Original Message -------- Subject: categories: A question on: Date: Mon, 19 Jun 2000 17:13:05 +1000 From: Ross Street To: "categories@mta.ca" I thought the CatNet would be interested in the following question which appeared on . The letter was pointed out to me by a colleague at Macquarie. --Ross ************************************************* From: mathwft@math.canterbury.ac.nz (Bill Taylor) Newsgroups: sci.math Subject: Query about Category Theory. Date: 18 Jun 2000 05:36:30 GMT Organization: Department of Mathematics and Statistics, University of Canterbury, Christchurch, NewZealand Does anyone know of any cases where Category Theory (morphisms, functors & all that) has helped solve an unsolved problem? That is, a problem in some other branch of math, posed without reference to categorical ideas, and previously unsolved, that was first solved via Category T. I realize that CT provides a unifying framework for many seemingly disparate ideas in math, and that is a fine thing of course; but I was just wondering if it had this problem-solving capability. TIA for any helpful responses. ---------------------------------------------------------------------------- --- Bill Taylor W.Taylor@math.canterbury.ac.nz From rrosebru@mta.ca Thu Jun 22 10:12:02 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id KAA22081 for categories-list; Thu, 22 Jun 2000 10:09:18 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Frank Atanassow To: categories@mta.ca Subject: categories: Adjoints in bicategories Message-Id: <20000622124507.EF71C451D@mail.cs.uu.nl> Date: Thu, 22 Jun 2000 14:45:07 +0200 (MET DST) Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: I'm looking for definitions of (the weak 2-dimensional analogues of 1-) products and coproducts for bicategories, and also adjoints. In his 1967 article "Introduction to Bicategories, Part I" Benabou promises to treat biadjoints in a sequel, but I gather this was never published. Gray treats a notion of "quasi-adjointness" in "Formal Category Theory"; is this accepted as the "right" generalization? Pointers to definitions of these concepts in one of the approaches to weak n-categories would be welcome as well. -- Frank Atanassow, Dept. of Computer Science, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-1012, Fax +31 (030) 251-3791 From rrosebru@mta.ca Fri Jun 23 14:40:12 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA18986 for categories-list; Fri, 23 Jun 2000 14:35:01 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <39538CC4.CEB0D163@math.ist.utl.pt> Date: Fri, 23 Jun 2000 16:13:56 +0000 From: Claudio Hermida Organization: CMA, IST X-Mailer: Mozilla 4.7 [en] (X11; I; Linux 2.2.12-20 i686) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Re: Adjoints in bicategories References: <20000622124507.EF71C451D@mail.cs.uu.nl> Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Frank Atanassow wrote: > I'm looking for definitions of (the weak 2-dimensional analogues of 1-) > products and coproducts for bicategories, and also adjoints. In his 1967 > article "Introduction to Bicategories, Part I" Benabou promises to treat > biadjoints in a sequel, but I gather this was never published. Gray treats a > notion of "quasi-adjointness" in "Formal Category Theory"; is this accepted as > the "right" generalization? > > Pointers to definitions of these concepts in one of the approaches to weak > n-categories would be welcome as well. Relevant references: Kelly, G. M. Elementary observations on $2$-categorical limits. Bull. Austral. Math. Soc. 39 (1989), no. 2, 301--317. Power, A. J. Coherence for bicategories with finite bilimits. I. Categories in computer science and logic (Boulder, CO, 1987),341--347, Contemp. Math., 92, Amer. Math. Soc., Providence, RI, 1989. Betti, Renato; Power, A. John On local adjointness of distributive bicategories. Boll. Un. Mat. Ital. B (7) 2 (1988), no. 4, 931--947. Bird, G. J.; Kelly, G. M.; Power, A. J.; Street, R. H. Flexible limits for $2$-categories. J. Pure Appl. Algebra 61 (1989), no. 1, 1--27. From rrosebru@mta.ca Fri Jun 23 14:40:12 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id OAA16298 for categories-list; Fri, 23 Jun 2000 14:34:11 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <3.0.6.32.20000622145228.0096e740@pop3.math.ubc.ca> X-Sender: johnm@pop3.math.ubc.ca X-Mailer: QUALCOMM Windows Eudora Light Version 3.0.6 (32) Date: Thu, 22 Jun 2000 14:52:28 -0600 To: categories@mta.ca From: John MacDonald Subject: categories: Re: Adjoints in bicategories In-Reply-To: <20000622124507.EF71C451D@mail.cs.uu.nl> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: In reply to Frank Atanassow's question: Here is a list of a few references I have on hand that are related or somewhat related to your question. This list is not intended to be complete and I hope others will add more references and/or details. John MacDonald, Department of Mathematics University of British Columbia Vancouver, B.C., Canada V5K 1N4 [1] R. Blackwell, G.M.Kelly, J.Power, Two-Dimensional Monad Theory, Sydney Category Seminar Reports 1987. [2] M.C.Bunge, Coherent Extensions and Relational Algebras, Trans. Amer. Math. Soc.197(1974), 355-390. [3] J.W.Gray, Formal Category Theory: Adjointness for 2-Categories, Lecture Notes in Mathematics 391, Springer-Verlag 1974. [4] C.B.Jay, Local Adjunctions, Journal of Pure and Applied Algebra 53(1988), 227-238 [5] G.M.Kelly, Elementary Observations on 2-Categorical Limits, Bull. Austral. Math. Soc. 39(1989), 301-317 [6] G.M.Kelly, R.H.Street, Review of the Elements of 2-Categories, Lecture Notes in Mathematics 420, Springer-Verlag 1974, 75-109. [7] J.L.MacDonald, A.Stone, Soft Adjunction between 2-Categories, Journal of Pure and Applied Algebra 60(1989), 155-203. [8] R.H.Street, The formal Theory of Monads, Journal of Pure and Applied Algebra 2(1972),149-168. At 02:45 PM 6/22/00 +0200, you wrote: >I'm looking for definitions of (the weak 2-dimensional analogues of 1-) >products and coproducts for bicategories, and also adjoints. In his 1967 >article "Introduction to Bicategories, Part I" Benabou promises to treat >biadjoints in a sequel, but I gather this was never published. Gray treats a >notion of "quasi-adjointness" in "Formal Category Theory"; is this accepted as >the "right" generalization? > >Pointers to definitions of these concepts in one of the approaches to weak >n-categories would be welcome as well. > >-- >Frank Atanassow, Dept. of Computer Science, Utrecht University >Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands >Tel +31 (030) 253-1012, Fax +31 (030) 251-3791 > > > > From rrosebru@mta.ca Sat Jun 24 20:14:13 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id UAA02516 for categories-list; Sat, 24 Jun 2000 20:08:11 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Received: from zent.mta.ca (zent.mta.ca [138.73.101.4]) by mailserv.mta.ca (8.9.3/8.9.3) with SMTP id GAA14326 for ; Sat, 24 Jun 2000 06:23:22 -0300 (ADT) X-Received: FROM ipmma27.mate.polimi.it BY zent.mta.ca ; Sat Jun 24 06:18:02 2000 -0300 X-Received: from Betti.mate.polimi.it (renbet.mate.polimi.it [131.175.23.75]) by ipmma27.mate.polimi.it (8.9.3/8.9.3) with SMTP id LAA29507 for ; Sat, 24 Jun 2000 11:16:57 +0200 Message-Id: <3.0.6.32.20000624111853.007d17e0@pop2.mate.polimi.it> X-Sender: renbet@pop2.mate.polimi.it X-Mailer: QUALCOMM Windows Eudora Light Version 3.0.6 (32) Date: Sat, 24 Jun 2000 11:18:53 +0200 To: categories@mta.ca From: Renato Betti Subject: categories: Categorical Studies in Italy Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: Readers of the catnet may be interested in looking at Categorical Studies in Italy the "Supplemento ai Rendiconti del Circolo Matematico di Palermo", serie II, n. 64, 2000, which has recently appeared. This is a collection of 15 papers by various authors connected with Italian category theorists. Most of the papers were presented at a meeting held in Perugia, May 1-3, 1997. The occasion was the 25th anniversary of the course on Category Theory and Topos Theory given in Perugia by Bill Lawvere.(The Rendiconti are available in most libraries.) Renato Betti From rrosebru@mta.ca Mon Jun 26 22:57:10 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id WAA14618 for categories-list; Mon, 26 Jun 2000 22:51:32 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Mon, 26 Jun 2000 07:27:34 -0400 (EDT) From: Peter Freyd Message-Id: <200006261127.e5QBRYC01847@saul.cis.upenn.edu> To: categories@mta.ca Subject: categories: Tony-San Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: On 4 January I posted: The Queen's New Years Honours list announced a knighthood for C.A.R. Hoare (the first person to find an application for 2-categories). Today: The Chronicle of Higher Education Monday, June 26, 2000 Computer Scientist, Biologist, Philosopher Win Kyoto Prizes Japan's Inamori Foundation on Friday named a computer scientist, a biologist, and a philosopher as this year's winners of the Kyoto Prizes, which are awarded annually to honor individuals who contribute to the scientific, cultural, or spiritual betterment of society. The winners will receive a special certificate and 50-million yen (approximately $477,000) at a ceremony in Kyoto on November 10. The winners and their achievements cited by the foundation, are: * Sir Charles Antony Richard Hoare, a professor emeritus of computer science at the University of Oxford, in Britain, for "pioneering and fundamental contributions to software science." * Walter Jacob Gehring, a professor of developmental biology at the University of Basel, in Switzerland, for his "discovery of conserved developmental mechanisms." * Paul Ricoeur, a professor emeritus of philosophy at the University of Paris, in France, and at the University of Chicago, for "an imposing construct of hermeneutic phenomenology that embraces a new concept of ethics." From rrosebru@mta.ca Thu Jun 29 16:26:05 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id QAA05949 for categories-list; Thu, 29 Jun 2000 16:21:08 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: calculemus-ig@dist.unige.it, calculemus-ig@ags.uni-sb.de, om@openmath.org, theorem-provers@ai.mit.edu, fg121@informatik.uni-ulm.de, qed@mcs.anl.gov, isabelle-users@cl.cam.ac.uk, coq@margaux.inria.fr, elf-list@CS.cmu.edu, info-hol@jaguar.cs.byu.edu, categories@mta.ca, formal-methods@cs.uidaho.edu, lics@research.bell-labs.com, logic@theory.lcs.mit.edu, uitp@dcs.gla.ac.uk, bonacina@cs.uiowa.edu Subject: categories: CALCULEMUS-2000 CFP Date: Wed, 28 Jun 2000 15:49:05 +0100 From: Manfred Kerber Message-Id: Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: CALL FOR PARTICIPATION CALCULEMUS-2000 Symposium on the Integration of Symbolic Computation and Mechanized Reasoning 6-7 August 2000 St Andrews, Scotland (collocated with ISSAC 2000) http://www.calculemus.net/meetings/standrews00/ PROGRAMME http://www.calculemus.net/meetings/standrews00/program.html REGISTRATION http://www-history.mcs.st-and.ac.uk/issac2000/registration.shtml SCOPE Both deduction systems and computer algebra systems are receiving growing attention from industry and academia. On the one hand, mathematical software systems have been commercially very successful. Their use is now wide-spread in industry, education, and scientific contexts. On the other hand, the use of formal methods in hardware and software development has made deduction systems indispensable not least because of the complexity and sheer size of the reasoning tasks involved. As many application domains fall outside the scope of existing deduction systems and computer algebra systems, there is still need for improvement and in particular need for the integration of computer algebra and deduction systems. The symposium is intended for researchers and developers interested in combining the reasoning capabilities of deduction systems and the computational power of computer algebra systems. TOPICS Topics of interest for the symposium include all aspects related to the combination of deduction systems and computer algebra systems. We explicitly encourage submissions of results from applications and case studies where such integration results are particularly important. FORMAT The symposium will feature invited talks, contributed presentations with ample time for discussion, and a panel session. Consistent with the tradition of the symposium as a lively forum for discussing controversial ideas, we expect and encourage contributed talks to present work in progress, rather than polished final results. CONFERENCE LOCATION CALCULEMUS 2000 will be held at St Andrews University, Scotland's oldest university. Visitors to St Andrews will discover a city full of charm and historical interest, and golfers will be delighted by the many famous and challenging golf courses in the area. Travel information can be found as http://www-history.mcs.st-and.ac.uk/issac2000/travel.shtml INVITED SPEAKERS - Henk Barendregt, U. Nijmegen, Mathematics and Computer Science - Arjeh Cohen, Eindhoven University of Technology, Dept. Math. - Gaston Gonnet, ETH Z"urich, Institute for Scientific Computation IMPORTANT DATES Symposium: 6-7 August 2000 ISSAC: 7-9 August 2000 13. OpenMath Workshop: 10 August 2000 ORGANIZATION and PROGRAMME CHAIRS Manfred Kerber, U. Birmingham, Michael Kohlhase, U. Saarbr"ucken, LOCAL ORGANIZER Steve Linton, St. Andrews U. PROGRAMME COMMITTEE Alessandro Armando, U. Genova Michael Beeson, San Jose State U. Manuel Bronstein, INRIA Sophia Antipolis Bruno Buchberger, RISC, Linz Jaques Calmet, U. Karlsruhe Olga Caprotti, TU. Eindhoven Edmund Clarke, CMU Fausto Giunchiglia, IRST Therese Hardin, Paris VI John Harrison, Intel Corp. Tudor Jebelean, RISC, Linz Helene Kirchner, Nancy LORIA/INRIA Deepak Kapur, U. New Mexico, Albuquerque Steve Linton, St. Andrews U. Ursula Martin, St. Andrews U. Julian Richardson, U. Edinburgh J"org Siekmann, U. Saarbr"ucken Carolyn Talcott, Stanford U. Andrzej Trybulec, U. Bialystok From rrosebru@mta.ca Fri Jun 30 09:43:30 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA19841 for categories-list; Fri, 30 Jun 2000 09:43:13 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Received: from zent.mta.ca (zent.mta.ca [138.73.101.4]) by mailserv.mta.ca (8.9.3/8.9.3) with SMTP id AAA13411 for ; Fri, 30 Jun 2000 00:56:25 -0300 (ADT) X-Received: FROM macadam.mpce.mq.edu.au BY zent.mta.ca ; Fri Jun 30 00:51:18 2000 -0300 X-Received: from hera.mpce.mq.edu.au (hera.mpce.mq.edu.au [137.111.219.13]) by macadam.mpce.mq.edu.au (8.8.8/8.8.8) with ESMTP id NAA11848 for ; Fri, 30 Jun 2000 13:56:18 +1000 (EST) X-Received: from [137.111.90.96] (grassmann.mpce.mq.edu.au [137.111.90.96]) by hera.mpce.mq.edu.au (8.9.3+Sun/8.9.3) with SMTP id NAA13163 for ; Fri, 30 Jun 2000 13:56:14 +1000 (EST) Date: Fri, 30 Jun 2000 13:56:14 +1000 (EST) Message-Id: <200006300356.NAA13163@hera.mpce.mq.edu.au> X-Sender: mbatanin@hera.mpce.mq.edu.au Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" To: categories@mta.ca From: mbatanin@ics.mq.edu.au (Michael Batanin) Subject: categories: preprint: "On the Penon method of weakening of algebraic structures" Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: Dear colleagues, a preprint M.Batanin, "On the Penon method of weakening of algebraic structures" is available on http://www.math.mq.edu.au/~mbatanin/papers.html I consider a generalization of the Penon approach to the definition of weak $n$-category and compare his definition with mine. I also correct one construction from my earlier paper about computads. Regards, Michael. From rrosebru@mta.ca Fri Jun 30 09:53:49 2000 -0300 Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id JAA16011 for categories-list; Fri, 30 Jun 2000 09:40:23 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: S.J.Vickers@open.ac.uk Message-ID: To: categories@mta.ca Subject: categories: Maps as toposes: terminology? Date: Fri, 30 Jun 2000 10:35:06 +0100 MIME-Version: 1.0 X-Mailer: Internet Mail Service (5.5.2650.21) Content-Type: text/plain; charset="iso-8859-1" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: As is well-known, given a topos Y then the maps f: X -> Y targeted at it are equivalent to toposes in the generalized universe of sets corresponding to Y. Hence there is a correspondence between properties of maps and constructive properties of toposes. Unfortunately, they often have different names. For instance, in "Proper maps of toposes", Moerdijk and Vermeulen have - compact (for toposes) vs. proper (for maps) strongly compact vs. tidy Stone vs. entire compact Hausdorff vs. separated (a.k.a. proper) Furthermore, sometimes f is genuinely to be thought of as a map, with X and Y toposes over some base topos B, and the properties can be relativized to B. For instance, Moerdijk and Vermeulen define "proper relative to B", and then "proper" unqualified means "proper relative to the target (Y)". More names can arise from this; for instance, "proper relative to 1" has been called - at least for locales - "semiproper", "perfect" or even "proper". Does anyone have suggestions of systematic terminology - other than systematically calling everything "proper" - that avoids this proliferation of names? Steve Vickers Department of Pure Maths Faculty of Maths and Computing The Open University ----------- Tel: 01908-653144 Fax: 01908-652140 Web: http://mcs.open.ac.uk/sjv22