From rrosebru@mta.ca Thu Mar 1 14:47:52 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f21I7Rg17252 for categories-list; Thu, 1 Mar 2001 14:07:27 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200103011400.PAA29145@irmast2.u-strasbg.fr> Date: Thu, 1 Mar 2001 15:00:57 +0100 (MET) From: Philippe Gaucher Reply-To: Philippe Gaucher Subject: categories: preprint : The branching nerve of HDA and the Kan condition To: categories@mta.ca MIME-Version: 1.0 Content-Type: TEXT/plain; charset=us-ascii Content-MD5: m5MUpjIZPtWc83D5wO/PZQ== X-Mailer: dtmail 1.3.0 @(#)CDE Version 1.3.5 SunOS 5.7 sun4u sparc Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 1 Title : The branching nerve of HDA and the Kan condition Abstract : We have already seen that in reasonable situations, i.e. when the path $\omega$-category associated to a higher dimensional automata (HDA) is an $\omega$-groupoid, only the globular nerve satisfies the Kan condition. Indeed for the branching and merging nerves, this condition generally does not hold. This drawback is overcome here by introducing two new nerves (the left and right globular nerves) satisfying the Kan condition in any reasonable situation and having conjecturally the same simplicial homology as the branching and merging nerves respectively for any $\omega$-category freely generated by a cubical set. Type : preprint Comment : 22 pages ; any comments are welcome. URLs : http://www-irma.u-strasbg.fr/~gaucher/fibrantcoin.ps.gz http://www-irma.u-strasbg.fr/~gaucher/fibrantcoin.pdf From rrosebru@mta.ca Sat Mar 3 10:52:15 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f23E8bm27049 for categories-list; Sat, 3 Mar 2001 10:08:37 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Subject: categories: TLCA2001 call for participation To: categories@mta.ca Date: Sat, 3 Mar 101 13:54:20 +0100 (MET) X-Mailer: ELM [version 2.4 PL25] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Message-Id: <20010303125420.906DF42881A@elf.ii.uj.edu.pl> From: tlca2001@ii.uj.edu.pl (TLCA Conference 2001) Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 2 || || || \||/ \/ YES ! IT'S TIME TO REGISTER FOR TLCA 2001 ! ******************************************************** * * * TLCA 2001 * * * * 5th International Conference on * * Typed Lambda Calculi and Applications * * May 2 -- 5, 2001 * * Krakow, Poland * * * * http://www.ii.uj.edu.pl/zpi/tlca2001/ * * * ******************************************************** ******************************************************** * * * CALL FOR PARTICIPATION * * * ******************************************************** The Fifth International Conference on Typed Lambda Calculi and Applications (TLCA 2001) will be held in Krakow, Poland from May 2 to 5, 2001. The Conference is organized by Jagiellonian University, Institute of Computer Science in co-operation with Warsaw University, Institute of Informatics. The program will consist of 4 invited and 28 contributed talks. The invited talks are as follows: Martin Hofmann (Edinburgh) --- From bounded arithmetic to memory management Peter Selinger (Stanford) --- Categorical semantics of control Olivier Danvy (Aarhus) --- Aspects of continuations Dag Normann (Oslo) --- Definability of total objects in PCF and related calculi The detailed program is available from the conference Web page. Note that a welcoming reception is planned for May 1st evening. ******************************************************** * * * EARLY REGISTRATION DEADLINE * * * * MARCH 13 * * * ******************************************************** CITY AND VENUE: Krakow, the old capital of Poland, is a must-see for everybody. If you have not been there, don't miss this occasion. If you have, you certainly want to come again. The Jagiellonian University, founded in 1364, is one of the oldest in Europe. Conference sessions will be held in one of the main buildings of the University, Collegium Novum. SCHEDULE: A welcoming reception will be served on May 1st evening in medieval Collegium Maius, where the University Museum is located. On Wednesday, Friday and Saturday there will be morning and afternoon sessions. Thursday afternoon is reserved for (optional) excursions, and only a morning session is planned. Each day begins with an invited talk followed by presentations of contributed papers. REGISTRATION: To register, visit the conference Web page http://www.ii.uj.edu.pl/zpi/tlca2001/ and fill the online registration form. In case of credit card payment you must however send or fax a copy of the registration form, with your handwritten signature, to: Eskapada, Rynek Glowny 27, 31-010 Krakow, Poland fax: (+48 12) 411 39 32 Bank transfers should made to the order of ESKAPADA sp.z o.o. SWIFT CODE: BREX PL PW KRA BRE BANK S.A. O/KRAKOW 11401081-00-541894-PLNCURR01 A copy of the bank transfer should be also sent by fax or mail to the above address. An ASCII registration form is enclosed below. REGISTRATION FEES: Full Time Accompanying Regular Student person Before March 13th: 100 USD 75 USD 50 USD After March 13th: 130 USD 100 USD 65 USD On site: 140 USD 110 USD 75 USD Regular and student fees include admission, coffee breaks, proceedings and other materials, reception and conference dinner. Accompanying person fee does not include Proceedings nor other materials. HOTELS: Participants can choose from a selection of hotels of different standards and prices. Hotel booking will be arranged by Eskapada travel office. The conference registration form includes hotel reservation. It is advisable to book your hotel early. Hotel prices (in USD) are as follows: single double Copernicus: 150 170 Pod Roza: 125 140 Polonia: 70 83 Fortuna Bis: 62 78 Saski: 75 92 University hotels (1) rooms with private bathrooms: 55 74 (2) rooms with shared bathrooms: 47 -- Student's hotel: 30 -- We look forward to see you in Krakow! Organizing Committee (tlca01@ii.uj.edu.pl) --------------------------- * REGISTER NOW! * --------------------------- || || || \||/ \/ ******************************************************** * * * http://www.ii.uj.edu.pl/zpi/tlca2001/ * * * ******************************************************** ----------------------------- cut here ---------------------------------- ******************************************************** * TLCA 2001 --- REGISTRATION FORM * ******************************************************** ================== INFORMATION ABOUT PARTICIPANT ======================= Name:_____________________________ First Name:_____________________________ Affiliation:________________________________________________________________ Postal address:_____________________________________________________________ City and Zip code:_________________________ Country:_______________________ E-mail:_____________________________ Telephone:____________________________ ========================= (I) REGISTRATION FEE ========================= Participant (100/130) ____________ Full time student (75/100) ______________ Accompanying person (50/65) _________ Registration Fee total (I): __________ =========================== (II) ACCOMMODATION =========================== Hotel (check one): Copernicus ___ Pod Roza ___ Polonia ___ Fortuna bis ___ Saski ___ University hotel (1) ___ (2) ___ Piast ___ Room single _____ double _____ Arrival on: _________ Departure on: _________ No. of nights _____________ x price ___________ = Hotel total (II): ________ ================== (III) EXCURSIONS and TRANSFERS ========================== Krakow Sightseeing (May 3rd) ___________ persons x USD 25 = ______________ Auschwitz-Birkenau (May 3rd) ___________ persons x USD 25 = ______________ Wieliczka Salt Mine (May 3rd) ___________ persons x USD 25 = ______________ Airport transfers (USD 12/person): Arrival date/time __________________________________________ for ___ persons Departure date/time ________________________________________ for ___ persons Railway station transfers (USD 6/person): Arrival date/time ___________________________________________ for ___ persons Departure date/time _________________________________________ for ___ persons Transfers _____ x $6 + _____ x $12 = ___________ Total part (III) ___________ ============================================================================= GRAND TOTAL (I+II+III) ________________ USD ===================== PLEASE CHARGE MY CREDIT CARD =========================+ card owner: _______________________ card number: ____________________________ exp. date: ________________ for total amount: ___________________________ USD date: ___________________________ signature: ________________________________ _____________________________________________________________________________ From rrosebru@mta.ca Mon Mar 5 16:06:10 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f25J64110708 for categories-list; Mon, 5 Mar 2001 15:06:04 -0400 (AST) 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.11.1/8.11.1) with SMTP id f1SFhub24234 for ; Wed, 28 Feb 2001 11:43:56 -0400 (AST) X-Received: FROM eo.cms.math.ca BY zent.mta.ca ; Wed Feb 28 11:48:36 2001 -0400 X-Received: (from majordom@localhost) by eo.cms.math.ca (8.9.0/8.9.0) id PAA30283 for cmath-l-out; Wed, 28 Feb 2001 15:42:08 GMT X-Received: from jardine.math.uwo.ca (root@jardine.math.uwo.ca [129.100.75.21]) by eo.cms.math.ca (8.9.0/8.9.0) with ESMTP id KAA30301 for ; Wed, 28 Feb 2001 10:38:26 -0500 (EST) X-Received: from uwo.ca (jardine@localhost [127.0.0.1]) by jardine.math.uwo.ca (8.10.2/8.10.0) with ESMTP id f1SFbdq27054 for ; Wed, 28 Feb 2001 10:37:39 -0500 Message-ID: <3A9D1B43.AB4F6926@uwo.ca> Date: Wed, 28 Feb 2001 10:37:39 -0500 From: Rick Jardine Organization: Math. Dept., Univ. of Western Ontario X-Mailer: Mozilla 4.75 [en] (X11; U; Linux 2.2.17 i686) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: 2nd announcement: meeting at Stanford Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 3 Second Announcement: Conference on Algebraic Topological Methods in Computer Science Department of Mathematics Stanford University July 30 - August 3, 2001 The application of algebraic topological methods in areas related to Computer Science is an emerging field that is of interest to both pure and applied mathematical scientists. The aim of this conference is to describe recent advances, and define the fundamental open problems in the field through a mixture of expository and technical lectures. There will be twenty-one main lectures, on a variety of topics in the area. This meeting has been funded by grants from Hewlett-Packard and the National Science Foundation. The following mathematical scientists have agreed to speak: John Baez (Math, UC Riverside) Marshall Bern (Xerox PARC) Anders Bjorner (Royal Institute of Technology, Stockholm) Tamal Dey (CS, Ohio State) Herbert Edelsbrunner (CS, Duke) David Eppstein (CS, UC Irvine) Michael Freedman (Microsoft) Philippe Gaucher (CNRS, Strasbourg) Eric Goubault (Commissariat a l'Energie Atomique, France) Jean Goubault-Larrecq (ENS Cachan) Marco Grandis (Dip. di Mat., Genova) Jeremy Gunawardena (HP BRIMS) John Harer (Math, Duke) Joel Hass (Math, UC Davis) Maurice Herlihy (CS, Brown) Reinhard Laubenbacher (Math, NMSU) Laszlo Lovasz (Microsoft) Vaughan Pratt (CS, Stanford) Christian Reidys (Los Alamos National Lab) Bernd Sturmfels (Math, UC Berkeley) Noson Yanofsky (CS, Brooklyn College) The organizers for this meeting are: Gunnar Carlsson, gunnar@math.stanford.edu Rick Jardine, jardine@uwo.ca We ask that all participants register for the meeting. The latest information and all registration forms are available at the Stanford Conference Web Site (http://math.stanford.edu/atmcs/index.htm). A limited amount of time at the meeting will be devoted to short talks by conference participants. If you would like to give a short presentation, please send an abstract to gunnar@math.stanford.edu. There will be a volume of proceedings for the conference, to appear in the journal "Homology, Homotopy and Applications", with Gunnar Carlsson as senior editor. Submissions for this volume should be set in LATEX and should be sent to gunnar@math.stanford.edu, to arrive by Friday, August 17. We are interested in expository papers on particular areas of application of topology, as well as research papers. There will be housing for conference participants on the Stanford campus, at the rate of about 50.00 US per night for single accomodation: a reservation form is available at the Stanford Conference Web Site. There are also several hotels in the area - see the Stanford site for a list. Limited financial support may be available for travel and housing: please make your request when registering. From rrosebru@mta.ca Thu Mar 8 23:49:14 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f293BfN27391 for categories-list; Thu, 8 Mar 2001 23:11:41 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Tue, 6 Mar 2001 19:32:33 +0100 From: "Konferencja TLCA'2001" Message-Id: <200103061832.f26IWXY32671@absurd.mimuw.edu.pl> To: categories@mta.ca Subject: categories: TLCA 2001 -- grants for participants Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 4 ******************************************************** * * * TLCA 2001 * * * * 5th International Conference on * * Typed Lambda Calculi and Applications * * May 2 -- 5, 2001 * * Krakow, Poland * * * * http://www.ii.uj.edu.pl/zpi/tlca2001/ * * * * EARLY REGISTRATION DEADLINE: MARCH 13 * * * ******************************************************** ******************************************************** * * * ONR SUPPORT FOR PARTICIPANTS * * * ******************************************************** Due to a grant from the Office of Naval Research, the organizing committee of TLCA 2001 is now able to offer limited support for participants who are otherwise unable to attend the conference due to insufficient funds. Depending on demand, we may be able to cover all or part of registration fees, hotel and subsistence costs. In some cases we may also support travel. Preference will be given to students and participants from Central and Eastern Europe. Applicants should send e-mail to the following address tlca@mimuw.edu.pl explaining what kind of support is being sought. You may also mail or fax your application to Pawel Urzyczyn, Institute of Informatics, Warsaw University, Banacha 2, 02-097 Warszawa, Poland, fax: (48-22) 55-444-00 Deadline for applications: March 26. Late registration fee will not be charged if you apply. Looking forward to see you in Krakow, Organizing Committee From rrosebru@mta.ca Thu Mar 8 23:49:14 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f293DN613627 for categories-list; Thu, 8 Mar 2001 23:13:23 -0400 (AST) 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: Thu, 8 Mar 2001 10:44:25 +1100 To: categories@mta.ca From: Ross Street Subject: categories: Some pdf files Content-Type: text/plain; charset="us-ascii" ; format="flowed" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 5 Dear Categories In the last few weeks I have been having fun pdf-ing lots of files, thanks to my very able graduate student Daniel Steffen who set my Mac up to do this easily. Some of these things are now available from my publications page http://www.maths.mq.edu.au/~street/Publications.html In particular I point to J. Bichon and R. Street, Militaru's D-equation in monoidal categories (February 2001; submitted). http://www.maths.mq.edu.au/~street/D-equn.ps.gz R. Street, Functorial calculus in monoidal bicategories (February 2001; submitted). http://www.maths.mq.edu.au/~street/Extraord.pdf B.J. Day, P. McCrudden and R. Street, Dualizations and antipodes (February 2001; submitted). http://www.maths.mq.edu.au/~street/Antipode.pdf Best wishes, Ross From rrosebru@mta.ca Fri Mar 9 16:13:31 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f29JRgN20604 for categories-list; Fri, 9 Mar 2001 15:27:42 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <006d01c0a5e0$97772880$17050aa3@info.unlp.edu.ar> From: "Marcelo Frias, Prof. Dr." To: Subject: categories: Call for Papers Argentinean Workshop in Theoretical Computer Science Date: Mon, 5 Mar 2001 22:16:20 -0300 MIME-Version: 1.0 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 6 CALL FOR PAPERS 30 JAIIO - WAIT'2001 Argentinian Workshop on Theoretical Computer Science Buenos Aires - Argentina September 10-14, 2001 -------------------------------------------------------------------- Since its foundation in 1997, the Argentinian Workshop on Theoretical Computer Science (WAIT) has become a relevant Latin American forum for the exchange of ideas and views and the presentation of research results in theoretical computer science, including applications to other domains, as e.g. software engineering, combinatorics or symbolic and numeric computation. WAIT 2001, the 5-th workshop in this series, will be held in Buenos Aires, Argentina, September 10-14, 2001, as part of the 30-th Argentinian Conference on Informatics and Operations Research (30 JAIIO). The workshop aims to build a bridge between academic and applied research in order to promote the exchange of ideas and experience from theory and empiry in the the field of computer science and its applications. The meeting includes invited and contributed talks and tutorials. IMPORTANT DATES: Deadline for reception of papers..............................May 13 Notification of acceptance........................................June 25 Deadline for reception of camera-ready versions.....July 16 TOPICS Specific topics of WAIT 2001 include (but not are limited to) : * Logical and algebraic foundations of computer science (logics for computer science, category theory, relation algebras, type theory etc.), * Formal program construction (formal specification of sequential and concurrent programs; analysis, verification and transformation of programs, etc.), * Algorithms and data structures (sequential, parallel, distributed and on-line computing, probabilistic algorithms etc.), * Computational complexity, * Automata theory, * Graph theory, * Symbolic and algebraic computation. Submissions are expected to contain original research results or to report on progress of theory-relevant academic or applied research. Papers will be refereed by international experts. * Research papers must contain previously unpublished results. They will be judged on the base of the originality and importance of their results and of the clarity of their presentation. Authors have to submit an extended abstract of not more than 4 pages or a full paper not more than 12 pages, including figures and references. * Short papers describing ongoing research in theoretical computer science are also welcome. Papers of this category should be of tutorial nature. * Finally there are invited papers describing applications of theoretical results to real-life situations. Papers of this kind should briefly describe a novel use of theory in an applied domain. INVITED SPEAKERS (to be confirmed soon) INSTRUCTIONS FOR AUTHORS: In order to facilitate the dissemination of papers and results, authors are invited to submit their contributions in English. Nevertheless, papers in Spanish or Portuguese are also welcome. Deadline for submission is May 13, 2001. Papers must be submitted electronically in PostScript format (ghostview-readable) to the following e-mail address: wait2001@dc.uba.ar Authors should communicate in a separate e-mail (in ASCII format) the title of the paper togehter with an abstract of ten lines, name and affiliation of all co-authors and their e-mail addresses, phone and FAX numbers. The message should also contain a list of keywords of the paper and should indicate to which of the above category it belongs. In case of an alternative way of sumbission please take first contact with one of the program chairs. The format of the camera-ready version of the accepted papers will be announced with in the letter of acceptance. WORKSHOP CO-CHAIRS: Prof. Marcelo Frias Department of Computer Science University of Buenos Aires Pabellon I - Ciudad Universitaria 1428 - Buenos Aires - ARGENTINA e-mail: mfrias@dc.uba.ar Prof. Joos Heintz Department of Mathematics University of Buenos Aires Pabellon I - Ciudad Universitaria 1428 - Buenos Aires - ARGENTINA e-mail : joos@mate.dm.uba.ar PRELIMINARY PROGRAM COMMITTEE: Gabriel Baum (Universidad Nacional de La Plata, Argentina) Javier Blanco (Universidad Nacional de Cordoba, Argentina) Esteban Feuerstein (Universidad de Buenos Aires) Marcelo Frias (Universidad de Buenos Aires, Argentina) Armando Haeberer (Oblog, Portugal) Hermann Haeusler (Pontificia Universidade Catolica de Rio de Janeiro, Brasil) Joos Heintz (Universidad Nacional de Buenos Aires, Argentina) Roger Maddux (Iowa State University, USA) Tom Maibaum (King=B4s College, UK) Bernhard Moeller (Universitaet Augsburg, Alemania) Gonzalo Navarro (Universidad de Chile, Chile) Alfredo Olivero (Universidad de Buenos Aires) Natarajan Shankar (SRI International, USA) Alvaro Tasistro (Universidad de la Republica, Uruguay) ______________________________ Prof. Dr. Marcelo Frias Department of Computer Science School of Sciences University of Buenos Aires Pabellon I, Ciudad Universitaria, 1428 Buenos Aires Argentina Phone: +54-11-4576-3390/99 Ext.717 FAX: +54-11-4576-3359 From rrosebru@mta.ca Fri Mar 9 16:15:48 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f29JTHR20299 for categories-list; Fri, 9 Mar 2001 15:29:17 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3AA7D8B7.A5069B5D@mcs.le.ac.uk> Date: Thu, 08 Mar 2001 19:08:39 +0000 From: "V. Schmitt" X-Mailer: Mozilla 4.76 [en] (X11; U; Linux 2.2.18 i686) X-Accept-Language: en MIME-Version: 1.0 To: "categories@mta.ca" Subject: categories: Paper Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 7 Dear all, I submitted the following paper a few months ago, Title: ``Applying enriched categories to quasi-uniform spaces'' Abstract: The represention of complete metric spaces of \cite{Law73} by enrichments is extented to quasi-uniform spaces. Moreover quasi-uniformly continuous maps are described as enriched functors. The quasi-uniform space completion is also viewed as a Cauchy-completion. Super monoidal functors are introduced to obtain these results. A 2-category of enrichments over different bases is defined. In this general context the Cauchy-completion is still a universal construction. Law73 is here the paper of F.W.Lawvere: ``Metric spaces, generalized logic and closed categories'' It is accessible on the site http://www.mcs.le.ac.uk/research/publications as the 6th research report of the year 2000. All the best. Vincent Schmitt From rrosebru@mta.ca Fri Mar 9 16:16:00 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f29JSGs23963 for categories-list; Fri, 9 Mar 2001 15:28:16 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Wed, 7 Mar 2001 12:42:47 +0100 (CET) From: Simon Helsen Reply-To: Simon Helsen To: categories@mta.ca Subject: categories: CFP -- JOURNAL OF FUNCTIONAL PROGRAMMING Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=ISO-8859-1 X-MIME-Autoconverted: from 8bit to quoted-printable by avalon.informatik.uni-freiburg.de id MAA10553 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id f27Bgwb31700 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 8 CALL FOR PAPERS SPECIAL ISSUE JOURNAL OF FUNCTIONAL PROGRAMMING: DEPENDENT TYPE THEORY MEETS PROGRAMMING PRACTICE Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types. There are several remedies to this situation. Dependent type systems, which allow the formation of types that explicitly depend on other types or values, are one of the most promising approaches. These systems are well-investigated from a theoretical point of view by logicians and type theorists. For example, dependent types are used in proof assistants to implement various logics and there are sophisticated proof editors for developing programs in a dependently typed language. To the present day, the impact of these developments on practical programming has been small, partially because of the level of sophistication of these systems and of their type checkers. Only recently, there have been efforts to integrate dependent systems into intermediate languages in compilers and programming languages. Additional uses have been identified in high-profile applications such as mobile code security, where terms of a dependently typed lambda calculus to encode safety proofs. A special issue of the Journal of Functional Programming will be devoted to the interplay between dependent type theory and programming practice. We welcome technical contributions in the field, as well as position papers that: - make researchers in programming languages aware of new developments and research directions on the theory side; - point out to theorists practical uses of advanced type systems and urge them to address theoretical problems arising in emerging applications. Authors who are concerned about the appropriateness of a topic are welcome to contact the guest editors. Manuscripts should be unpublished works and not submitted elsewhere. Revised and enhanced versions of papers published in conference proceedings that have not appeared in archival journals are eligible for submission. All submissions will be reviewed according to the usual standards of scholarship and originality. Submissions should be sent to Gilles Barthe (Gilles.Barthe@inria.fr), with a copy to Nasreen Ahmad (nasreen@dcs.gla.ac.uk). Submitted articles should be sent in postscript format preferably gzipped and uuencoded. In addition, please send, as plain text, title, abstract, and contact information. The submission deadline is December 1st, 2001. Guest Editors: o Gilles Barthe, INRIA Sophia-Antipolis, France o Peter Dybjer, Chalmers Tekniska Högskola, Sweden o Peter Thiemann, Universität Freiburg, Germany From rrosebru@mta.ca Sat Mar 10 18:25:53 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2ALetH27509 for categories-list; Sat, 10 Mar 2001 17:40:55 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Sat, 10 Mar 2001 19:33:56 +0100 Message-Id: <200103101833.TAA23615@tosca.dmi.unict.it> From: Vladimiro Sassone To: categories@mta.ca Subject: categories: ConCoord: Concurrency and Coordination Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 9 [[ -- Apologies for multiple copies of this message -- \vs ]] Second Announcement ConCoord International Workshop on Concurrency and Coordination ====================================================== Lipari Island, Italy 6-8 July 2001 A workshop associated to the 13th Lipari School --------------------------------------------------------------------------- Aims and Scope During the last few years, the role of global computing, and in particular of web applications, has become more and more widespread. The emerging programming paradigms require on the one hand mechanisms to support mobility of code and computations, and effective infrastructures to support coordination and control of dynamically loaded software modules. On the other hand, an abstract semantic framework to formalize the model of computation of internet applications is clearly needed. Such a semantic framework may provide the formal basis to discuss and motivate controversial design/implementation issues and to state and certify properties in a rigorous way. Similar aims have been pursued by two Esprit working groups, which recently terminated their activity: CONFER-2 (CONcurrency and Functions: Evaluation and Reduction ) led by Jean-Jacques Lévy (Inria Roquencourt), with technical assistance of Lone Leth and Bent Thomsen (ICL, London); and COORDINA (From COORDINAtion models to applications, ), led by Antonio Porto (DI-FCT/UNL, Lisboa). The goal of the workshop is to review the large range of results achieved by the two working groups and to set the stage for future scientific advances and collaboration. However contributions and participation are encouraged by all those interested in the mentioned topics. --------------------------------------------------------------------------- Location The workshop is associated to the 13th Lipari School for Computer Science Researchers, Lipari, July 1-14, 2001. The Lipari School () is a well established initiative attended every year by about 60 PhD students and researchers from Italy, Europe and the US. In 2001 the school will be dedicated to the foundations of Wide Area Network Programming and will consist of lectures by Martin Abadi, Bell Labs Research, Palo Alto; Luca Cardelli, Microsoft Research, Cambridge, UK; Paolo Ciancarini, University of Bologna; Peter Lee, Carnegie-Mellon University, Pittsburgh; Doug Lea, State University of New York at Oswego; Michael I. Schwartzbach, University of Aarhus; and Jim Waldo, Sun Microsystems, Burlington, Mass. and Harvard University. Lipari is the largest island of the Eolie Archipelago, located north of Sicily, well known for its volcanic activities. It has sceneries of incomparable beauty and contrasting character. It can be easily reached from Milazzo, Palermo, Naples, Messina and Reggio Calabria by ferry or hydrofoil (50 minutes from Milazzo). --------------------------------------------------------------------------- Program The program of the workshop will include invited talks by the lecturers of the Lipari School (and possibly others), and talks presenting submitted contributions. --------------------------------------------------------------------------- Program Committee Farhad Arbab, CWI Jean-Jacques Lévy, Inria Roquencourt Ugo Montanari, University of Pisa (co-chair) Antonio Porto, Universidade Nova De Lisboa Vladimiro Sassone, University of Catania (co-chair) Bjorn Victor, Uppsala University --------------------------------------------------------------------------- Submissions Extended abstracts (of at most 8 pages) should be submitted electronically as uuencoded postscript files at the address . A separate message should also be sent, with a text-only one-page abstract and with mailing addresses (both postal and electronic), telephone number and fax number of the corresponding author. The proceedings will be published in the ENTCS series. To make easier the preparation of the final versions, papers should be formatted using Latex with the ENTCS style (look at for instructions) --------------------------------------------------------------------------- Important Dates Deadline for submission: 9 April 2001. Notification of acceptance: 21 May 2001. Final version due: 11 June 2001. Workshop dates: 6-8 July 2001. --------------------------------------------------------------------------- Registration and Hotel Reservation Due to the high season in Lipari, hotel reservation will be guaranteed only for those registering before May 31. --------------------------------------------------------------------------- Organizers Alfredo Ferro (Catania), Ugo Montanari (Pisa), Vladimiro Sassone (Catania). --------------------------------------------------------------------------- For more information: WWW: EMAIL: =========================================================================== From rrosebru@mta.ca Tue Mar 13 20:31:12 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2DNga119194 for categories-list; Tue, 13 Mar 2001 19:42:36 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Sender: ageron@mail.math.unicaen.fr Message-Id: Mime-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" To: categories@mta.ca From: Pierre Ageron Subject: categories: Apery and categories Date: Tue, 13 Mar 2001 16:39:01 +0100 (CET) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id f2DFdCb04275 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 10 Professor Roger Apéry (1916-1994) spent all of his career at the University of Caen. He is best known for advocating constructive mathematics against bourkakism and for proving that zeta(3) is irrational. What is less known is his enthusiasm about category theory, as an alternative to set theory (to some extent). According to his son, he became a lover of CT at a seminar in Montréal in 1964. If any reader of this list remembers talking with Apéry at that time or later, or knows of any idea he expressed on CT, I would be grateful about any bit of information. Thank you! PIERRE AGERON 1) coordonnees bureau adresse: Departement de mathematiques, Universite de Caen, 14032 Caen Cedex (mon bureau se trouve desormais sur le Campus 2, bat. Sciences 3, piece 322) telephone : 02 31 56 74 67 telecopie : 02 31 56 73 20 adresse electronique : ageron@math.unicaen.fr page personnelle : http://matin.math.unicaen.fr/~ageron/ 2) coordonnees domicile adresse : 28 rue de Formigny 14000 Caen telephone : 02 31 84 39 67 From rrosebru@mta.ca Wed Mar 14 20:17:27 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2ENaXt31356 for categories-list; Wed, 14 Mar 2001 19:36:33 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: gandalf-vm.cs.yale.edu: taha owned process doing -bs Newsgroups: comp.lang.ml,comp.lang.functional,comp.compilers,comp.lang.scheme Date: Tue, 13 Mar 2001 11:39:27 -0500 (EST) From: Walid Taha To: , , , , , , , Subject: categories: CFP: SAIG'01 In-Reply-To: Message-ID: References: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=ISO-8859-1 X-MIME-Autoconverted: from 8bit to quoted-printable by netra.cs.yale.edu id PAA30860 Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id f2DKtgb05017 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 11 CALL FOR PAPERS Semantics, Applications and Implementation of Program Generation (SAIG'01) PLI Workshop, September 6th, 2001. (Deadline: May 20, 2001) http://www.cs.yale.edu/~taha/saig/cfp01.html Program generation has the prospect of being an integral part of a wide range of software development processes. Many recent studies investigate different aspects of program generation systems, including their semantics, their applications, and their implementation. Existing theories and systems address both high-level (source) language and low-level (machine) language generation. A number of programming languages now supports program generation and manipulation, with different goals, implementation techniques, and targeted at different applications. The goal of this workshop is to provide a meeting place for researchers and practitioners interested in this research area, and in program generation in general. Scope: The workshop solicits submissions related to theoretical and practical models and tools for building program generators systems, Examples include: * Semantics, type systems, and implementations for multi-stage languages. * Run-time specialization systems: e.g. compilers, operating systems. * High-level program generation (applications, foundations, environments). * Program synthesis from high-level specifications. * Symbolic computation, linking and explicit substitution, in-lining and macros. Reports on applications of these techniques to real-world problems are especially encouraged, as are submissions that relate ideas and concepts from several of these topics, or bridge the gap between theory and practice. The program committee is happy to advise on the appropriateness of a particular subject. Format: The one-day workshop will contain slots for technical papers (30 minutes) and position papers (20 minutes. Both times include discussion.) In addition, there will be one hour allocated for open discussions at the end of the workshop. Proceedings will be published as an LNCS volume. Invited Speakers: * Krzysztof Czarnecki, University of Ilmenau and Daimler Chrysler * Tim Sheard, Oregon Graduate Institute of Science and Technology * Mitch Wand, Northeastern University Submission Details: Authors are invited to submit papers of at most 5000 words (excluding figures), in postscript format (letter or A4), using the electronic submission form by May 20th, 2001. This deadline is not extensible. Both position and technical papers are welcome. Please indicate at time of submission. Position papers are expected to describe ongoing work, future directions, and/or survey previous results. Technical papers are expected to contain novel results. All papers will be reviewed by the program committee for the above mentioned criteria, in addition to correctness and clarity. Authors will be notified of acceptance by July 17th, 2001. Final version of the papers must be submitted by July 15th, 2001. Program Committee: * Gilles Barthe, INRIA * David Basin, Freiburg * Don Batory, Texas * Robert Glück, DIKU * Nevin Heintze, Bell-Labs * Eugenio Moggi, DISI * Greg Morrisett, Cornell * Flemming Nielson, Aarhus * David Sands, Chalmers * Walid Taha,Yale (PC Chair) From rrosebru@mta.ca Wed Mar 14 20:17:45 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2ENWQM05217 for categories-list; Wed, 14 Mar 2001 19:32:26 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <002f01c0aa78$a6a36f20$897379a5@osherphd> From: "Osher Doctorow" To: Subject: categories: How do Cross-Category Results Relate to Category Theory? - Doctorow Date: Sun, 11 Mar 2001 14:14:31 -0800 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 5.50.4133.2400 X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4133.2400 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 12 From: Osher Doctorow, Ph.D. osher@ix.netcom.com, Sunday March 11, 2001 2:02PM How do cross-category results relate to category theory? In particular, is there a *deeper* theory than category theory which crosses different categories? I ask this question because I have been following the function p1(x,y) = 1 + y - x and its n-dimensional generalization pn(x,y) = 1 + y - Sn/n where Sn = x1 + x2 + ... + xn and where 0 < = y < = xi < = 1 for i = 1, 2, ..., n (although the inequality can be changed to just y < = xi in certain categories) not only across categories but branches of mathematics including probability, mathematical logic, mathematical physics, geometry, number theory, algebra including especially ring and module theory, geometric nonlinear functional analysis, etc. Even p1 alone appears to have remarkable importance across these fields and others (including functional differential and integrodifferential equations). The category object changes, but the function p1 and the inequality remains, and there is even a non-function (which can be made into a function with suitable restrictions) of type y/x --> 1 + y - x which often splits branches of mathematics down the middle with one branch using y/x and the other using 1 + y - x in a generalization of the notion of phase differences (solid versus liquid versus gas versus superfluid versus superconduction types generalized to rare versus common/frequent events, highly influencing or influenced versus low influencing/influenced events, zero curvature versus non-zero curvature events or objects, anomalous versus non-anomalous conditions, etc.). Osher Doctorow Ventura College, etc. From rrosebru@mta.ca Thu Mar 15 09:58:56 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2FCkHN22924 for categories-list; Thu, 15 Mar 2001 08:46:17 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <5.0.2.1.2.20010314233232.00a608f0@mailbox.syr.edu> X-Sender: lglewis@mailbox.syr.edu X-Mailer: QUALCOMM Windows Eudora Version 5.0.2 Date: Wed, 14 Mar 2001 23:55:00 -0500 To: categories@mta.ca From: Gaunce Lewis Subject: categories: question about symmetric monoidal categories Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii"; format=flowed Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 14 I'm looking for a reference for two notions related to symmetric monoidal categories and symmetric monoidal functors. Assume that A and B are symmetric monoidal categories, and denote the product operation on both by \tensor. Assume that L is a lax (symmetric) monoidal functor from A to B. Here are the two closely related notions: 1. Let G be a functor from A to B for which there is a natural transformation L(a_1) \tensor G(a_2) -> G(a_1 tensor a_2) for all a_1, a_2 in A making the obvious diagrams commute (one an associativity diagram and the other a unit diagram). One can think of L as acting on G, or of G as "modular" over L (I'm working in the abelian category context, so it is natural to think in terms of rings and modules). 2. Now suppose that L has a right adjoint R and G has a left adjoint F. Also assume that L is strictly (or is it strongly) monoidal, and that R has the "dual" monoidal structure. There seems to be a natural common source for an action of L on G and of R on F. This source is a natural isomorphism of the form F(L(a) \tensor b) \iso a \tensor F(b) for all a in A and b in B. If the appropriate diagrams commute, then it is easy to derive the actions of L on G and R on F from this isomorphism. What intrigues me most about this situation is the way in which the adjunctions go in the opposite direction. These two situations appear throughout some stuff in algebraic topology that I am working on right now. Is there a reference in the literature where these notions are discussed? Here is a standard (somewhat degenerate) example of this situation. Let h: S -> T be a homomorphism of commutative rings. There is an associated pullback functor from T-Mod to S-mod which plays the role of the functors R and F above. This functor has both left adjoint (playing the role of L) and right adjoint (playing the role of G). The pullback functor R is lax monoidal, and its left adjoint L is strict monoidal. The functor L acts on G, and R = F acts on F via the lax monoidal structure on R. In the examples that show up in my topological research, R and F are distinct, and neither F nor G have monoidal structures. Thanks, Gaunce Lewis From rrosebru@mta.ca Thu Mar 15 16:09:39 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2FJF6w08877 for categories-list; Thu, 15 Mar 2001 15:15:06 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: triples.math.mcgill.ca: barr owned process doing -bs Date: Thu, 15 Mar 2001 10:53:16 -0500 (EST) From: Michael Barr X-Sender: barr@triples.math.mcgill.ca To: Categories list Subject: categories: Warning in diagram Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 15 Under certain circumstances, a perfectly legitimate procedure in diagram.tex will cause a useless warning to appear on the screen when used in latex2e, although not in latex2.09. The way to prevent this rather annoying warning is to add the line \let\@picture@warn\relax to diagram.tex, AFTER the line near the top that says \makeatletter I had been living with this warning for a couple years and I want to thank Richard Wood for having given me the clue necessary to track it down. Michael From rrosebru@mta.ca Fri Mar 16 16:14:35 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2GJHn830946 for categories-list; Fri, 16 Mar 2001 15:17:49 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200103161827.TAA03919@irmast2.u-strasbg.fr> Date: Fri, 16 Mar 2001 19:27:14 +0100 (MET) From: Philippe Gaucher Reply-To: Philippe Gaucher Subject: categories: Call for papers GETCO 2001 To: categories@mta.ca MIME-Version: 1.0 Content-Type: TEXT/plain; charset=ISO-8859-1 Content-MD5: IvHmpvHXfr1VxpK73u+QWw== X-Mailer: dtmail 1.3.0 @(#)CDE Version 1.3.5 SunOS 5.7 sun4u sparc Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from QUOTED-PRINTABLE to 8bit by mailserv.mta.ca id f2GIRJb31011 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 16 3rd workshop on Geometric and Topological Methods in Concurrency GETCO 2001 hosted by Concur 2001, , and Aalborg University Venue: Aalborg University, Denmark Conference dates: CONCUR: August 21-24, 2001 GETCO: August 25, 2001 Call for papers Scope of the workshop The main mathematical disciplines that have been used in computer science are discrete mathematics (especially, graph theory and ordered structures), logics (mostly proof theory for all kinds of logics, classical, intuitionistic, modal etc.) and category theory (cartesian closed categories, topoi etc.). General Topology has also been used for instance in denotational semantics, with relations to ordered structures in particular. Recently, ideas and notions from mainstream "geometric" topology and algebraic topology have entered the scene in Concurrency Theory and Distributed Systems Theory (some of them based on older ideas). They have been applied in particular to problems dealing with coordination of multi-processor and distributed systems (see the historical note ). Among those are techniques borrowed from algebraic and geometric topology: Simplicial techniques have led to new theoretical bounds for coordination problems. Higher dimensional automata have been modelled as cubical complexes with a partial order reflecting the time flows, and their homotopy properties allow to reason about a system's global behaviour. The first workshop on the subject Geometric and Topological Methods in Concurrency Theory has been held in Aalborg, Denmark, in June 1999. GETCO 2000 was organised as a workshop affiliated with CONCUR 2000 at Penn State University.The recent volumes 10 of Math. Struct. in Comp. Science and 39, issue 2, of Electr. Notes Theor. Comp. Science have been devoted to this area. The 3rd workshop in this series will be organised as a satellite to CONCUR 2001 at Aalborg University (Aug.21 - Aug.24). It aims at bringing together researchers from both the mathematical (geometry, topology, algebraic topology etc.) and computer scientific side (concurrency theorists, semanticians, researchers in distributed systems etc.) with an active interest in these or related developments. Topics include (but are not limited to) Semantics, Concurrency Theory, Model-checking, Abstract Interpretation, Fault-tolerant Protocols for Distributed Systems, Geometrical/Topological models, Applications of algebraic topology, Category theory etc. Paper submission The deadline for submission to the workshop is May 20, 2001 (midnight). Submissions may be of two forms: * Short abstracts: up to 4 pages, in format A4, typeset 11 points * Full papers: up to 12 pages, in format A4, typeset 11 points (excluding bibliography and technical appendices) Both forms of submission should include a separate page with the following informations: title, author(s), corresponding author, contact information and a 12-15 lines summary. Simultaneous submission to other conferences or journals is only allowed for short abstracts. Electronic submission is strongly encouraged. The paper or abstract should be sent by e-mail in the form of a postscript file to both the addresses raussen@math.auc.dk and goubault@aigle.saclay.cea.fr. The accompanying page should be sent in a separate email message. If surface mail has to be used, then 3 copies of the paper/abstract should be sent to: Martin Raussen, Dept. of Mathematical Sciences, Aalborg University, Fredrik Bajersvej 7G, DK-9220 Aalborg Øst, Denmark. Publication Accepted papers will be made available in the BRICS Notes series. For full publication -- only full papers -- first contacts have been taken with Electronic Notes in Theoretical Computer Science. Acceptance of papers will be decided upon after the workshop. Registration The registration for GETCO'2001 is made through the registration for Concur'2001 with no extra-charge. Programme Committee (to be completed): * Patrick Cousot, Ecole Normale Superieure, Paris, France * Lisbeth Fajstrup, Aalborg University, Denmark * Eric Goubault, Commissariat à l'Energie Atomique, France * Jeremy Gunawardena, Hewlett-Packard BRIMS, England * Martin Raussen, Aalborg University, Denmark * Vladimiro Sassone, Catania University, Italy Important Dates * Call for Papers: March 13, 2001 * Deadline for submission: May 20, 2001 * Notification of acceptance: July 1, 2001 * Final version due: July 29, 2001 * CONCUR: August 21-August 24, 2001 * GETCO: August 25, 2001 Local Organization * Lisbeth Fajstrup, Aalborg University, Denmark * Eric Goubault, Commissariat à l'Energie Atomique, France * Martin Raussen, Aalborg University, Denmark Contact http://www.math.auc.dk/~raussen/GETCO/getco.html Martin Raussen Department of Mathematics Aalborg University Fredrik Bajersvej 7G DK-9220 Aalborg Øst Denmark Phone: (+45) 96 35 88 55 Fax: (+45) 98 15 81 29 Email: raussen@math.auc.dk From rrosebru@mta.ca Thu Mar 22 22:35:26 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2N29KQ29205 for categories-list; Thu, 22 Mar 2001 22:09:20 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f From: Peter Baumgartner MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Message-ID: <15031.20682.176006.6839@nostromo.uni-koblenz.de> Date: Tue, 20 Mar 2001 13:44:58 +0100 To: Ijcar Publicity Chair Subject: categories: IJCAR 2001 - Deadlines reminder + List of accepted papers X-Mailer: VM 6.90 under 21.1 (patch 14) "Cuyahoga Valley" XEmacs Lucid Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id f2KClsb20531 Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 17 ------------------------------------------------------------ IJCAR 2001 The International Joint Conference on Automated Reasoning http://www.dii.unisi.it/~ijcar/ ------------------------------------------------------------ Contents: 1) About IJCAR 2) Deadlines reminder 3) List of accepted Research Papers 4) List of accepted System Descriptions 1) About IJCAR -------------- The International Joint Conference on Automated Reasoning (IJCAR) is the fusion of three major conferences in Automated Reasoning: CADE (The International Conference on Automated Deduction), TABLEAUX (The International Conference on Automated Reasoning with Analytic Tableaux and Related Methods) and FTP (The International Workshop on First-Order Theorem Proving). These three events will join for the first time at the IJCAR conference in Siena in June 2001. 2) Deadlines reminder --------------------- The submission deadline for research papers and system descriptions has passed. However, submission of short papers and submission to workshops is still open. Short papers submission deadline : April 2, 2001 Workshop submission deadlines: Theory and Application of Quantified Boolean Formulas : March 24, 2001 Verification : March 25, 2001 Future directions in Automated Reasoning : March 29, 2001 Mechanized Reasoning about Languages with Variable Bindings : March 30, 2001 Precise Modelling and Deduction for OO-Software Development : March 31, 2001 Automation of Proof by Mathematical Induction : March 31, 2001 Strategies in Automated Deduction (STRATEGIES 2001) : March 31, 2001 Proof Transformations, Proof Presentations and Complexity of Proofs (PTP-01) : March 31, 2001 Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics : April 1, 2001 Unification (UNIF-2001) : April 15, 2001 For details please visit the IJCAR web page given above. 3) List of accepted Research Papers ----------------------------------- (88 submitted, 37 accepted) Ulrike Sattler, Moshe Y. Vardi The Hybrid mu-Calculus Carsten Lutz NExpTime-complete Description Logics with Concrete Domains R. Pliuskevicius Deduction-based Decision Procedure for a Clausal Miniscoped Fragment of FTL Carsten Lutz, Holger Sturm, Frank Wolter, Michael Zakharyaschev A tableau calculus for temporal description logic: the constant domain case Juergen Giesl, Deepak Kapur Decidable Classes of Inductive Theorems Arnon Avron, Iddo Lev Canonical Propositional Gentzen-Type Systems Aart Middeldorp, Seitaro Yuuki Approximating Dependency Graphs using Tree Automata Techniques Haarslev, Volker, Möller, Ralf, Turhan, Anni-Yasmin Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics Bernard Boigelot, Sébastien Jodogne, Pierre Wolper On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables Haarslev, V., Moeller, R., Wessel, M. The Description Logic ALCNHR Extended with Concrete Domains: A Practically Motivated Approach Gilles Audemard, Laurent Henocque The eXtended Least Number Heuristic Nicolas Peltier A general method for using schematizations in automated deduction Franz Baader, Stephan Tobies The Inverse Method Implements the Automata Approach for Modal Satisfiability Marco Benedetti Conditional Pure Literal Graphs CERRITO Serenella, CIALDEA-MAYER Marta Free-Variable Tableaux for Constant-Domain Quantified Modal Logics with Rigid and Non-Rigid Designation Bernhard Beckert, Steffen Schlager A Sequent Calculus for First-order Dynamic Logic with Trace Modalities Pablo Armelin, David Pym Bunched Logic Programming (Extended Abstract)) W. Reif, G. Schellhorn, A. Thums Flaw Detection in Formal Specification Stefan Szeider NP-Completeness of Refutability by Literal-Once Resolution Xavier Urbain Automated Incremental Termination Proofs for Hierarchically Defined Term Rewriting Systems Sylvie Doutre, Jerome Mengin Preferred Extensions of Argumentation Frameworks: Query Answering and Computation Reiner Haehnle, Neil V. Murray, Erik Rosenthal Ordered Resolution vs. Connection Graph Resolution Andrea Formisano, Eugenio G. Omodeo, Marco Temperini Instructing equational set-reasoning with Otter Martin Giese Incremental Closure of Free Variable Tableaux Hans de Nivelle, Ian Pratt-Hartmann A Resolution-Based Decision Procedure for the Two-Variable fragment with Equality Marko Luther More On Implicit Syntax Kewen Wang A Top-down Procedure for Disjunctive Well-founded Semantics Brigitte Pientka Termination and Reduction Checking for Higher-Order Logic Programs Enrico Giunchiglia, Massimo Maratea, Armando Tacchella, Davide Zambonin Evaluating search heuristics and optimization techniques in propositional satisfiability Jürgen Stuber A Model-based Completeness Proof of Extended Narrowing And Resolution Joshua S. Hodas, Naoyuki Tamura LolliCoP -- A Linear Logic Implementation of a Lean Connection-Method TheoremProver for First-Order Classical Logic Uwe Egly, Stephan Schmitt Deriving Modular Programs from Short Proofs Christopher Lynch, Barbara Morawska Decidability and Complexity of Finitely Closable Linear Equational Theories Uwe Waldmann Superposition and Chaining for Totally Ordered Divisible Abelian Groups(Extended Abstract) Robert Nieuwenhuis, Thomas Hillenbrand, Alexandre Riazanov, Andrei Voronkov On the Evaluation of Indexing Techniques for Theorem Proving Harald Ganzinger, David McAllester Bottum-up deduction with deletion Harald Ganzinger, Robert Nieuwenhuis, Pilar Nivela Context trees 4) List of accepted System Descriptions --------------------------------------- (24 submitted, 19 accepted) Maria Paola Bonacina Combination of distributed search and multi-search in Peers-mcd.d Dominique PASTRE Muscadet 2.3: A Knowledge-based Theorem Prover Based on Natural Deduction Stephan Schmitt, Lori Lorigo, Christoph Kreitz, Alexey Nogin JProver: Integrating Connection-based Theorem Proving into Interactive Proof Assistants Michael Beeson A Second-order Theorem Prover applied to Circumscription Peter F. Patel-Schneider, Roberto Sebastiani A System and Methodology for Generating Random Modal Formulae Haarslev, V., Moeller, R. RACE System Description C. Anger, K. Konczak, Th. Linke NoMoRe: A System for NonMonotonic Reasoning with logic Programs under Answer Set Semantic Jens Happe The ModProf Theorem Prover Stephan Schulz System Abstract: E 0.61 Alessandro Armando, Luca Compagna, Silvio Ranise System Description: RDL---Rewrite and Decision procedure Laboratory Kahlil Hodgson, John Slaney Development of a Semantically Guided Theorem Prover Armin Fiedler P.rex: An Interactive Proof Explainer Reinhold Letz, Gernot Stenz DCTP -- A Disconnection Calculus Theorem Prover -- System Abstract D. Larchey-Wendling, D. Mery, D. Galmiche STRIP: Structural sharing for efficient proof-search Enrico Giunchiglia, Massimo Narizzano, Armando Tacchella QuBE: A system for deciding Quantified Boolean Formulas Satisfiability Joerg Luecke Hilberticus - a Tool Deciding an Elementary Sublanguage of Set Theory Farinas del Cerro, Luis, Fauthoux, David, Gasquet, Olivier, Herzig, Andreas, Longin, Dominique, Massacci, Fabio Lotrec: The Generic Tableau Prover for Modal and Description Logics Jürgen Avenhaus, Bernd Löchner CCE: Testing Ground Joinability Alexandre Riazanov, Andrei Voronkov Vampire 1.1 (system description) -- Peter Baumgartner Tel. (Giessen): +49 641 99-32160 Mail: peter@uni-koblenz.de Tel. (Koblenz): +49 261 287-2777 WWW: http://www.informatik.uni-giessen.de/staff/baumgart/ From rrosebru@mta.ca Thu Mar 22 22:35:33 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2N268L01968 for categories-list; Thu, 22 Mar 2001 22:06:08 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <5351C3F6EB14D211B62D00A0C98F178D026869@compnt.cs.unp.ac.za> From: Yuri Velinov To: "'categories@mta.ca'" Subject: categories: LAST CFP: FORMAL STRUCTURES IN COMPUTER SCIENCE Date: Mon, 19 Mar 2001 11:51:47 +0200 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: X-Keywords: X-UID: 18 LAST CALL FOR PAPERS FORMAL STRUCTURES IN COMPUTER SCIENCE Organized by Y. Velinov, University of Natal Invited Session of the SCI'2001 Conference The Fifth World Multi-Conference on Systemics, Cybernetics and Informatics, Orlando, Florida, USA, July 22--25, 2001 Professor Nagib Callaos, General Chair URL http://www.iiis.org/sci ------------------------- TOPICS OF THE INVITED SESSION: A rich variety of formal models are currently in use in every field of the contemporary information technology. New formal structures are frequently introduced to model real world situations. Old, sometimes almost forgotten, are revived finding new applications. The aim of the present session is, instead of concentrating on a particular approach, to get together researchers from different areas to share ideas, approaches and their practical efficiency. The scope of the session includes set-theoretical, relational, logical or categorical structures. More specific areas like Petri nets or Automata theory are also welcome. SUBMISSION ------------ Potential authors are asked to inform for their intention to submit a paper as soon as possible by sending a short abstract to yuri@cs.unp.ac.za. Potential authors are expected to send the draft of their paper for reviewing before 12 April 2001 in PS (possibly zipped) or PDF format to yuri@cs.unp.ac.za. Instructions for preparing a paper for the session can be found at the conference site. The invited sessions will be published by IIIS (International Institute of Informatics and Systemics) as books with multiple authors. IMPORTANT DATES : ----------------- April, 12, 2001. Deadline for submitting paper drafts. April, 30, 2001. Deadline for acceptations. May, 20, 2001. Deadline for sending the camera-ready papers. From rrosebru@mta.ca Thu Mar 22 22:35:54 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2N2BVU24399 for categories-list; Thu, 22 Mar 2001 22:11:31 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f X-Authentication-Warning: triples.math.mcgill.ca: rags owned process doing -bs Date: Tue, 20 Mar 2001 17:20:45 -0500 (EST) From: "Robert A.G. Seely" To: Categories List Subject: categories: preprint: The logic of linear functors Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 19 We wish to announce the availability of the following paper, at the URL given below. The logic of linear functors by Richard Blute, J.R.B. Cockett, and R.A.G. Seely It has been commonplace to base logics and type theories on categorical doctrines; with this paper we propose a more general paradigm, suggesting that logics and type theories may be based on functorial doctrines. This paradigm is very general - in particular, it subsumes all of usual categorical logic and type theory as degenerate cases. So as to be able to make precise claims, we illustrate this idea with a special case, developing the logic of linear functors with sufficient detail to see that this one doctrine is general enough to deal with basic linear modal logic and with the Abrusci-Ruet mixed non-commutative linear logic. We emphasise the case where the logic is based on a single functor, but it will be clear that one could also base it on a family of functors, which would allow one to deal with process logic as considered by Hennessy and Milner. The paper's abstract is given in full below. The paper may be found at http://www.math.mcgill.ca/rags/linear/lfl.ps.gz> or go to R.A.G. Seely's home page http://www.math.mcgill.ca/rags/ and click on the appropriate link. ......................................................... The logic of linear functors by Richard Blute, J.R.B. Cockett, and R.A.G. Seely ABSTRACT: This paper describes a family of logics whose categorical semantics is based on functors with structure rather than on categories with structure. This allows the consideration of logics which contain possibly distinct logical subsystems whose interactions are mediated by functorial mappings. For example, within one unified framework, we shall be able to handle logics as diverse as modal logic, ordinary linear logic, and the "noncommutative logic" of Abrusci and Ruet, a variant of linear logic which has both commutative and noncommutative connectives. Although this paper will not consider in depth the categorical basis of this approach to logic, preferring instead to emphasize the syntactic novelties that it generates in the logic, we shall focus on the particular case when the logics are based on a linear functor, to give a definite presentation of these ideas. However, it will be clear that this approach to logic has considerable generality. There have been several individual attempts to develop logics with distinct but related subsystems of connectives, such as the Abrusci--Ruet noncommutative logic and the bunch logic of O'Hearn and Pym; generally these are presented in terms of "bunching" the formulas in the sequents of the logics via different "punctuation". The present functor logic, by contrast, uses a system of "formula blocks", which represent the functorial action and which give finer control over what logical features may be displayed. By displaying a family of functor logics, we illustrate how different logical systems can be developed along these lines, logics which are primarily distinguished by the degree to which they permit nesting of formula blocks. Our examples will include a basic logic where there is essentially no nesting, a system of linear modal logic, which allows nesting, but has only one system of connectives, and the Abrusci--Ruet logic, where nesting is virtually unrestricted and there are two subsystems of connectives. We finish by showing how to translate between the ``bunch'' style of logic and our ``formula block'' or functor logic using the Abrusci--Ruet noncommutative logic as an example. ================== R.A.G. Seely From rrosebru@mta.ca Thu Mar 22 22:37:30 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2N2GfF10575 for categories-list; Thu, 22 Mar 2001 22:16:41 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: categories@mta.ca Subject: categories: TACS 2001 -- call for papers Reply-to: bcpierce@cis.upenn.edu Date: Wed, 14 Mar 2001 22:51:06 EST Message-ID: <15122.984628266@saul.cis.upenn.edu> From: "Benjamin C. Pierce" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 20 Call For Papers Fourth International Symposium on Theoretical Aspects of Computer Science (TACS 2001) October 29-31, 2001 Tohoku University, Sendai, Japan http://tacs2001.ito.ecei.tohoku.ac.jp/tacs2001/ The TACS Symposium will focus on the theoretical foundations of programming and their applications. The topics of interest include... Theoretical aspects of the design, semantics, analysis, and implementation of programming languages and systems; logics of programs; calculi and models of concurrency and parallel computation; theories of mobile computation and system security; categories and types in computer science; formalisms, methods, and systems for program specification, verification, synthesis, and optimization; constructive, linear, and modal logics in computer science. The scientific program will consist of invited lectures, contributed talks, and demo sessions. A proceedings containing the full papers of the invited and contributed talks will be published by Springer-Verlag as a volume of Lecture Notes in Computer Science. IMPORTANT DATES Submission deadline: April 1, 2001 Notification to authors: June 15, 2001 Deadline for final versions: July 20, 2001 INVITED SPEAKERS Luca Cardelli Microsoft Research Daniel Jackson Massachusetts Institute of Technology Christine Paulin-Mohring Universite Paris Sud & INRIA Andrew Pitts University of Cambridge Jon Riecke Lucent Technologies Kazunori Ueda Waseda University CONFERENCE CHAIR: Takayasu Ito Tohoku University PROGRAM CO-CHAIRS: Naoki Kobayashi Tokyo Institute of Technology kobayasi@cs.titech.ac.jp Benjamin Pierce University of Pennsylvania bcpierce@cis.upenn.edu PROGRAM COMMITTEE: Zena Ariola University of Oregon Cedric Fournet Microsoft Research Jacques Garrigue Kyoto University Masami Hagiya University of Tokyo Robert Harper Carnegie Mellon University Masahito Hasegawa Kyoto University Nevin Heintze Lucent Technologies Martin Hofmann Edinburgh University Zhenjiang Hu University of Tokyo Naoki Kobayashi Tokyo Institute of Technology Martin Odersky Ecole Polytechnique Federale de Lausanne Catuscia Palamidessi Pennsylvania State University Benjamin Pierce University of Pennsylvania Francois Pottier INRIA Andre Scedrov University of Pennsylvania Natarajan Shankar SRI International Ian Stark Edinburgh University Makoto Tatsuta Kyoto University SUBMISSION INFORMATION Authors are invited to submit full papers (up to 6000 words, including figures and bibliographies). Papers must be unpublished and not submitted for publication elsewhere. Submissions should be in Postscript or PDF format, on A4 or US letter pages. They must be printable on common printers and viewable with ghostview or acroread. The first page of each submission should include the email address, telephone, and fax numbers of the corresponding author. Accepted papers must be presented at the symposium, and the final manuscript must be prepared in the LNCS format. All submissions should be done electronically through the TACS submission page http://saul.cis.upenn.edu:8086/. From rrosebru@mta.ca Fri Mar 23 15:38:15 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2NIqCL09668 for categories-list; Fri, 23 Mar 2001 14:52:12 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 23 Mar 2001 14:05:47 -0400 (AST) From: aurelio.carboni@uninsubria.it To: categories Subject: categories: A. Carboni - eaddress Message-ID: MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 21 >From now on my e-mail address that should be used is aurelio.carboni@uninsubria.it at my official institution, which is Universita' dell'Insubria Dipartimento di Scienze CC, FF e MM Via Valleggio 11 22100 COMO (IT). Thanks, Aurelio. From rrosebru@mta.ca Wed Mar 28 12:41:10 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2SFsx312833 for categories-list; Wed, 28 Mar 2001 11:54:59 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3AC07B68.B1EDF550@it-c.dk> Date: Tue, 27 Mar 2001 13:37:13 +0200 From: rms X-Mailer: Mozilla 4.74 [en] (WinNT; U) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: jobs: Open positions at IT-C Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 22 Regarding open positions at The IT-University of Copenhagen, Via the following URL you will find a detailed description of 13 positions as Associate or Assistant Professor currently open at The IT-University of Copenhagen. http://www.it-c.dk/pub_uk/db_363.html Kind Regards Personnel Department/ The IT-University of Copenhagen From rrosebru@mta.ca Wed Mar 28 12:41:46 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2SFgjd31049 for categories-list; Wed, 28 Mar 2001 11:42:45 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-Id: <200103261723.SAA21097@champit.dcs.ed.ac.uk> To: categories@mta.ca cc: pbj@dcs.ed.ac.uk Subject: categories: PhD studentships at the LFCS, U. of Edinburgh Mime-Version: 1.0 (generated by tm-edit 1.7) Content-Type: text/plain; charset=US-ASCII Date: Mon, 26 Mar 2001 18:23:32 +0100 From: Paul Jackson Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 23 [This announcement has been sent to the categories mail list since much research at the LFCS makes use of category theory. Please pass it on to interested students and colleagues at your university or research institute. Apologies if you receive multiple copies] PhD positions available for October 2001 Laboratory for Foundations of Computer Science Division of Informatics, University of Edinburgh Applications are open for students to take up PhD places at Edinburgh in October 2001. Supporting funds are available for postgraduates of any nationality. The Laboratory for Foundations of Computer Science is one of the world's leading centres of research into theoretical computer science and its application. An important part of this is its active community of research students, currently over 20 strong. LFCS runs a 3-year PhD programme; this includes a series of taught courses which provide a broad background in the theory of computation, and prepare students to do their own research work. All students are directly supervised by an academic staff member. The Laboratory and the Division fund some studentships of their own, open to applicants of any nationality. UK students can also apply for one of several grants awarded to the Division by the EPSRC. For more information, including details of how to apply, please consult our web site. http://www.lfcs.informatics.ed.ac.uk/research/students.html From rrosebru@mta.ca Fri Mar 30 12:28:40 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2UFS5418510 for categories-list; Fri, 30 Mar 2001 11:28:05 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f User-Agent: Microsoft Outlook Express Macintosh Edition - 5.01 (1630) Date: Wed, 28 Mar 2001 15:31:18 -0800 Subject: categories: Looking for adjoints From: Jean-Pierre Marquis To: Message-ID: Mime-version: 1.0 Content-type: text/plain; charset="US-ASCII" Content-transfer-encoding: 7bit Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 24 I would like to have a large pool of examples of adjoint functors in as many different fields of mathematics as possible. I am looking for the "nicest", in whatever sense you can think of this expression (e.g. unexpected, their existence is equivalent to a classical theorem, etc), cases in various fields. References or examples anyone? (Besides the standard ones found in Mac Lane, etc.) Thank you, Jean-Pierre Marquis From rrosebru@mta.ca Fri Mar 30 17:13:52 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2UKj0Z20970 for categories-list; Fri, 30 Mar 2001 16:45:00 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Date: Fri, 30 Mar 2001 18:16:40 +0100 From: Paul Taylor Message-Id: <200103301716.SAA17727@koi-pc.dcs.qmw.ac.uk> To: categories@mta.ca, Jean-Pierre.Marquis@UMontreal.CA Subject: categories: Re: Looking for adjoints Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 25 > I would like to have a large pool of examples of adjoint functors See "Practical Foundations of Mathematics" (Cambridge University Press, 1999), especially Section 7.1. Paul From rrosebru@mta.ca Fri Mar 30 17:18:56 2001 -0400 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f2UKiS617200 for categories-list; Fri, 30 Mar 2001 16:44:28 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f To: categories@mta.ca Subject: categories: TACS 2001 -- extended deadline Reply-to: bcpierce@cis.upenn.edu Date: Fri, 30 Mar 2001 10:38:01 EST Message-ID: <702.985966681@saul.cis.upenn.edu> From: "Benjamin C. Pierce" Sender: cat-dist@mta.ca Precedence: bulk Status: O X-Status: X-Keywords: X-UID: 26 In response to a large number of requests, the submission deadline for TACS has been extended to April 15th. Authors intending to submit during this grace period are requested to email the title and abstract of their paper before the original deadline (April 1st) to bcpierce@cis.upenn.edu. Call For Papers Fourth International Symposium on Theoretical Aspects of Computer Science (TACS 2001) October 29-31, 2001 Tohoku University, Sendai, Japan http://tacs2001.ito.ecei.tohoku.ac.jp/tacs2001/ The TACS Symposium will focus on the theoretical foundations of programming and their applications. The topics of interest include... Theoretical aspects of the design, semantics, analysis, and implementation of programming languages and systems; logics of programs; calculi and models of concurrency and parallel computation; theories of mobile computation and system security; categories and types in computer science; formalisms, methods, and systems for program specification, verification, synthesis, and optimization; constructive, linear, and modal logics in computer science. The scientific program will consist of invited lectures, contributed talks, and demo sessions. A proceedings containing the full papers of the invited and contributed talks will be published by Springer-Verlag as a volume of Lecture Notes in Computer Science. IMPORTANT DATES Submission deadline: April 15, 2001 Notification to authors: June 20, 2001 Deadline for final versions: July 23, 2001 INVITED SPEAKERS Luca Cardelli Microsoft Research Daniel Jackson Massachusetts Institute of Technology Christine Paulin-Mohring Universite Paris Sud & INRIA Andrew Pitts University of Cambridge Jon Riecke Lucent Technologies Kazunori Ueda Waseda University CONFERENCE CHAIR: Takayasu Ito Tohoku University PROGRAM CO-CHAIRS: Naoki Kobayashi Tokyo Institute of Technology kobayasi@cs.titech.ac.jp Benjamin Pierce University of Pennsylvania bcpierce@cis.upenn.edu PROGRAM COMMITTEE: Zena Ariola University of Oregon Cedric Fournet Microsoft Research Jacques Garrigue Kyoto University Masami Hagiya University of Tokyo Robert Harper Carnegie Mellon University Masahito Hasegawa Kyoto University Nevin Heintze Lucent Technologies Martin Hofmann Edinburgh University Zhenjiang Hu University of Tokyo Naoki Kobayashi Tokyo Institute of Technology Martin Odersky Ecole Polytechnique Federale de Lausanne Catuscia Palamidessi Pennsylvania State University Benjamin Pierce University of Pennsylvania Francois Pottier INRIA Andre Scedrov University of Pennsylvania Natarajan Shankar SRI International Ian Stark Edinburgh University Makoto Tatsuta Kyoto University SUBMISSION INFORMATION Authors are invited to submit full papers (up to 6000 words, including figures and bibliographies). Papers must be unpublished and not submitted for publication elsewhere. Submissions should be in Postscript or PDF format, on A4 or US letter pages. They must be printable on common printers and viewable with ghostview or acroread. The first page of each submission should include the email address, telephone, and fax numbers of the corresponding author. Accepted papers must be presented at the symposium, and the final manuscript must be prepared in the LNCS format. All submissions should be made electronically through the TACS submission page http://saul.cis.upenn.edu:8086/. From rrosebru@mta.ca Sun Apr 1 17:59:54 2001 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f31KBiY15490 for categories-list; Sun, 1 Apr 2001 17:11:44 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <004c01c0b98d$173d6240$218d6c18@ivideon.com> From: "Derek Ross" To: References: <200103301716.SAA17727@koi-pc.dcs.qmw.ac.uk> Subject: categories: Re: Looking for adjoints Date: Fri, 30 Mar 2001 18:48:39 -0800 MIME-Version: 1.0 Content-Type: text/plain; charset="Windows-1252" Content-Transfer-Encoding: 7bit X-Priority: 3 X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook Express 5.50.4522.1200 X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4522.1200 Sender: cat-dist@mta.ca Precedence: bulk Status: RO X-Status: X-Keywords: X-UID: 27 Excerpts from that book may also be found online at: http://www.dcs.qmw.ac.uk/~pt/Practical_Foundations/html/c7.html Derek. > > I would like to have a large pool of examples of adjoint functors > > See "Practical Foundations of Mathematics" (Cambridge University Press, 1999), > especially Section 7.1. > > Paul > From rrosebru@mta.ca Sun Apr 1 17:59:55 2001 -0300 Return-Path: Received: (from Majordom@localhost) by mailserv.mta.ca (8.11.1/8.11.1) id f31KDSC17023 for categories-list; Sun, 1 Apr 2001 17:13:28 -0300 (ADT) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Message-ID: <3AC60091.2F3C919F@ip.osgf.ge> Date: Sat, 31 Mar 2001 20:06:42 +0400 From: Irakli Tskhvedadze Reply-To: asrios@ip.osgf.ge Organization: ASRIOS X-Mailer: Mozilla 4.5 [en] (Win98; I) X-Accept-Language: en MIME-Version: 1.0 To: categories@mta.ca Subject: categories: Co-operation with ASRIOS-Georgia Content-Type: text/plain; charset=iso-8859-1 X-MIME-Autoconverted: from 8bit to quoted-printable by kolibri.osgf.ge id f2VEuDj01471 Sender: cat-dist@mta.ca Precedence: bulk Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by mailserv.mta.ca id f31KDSC17023 Status: RO X-Status: X-Keywords: X-UID: 28 Dear Sir/Madam , Georgian Association of System Reforms and Informatization of Organizational Structures (ASRIOS) intends to find partners, carrying out Mathematical Structures in Computer Science, on close cooperation based on conceptual project “Research to the Development of Dynamic Database Structure based on Mathematical Models” with possible funding support. ASRIOS conducts development of methodology of construction of information complexes on the basis of their unification based on Categorial Analysis, Petri Nets, Mathematical Lattice etc. If you take an interest in the given proposal, your recommendations for further interaction will be desirable. To learn more about ASRIOS activity, please visit web-site http://www.asrios.ge Thank you in advance, Sincerely, Irakli Tskhvedadze Vice-President of the Association of System Reforms and Informatization of Organizational Structures **************************************************** Association of System Reforms and Informatization of Organizational Structures(ASRIOS) Address: Georgia, 380071 Tbilisi, Gamsachurdia ave.10, apt.1 Web: http://www.asrios.ge E-mail: asrios@ip.osgf.ge asrios@parliament.ge Tel: +995 32 389710 +995 32 397926 *********************************************************