May 1999 - Categories - categories.org.au

Re: Recursive types in polymorphic lambda calculus
by Philip Wadler 01 Jun '99

01 Jun '99

Thanks to all for the responses to my question, and sorry for the delay in summarising the replies. The concensus seems to be that Reynolds (83) and Bohm-Berarducci (85) understood the concept, and that Reynolds-Plotkin (preprint in 88) spelled out the categorical construction, with many other pieces of related work. -- P ======================================================================== The question: ======================================================================== To: types(a)cis.upenn.edu, categories(a)mta.ca Subject: categories: Recursive types in polymorphic lambda calculus Date: Fri, 14 May 1999 15:24:32 -0400 From: Philip Wadler <wadler(a)research.bell-labs.com> There is a fairly standard encoding of recursive types into polymorphic lambda calculus, given by rec X.F[X] = all X.(F[X] -> X) -> X where F[X] is a type in which the type variable X appears only covariantly. Recall that every covariant type corresponds to a covariant functor, so for every h:X->Y we have F[h]:F[X]->F[Y]. If we abbreviate T = rec X.F[X], then the key functions on this type are given by the polymorphic lambda terms: fold : all X.(F[X] -> X) -> T -> X fold = Lam X.lam k:F[X]->X.lam t:T.t{X}(k) in : F[T] -> T in = lam u:F[T].Lam X.lam k:F[X]->X.k(F[fold{X}(k)](u)) out : T -> F[T] out = fold{F[T]}(F[in]) Questions: Who first had this insight? Where is a good place to find this spelled out in the literature? Please send results to me, and I will summarize them for the list. Cheers, -- P ======================================================================== The answers: ======================================================================== Date: Sat, 15 May 1999 23:40:29 -0400 From: "P. Scott" <scpsg(a)matrix.cc.uottawa.ca> To: wadler(a)research.bell-labs.com Subject: Re: Recursive types in polymorphic lambda calculus Cc: scpsg(a)matrix.cc.uottawa.ca Dear Phil: I can give you a bit of the history of the functorial type approach, as far as I know it. I will start with recent history, then mention a few ancient tidbits. RECENT HISTORY Syntactically, the fact that for any multisorted finitary algebraic signature, that the elements of initial algebras can be represented by closed normal terms of polymorphic type is well-known. It is implicit in Girard's Phd thesis (by Curry-Howard), and explicit in Reynolds 1983 paper "Types, abstraction, and parametric polymorphism", as well as in Bohm-Berarducci "Automatic synthesis of typed \Lambda-programs on term algebras, TCS 39 (1985), 135-154. More recently, of course, one can look at Girard-Lafont-Taylor, Section 11.5, and also the interesting discussion in John Mitchell's Foundations for Programming Languages, MIT Press, 1996, Section 9.3. Categorically, the first place I saw the functorial approach published in detail--and the fact that in System F, \forall p [ T(p) ==> p ==> p ] is a weakly initial T-algebra (for definable covariant functors T) is in Reynolds-Plotkin "On Functors Expressible in the Polymorphic Typed Lambda Calculus (Inf. & Computation, 1993, reprinted in "Logical Foundations of Functional Programming", edited by G. Huet, Addison-Wesley, 1990). The second place where this is done in detail is the paper "Functorial Polymorphism", by Bainbridge, Freyd, Scedrov, and me (TCS 70 (1990), Subsection 4.9 of "Reynolds' Parametricity". A closely related work to the above is by R. Hasegawa, "Categorical data types in parametric polymorphism, MSCS 4, 1994, pp. 71-109. A basic categorical reference for some of this is Roy Crole's book "Categories for Types", CUP, Chapter 5. More advanced remarks on formal category theory are also in John Mitchell's book, Section 9.3, loc. cit. Finally, I can recommend a few papers on related material: Abadi, Cardelli, Curien "Formal parametric polymorphism, TCS 121 (1993), pp. 9-58, Plotkin & Abadi, "A logic for parametric polymorphism" TLCA'93, SLNCS 664, 1993, pp. 361-375 R. Hasegawa, A logical aspect of parametric polymorphism, CSL'95, SLNCS 1092, 1995. PRE-HISTORY: It's been known since Russell that in higher-order logic (using quantification over propositional and higher-type variables) that we can define various propositional connectives, and can even form a version of type theory based on equality. For example, in Lambek-Scott, our treatment of Full Impredicative Intuitionistic Type Theory (e.g. Part II, Chap. 1, p. 129) and type theory based on Equality (Part II, Chap. 2, p. 133) were inspired not only by Prawitz's 1965 book (Natural Deduction) but some formulas were literally taken from Russell's 1908 article. If you then add Curry-Howard to the mixture, assigning proof terms to the formulas involved, one essentially moves into the modern realm of data types above. Cheers, Phil Scott ======================================================================== From: Daniel Leivant <leivant(a)cs.indiana.edu> Subject: Re: Recursive types in polymorphic lambda calculus To: wadler(a)research.bell-labs.com (Philip Wadler) Date: Sat, 15 May 1999 10:31:06 -0500 (EST) Certainly the basic ideas have been known (for inductive definitions of sets) by mathematical loogicians for many years before the second order lambda calculus was invented. I am sure Kleene had a big role here. I can vouch on the fly for the exact pedigree, but a good reference for tracking things down is probably Moschovakis's 1974 monograph "elementary indcution on abstact structures" For the lambda calculus I am not sure who was first, but I did things independently from scratch in my paper "contracting proofs to programs" in odifreddi volume "logic and computer science", academic press 1990. See in particular chapter 6, but also chapters 5 and 3. I hope this useful. let me know if I can help otherwise. I hope you have my paper above, if not i'll email you a source and/or hard copy. best wishes -- Daniel ======================================================================== To: Philip Wadler <wadler(a)research.bell-labs.com> Subject: Re: Recursive types in polymorphic lambda calculus Date: Sat, 15 May 1999 17:25:37 -0400 From: Jon Riecke <riecke(a)research.bell-labs.com> I'm not exactly sure to whom this is due, but my impression was that it went back a long way. Also, isn't parametricity required to prove that the encoding yields an initial algebra? There's some more recent work of Plotkin's that others might not be aware of: if one takes *linear* polymorphic lambda calculus with term recursion, plus some modest axioms for parametricity, one can code up recursive types whose type variable appears with any variance (covariant, contravariant, or mixed variance). I can dig up precise references to his talks on the subject. -Jon ======================================================================== From: "John C Mitchell" <mitchell(a)cs.stanford.edu> To: "Philip Wadler" <wadler(a)research.bell-labs.com> Subject: RE: categories: Recursive types in polymorphic lambda calculus I think this is Reynolds and Plotkin, the first incarnation of the idea coming from Reynolds. I remember looking into this when I was a graduate student, but I think it was their idea first. The idea comes from category theory, or Smyth-Plotkin approach, most specifically -- the obvious type for an initial F-algebra is All t. (F(t) -> t) -> t. John ======================================================================== To: Philip Wadler <wadler(a)research.bell-labs.com> cc: Andrew.Pitts(a)cl.cam.ac.uk Subject: Re: Recursive types in polymorphic lambda calculus Date: Mon, 17 May 1999 09:02:39 +0100 From: Andrew Pitts <Andrew.Pitts(a)cl.cam.ac.uk> I think the best place in the literature to look is @Article{ReynoldsJC:funept, author = {J.~C.~Reynolds and G.~D.~Plotkin}, title = {On Functors Expressible in the Polymorphic Typed Lambda Calculus}, journal = {Information and Computation}, year = 1993, volume = 105, pages = {1--29} } There is some discussion of the origin of the encoding at the beginning of this paper. I guess special cases of it were known to Girard (he covers some in Proofs and Types, without history of course). The case of algebraic signatures (ie T a sum of products) was worked out in full generality in Bohm & Berarducci (TCS 39(1985)135--154), although the Reynolds-Plotkin paper also refers to a paper by Leivant in 24th FOCS (1983) for this case. However, the general case of a definable covariant functor T seems to be down to Reynolds-Plotkin. I've taken to referring to this general case as the "Reynolds-Plotkin" lemma when I refer to it in lectures. One important question is what properties tyhe encoding has. Up to beta conversion, rec X.F[X] = all X.(F[X] -> X) -> X gives a weak initial algebra for F. In the presence of relational parametricity properties, one can deduce that it is actually initial. Which brings me to the final place in the literature to look for material on this topic: @inproceedings{PlotkinGD:logpp, author = {G.~D.~Plotkin and M.~Abadi}, title = {A Logic for Parametric Polymorphism}, booktitle = {Typed Lambda Calculus and Applications}, editor = {M.~Bezem and J.~F.~Groote}, volume = 664, series = {Lecture Notes in Computer Science}, year = 1993, publisher = {Springer-Verlag, Berlin}, pages = {361--375}, } Best wishes, Andy ======================================================================== Date: Mon, 17 May 1999 11:03:10 +0200 From: Giuseppe Rosolini <rosolini(a)disi.unige.it> To: Philip Wadler <wadler(a)research.bell-labs.com> CC: Edmund Robinson <E.P.Robinson(a)dcs.qmw.ac.uk> Subject: Re: categories: Recursive types in polymorphic lambda calculus Dear Phil, in a paper at LICS 5, Edumnd Robinson and I use an adaptation of the usual argument you quote. We assumed that it came from the original work of Reynolds and Plotkin on non-existence of set-theoretic models for polymorphic lambda calculus. Hope this is useful. Ciao Pino @article {MR94h:03036, AUTHOR = {Reynolds, John C. and Plotkin, Gordon D.}, TITLE = {On functors expressible in the polymorphic typed lambda calculus}, JOURNAL = {Inform. and Comput.}, FJOURNAL = {Information and Computation}, VOLUME = {105}, YEAR = {1993}, NUMBER = {1}, PAGES = {1--29}, ISSN = {0890-5401}, } @incollection {MR86e:03016, AUTHOR = {Reynolds, John C.}, TITLE = {Polymorphism is not set-theoretic}, BOOKTITLE = {Semantics of data types (Valbonne, 1984)}, PAGES = {145--156}, PUBLISHER = {Springer}, ADDRESS = {Berlin}, YEAR = {1984}, } @incollection {MR1099156, AUTHOR = {Robinson, Edmund and Rosolini, Giuseppe}, TITLE = {Polymorphism, set theory, and call-by-value}, BOOKTITLE = {Fifth Annual IEEE Symposium on Logic in Computer Science (Philadelphia, PA, 1990)}, PAGES = {12--18}, PUBLISHER = {IEEE Comput. Soc. Press}, ADDRESS = {Los Alamitos, CA}, YEAR = {1990}, } ======================================================================== From: Mitchell Wand <wand(a)ccs.neu.edu> Date: Mon, 17 May 1999 09:37:40 -0400 (EDT) To: Philip Wadler <wadler(a)research.bell-labs.com> Subject: Recursive types in polymorphic lambda calculus Are you thinking of the Bohm-Berarducci coding? The Bohm-Berarducci coding types the integers rec X. (1 + X) as all X. (X->X) -> (X -> X) which is not far from all X. ((1 + X) -> X) -> X , depending on how you want to treat + . I usually cite Girard-Lafont-Taylor for this. --Mitch ======================================================================== From: Nick Benton <nick(a)microsoft.com> To: "'Philip Wadler'" <wadler(a)research.bell-labs.com> Subject: RE: categories: Recursive types in polymorphic lambda calculus Date: Mon, 17 May 1999 09:03:32 -0700 I'd say algebraic or inductive rather then recursive in this context. (Though of course, there's a coalgebraic version too, but recursive seems to imply mixed-variance) I think the usual references for the fact that one can construct weakly initial algebras for expressible functors are: C. Bohm and A. Berarducci. Automatic synthesis of typed \Lambda-programs on term algebras. TCS 39 (1985) D. Leivant. Reasoning about functional programs and complexity classes associated with type disciplines. FOCS 24 (1983) G. Takeuti. Proof Theory. North-Holland studies in logic and the foundations of mathematics. (1975) The construction is explained in Proofs and Types (Girard Lafont Taylor, CUP 1989) Chapter 11. The construction gives strongly initial algebras if the calculus satisfies some parametricity theorems. I think I first saw the coalgebraic version in something by Gavin Wraith, but I seem to have misplaced the reference. Nick ======================================================================== From: Robert Harper <Robert.Harper(a)cs.cmu.edu> To: "'Philip Wadler'" <wadler(a)research.bell-labs.com> Subject: RE: categories: Recursive types in polymorphic lambda calculus Date: Mon, 17 May 1999 13:46:55 -0400 Hi Phil: I don't know who discovered this, but certainly Reynolds exploited it in his paper (eventually with Plotkin) "Polymorphism is not Set-Theoretic". There he uses F[X] = (X -> 2) -> 2, where X occurs doubly negatively, hence positively (but not strictly positively). The argument is essentially Cantor's diagonal argument, once you get down to it. The crux of the issue is that the syntax provides only weakly initial algebras for definable functors (no uniqueness condition on the mediating morphism), whereas a set model gives initial algebras, hence we'd have a set isomorphic to its double powerset, which is impossible. The key is that Set has enough equalizers to turn any weakly initial algebra into an initial algebra; models like Cpo have essentially no equalizers, so they form a valid model. Bob ======================================================================== Date: Mon, 17 May 1999 18:15:57 +0200 From: Pawel Urzyczyn <urzy(a)mimuw.edu.pl> To: wadler(a)research.bell-labs.com Subject: Re: Recursive types in polymorphic lambda calculus Cc: urzy(a)absurd.mimuw.edu.pl, zs(a)pwr.wroc.pl Dear Philip, As far as I know, representation in \2 of inductive data types (least fixpoints of monotonic operators) like natural numbers or lists dates back to the paper of Bohm and Berarducci in TCS 1985. A generic translation similar to the one you mention in your types message was probably first given in H.~Geuvers. Inductive and coinductive types with iteration and recursion. In {\em Proceedings of the Workshop on Types for Proofs and Programs}, B{\aa}stad, Sweden, 1992, 193--217. but to my understanding it is implicitly present in Leivant, D., Contracting proofs to programs, in: {\it Logic in Computer Science\/} (P.~Odifreddi, ed.), Academic Press, 1990, pp. 279--327. Let me point out however that there are various definitions of inductive and recursive types and it is not the case that all these are equivalent. In general the systems with "iterators" can be defined within system F, while those with "recursors" can not. A discussion of these issues is given in the PhD Thesis of Zdzislaw Splawski: Sp\l awski, Z., {\it Proof-Theoretic Approach to Inductive Definitions in ML-like Programming Language versus Second-Order Lambda Calculus\/}, PhD Thesis, Wroc\l aw University, 1993. The following paper contains the main results about translatability between various systems with inductive types, including the new result that recursors cannot be implemented within system F by means of beta reduction. It should be made available in a few weeks (we will post an anouncements on types when it is ready). Splawski, Z., Urzyczyn, P., Type Fixpoints: Iteration versus Recursion, to appear in Proc. 4th ICFP, Paris, France, September 1999. Sincerely yours, Pawel Urzyczyn ======================================================================== Date: Mon, 17 May 1999 23:35:27 +0200 From: Bernhard Reus <reus(a)informatik.uni-muenchen.de> To: Philip Wadler <wadler(a)research.bell-labs.com> Subject: Re: categories: Recursive types in polymorphic lambda calculus Dear Phil, Well, in fact this is not quite the recursive type you "really" want since you cannot prove uniqueness of elimination. You just have a weakly initial solution of your domain equation F(X) = X. So you must e.g. add an induction principle if you want to prove something. In a dependently typed calculus (CoC) with an impredicative universe you could even express the *initial* solution. Categorically, this goes back to FAFT and the "solution set condition" where the existence of a left adjoint is related to the existence of initial objects. If the category of discourse is locally small and internally complete, then the category has an initial object: I = { x \in W | forall h \in Hom(W,W). h(p) = p } where W is the weakly initial object constructed as T above and "all" ranges over the set of objects of the category. (this is e.g. discussed in Crole's book "Categories for Types", if I remember correctly, and maybe there one can find more references.) Type theoretically speaking, you can find the encoding already in Girard et al.'s "Proofs and Types". Just with the difference that maps k : F(X)->X are spelled out for concrete examples of F. "Fold" is called "It" there and "in" is again given in form of several constructors depending on the concrete form of F. "Out" is obviously a simple application of "fold" and was not treated there. I'm not sure that this really is what you are searching for, so if not -- e.g. if you want to find a reference with "exactly" the formulation you mentioned --, please accept my excuses. Regards, Bernhard ======================================================================== Philip Wadler wadler(a)research.bell-labs.com Bell Labs, Lucent Technologies http://www.cs.bell-labs.com/~wadler 600 Mountain Ave, room 2T-402 office: +1 908 582 4004 Murray Hill, NJ 07974-0636 fax: +1 908 582 5857 USA home: +1 908 626 9252 ----------------------------------------------------------------------- "Verbosity leads to unclear, inarticulate things." --Dan Quayle -----------------------------------------------------------------------

1 0

LUATCS'99 2nd announcement
by Peter Jipsen 25 May '99

25 May '99

Dear Colleagues and Students, Apologies if you receive more than one copy of this message. Included below is the second announcement for the LUATCS Summer School and Workshop, as well as a registration form. The same information can also be obtained from the LUATCS webpage at http://proof.mth.uct.ac.za/~pjipsen/luatcs99 We hope you are interested in this event and also make this information known to your friends and students. Regards Val Goranko and Peter Jipsen %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% FIRST SOUTHERN AFRICAN SUMMER SCHOOL AND WORKSHOP ON LOGIC, UNIVERSAL ALGEBRA, AND THEORETICAL COMPUTER SCIENCE (LUATCS'99) Rand Afrikaans University, Johannesburg, South Africa December 1-10, 1999 SECOND ANNOUNCEMENT AND CALL FOR PARTICIPATION LUATCS'99 is organized under the auspices of the Department of Mathematics at the Rand Afrikaans University (RAU) in Johannesburg, South Africa, the National Research Foundation of South Africa (NRF), the Laboratory for Formal Aspects and Complexity in Computer Science (FACCS-Lab) at the University of Cape Town, and the Interest Group in Logic, Universal Algebra and Theoretical Computer Science at the South African Mathematical Society (SAMS). ADVISORY BOARD: Samson Abramsky (University of Edinburgh, UK) Hajnal Andreka (Math. Inst. of the Hungarian Acad. of Sciences) Johan van Benthem, Chair (University of Amsterdam, Netherlands) Chris Brink (University of Wollongong, Australia) Robin Hirsch (University College London, UK) Wilfrid Hodges (Queen Mary and Westfield College, UK) Bjarni Jonsson (Vanderbilt University, USA) Istvan Nemeti (Math. Inst. of the Hungarian Acad. of Sciences) Jeff Zucker (McMaster University, Canada) ORGANIZING COMMITTEE: Isabella Burger (Rand Afrikaans University, local arrangements), Val Goranko (Rand Afrikaans University, co-chair), Peter Jipsen (University of Cape Town, co-chair). I. ACTIVITIES: Short introductory and advanced courses, tutorials and workshops on each of the three subjects: Logic, Universal Algebra and Theoretical Computer Science, as well as combined courses and tutorials/workshops on specific topics within the scope of the school. Also, there will be open sessions with contributed talks. The courses and tutorials will be given by invited lecturers and will be grouped in two parts: introductory and advanced. The purpose of the single-subject courses is to give a concise introduction into the basics, and some advanced topics of the subject for participants with little or no background (for the introductory courses) and with basic knowledge (for the advanced courses) in the subject. The purpose of the interdisciplinary courses, tutorials, and workshops is to discuss the interaction between the subjects of the school. A general purpose of the school is to reflect the current development of each of the three subjects and the interaction between them, with an emphasis on recent trends and research topics in them. The introductory part is aimed at lower graduate (honours and masters) students but will be accessible for undergraduates majoring in mathematics and computer science too. Essentially no special knowledge, but some formal background, will be expected for these courses. The advanced part will be suitable for higher graduate (masters and doctoral) students and researchers. 1) PART 1: Introductory courses. December 1-4, RAU-Island (Vaal Dam, see below). Each course will comprise four sessions and will give a general background into the subject(s), necessary to follow the advanced courses. COURSES AND LECTURERS: (Legend: L:Logic, UA: Universal Algebra, TCS: Theoretical Computer Science) L: Patrick Blackburn (University of Saarland) UA: Matt Valeriote (McMaster University, Canada) TCS: Austin Melton (Kent State Univ., USA) L&UA: Yde Venema (University of Amsterdam, Netherlands) L&TCS: Holger Schlingloff (University of Bremen, Germany) UA&TCS: H. Peter Gumm (University of Marburg, Germany) 2) PART 2: Advanced courses, tutorials, workshops, open sessions. December 6-10, Rand Afrikaans University, Johannesburg. (NB: the duration of the school has been extended by 1 day since the 1st announcement.) Each of the modules listed below will consist of a tutorial part, possibly followed by a workshop part. 2.1) LECTURERS/WORKSHOP ORGANIZERS AND TOPICS: -) Hajnal Andreka, Istvan Nemeti (Math. Inst. Hungarian Acad. of Sciences): Logic, relativity theory and Tarskian geometry. -) Johan van Benthem (Univ. of Amsterdam, Netherlands): Game theory and modal logic. -) Zhou Chaochen, (United Nations Univ., Macau): Duration Calculus. -) Anuj Dawar (Univ. of Cambridge, UK): Fixed point logics and finite model theory. -) Brian Davey (La Trobe Univ., Australia): Advanced universal algebra. -) Mai Gehrke (New Mexico State Univ., USA): Lattices with additional operations. -) Robin Hirsch (Univ. College London, UK): Algebraic logic. -) Wilfrid Hodges (Queen Mary and Westfield College,UK): Advanced logic. -) Bart Jacobs (University of Nijmegen, Netherlands) and Jan Rutten (Centre for Mathematics and Computer Science, Netherlands): Co-algebra, theory and applications. -) Thomas Jech (Penn State Univ., USA): Left-distributive algebras. -) Maarten de Rijke (Univ. of Amsterdam, Netherlands): Computational logic and automated theorem proving. -) Moshe Vardi (Rice Univ., USA): Automata-theoretic approach to design verification. -) Jeff Zucker (McMaster Univ., Canada): Computability on abstract algebras. 2.2) WORKSHOPS and OPEN SESSIONS: Participants will have the opportunity to present their research at open sessions and special workshop sessions. If you wish to contribute a talk to any of the workshops, please contact the respective organizer(s) BEFORE AUGUST 1 (see webpage for email addresses). For participation in the open session, send or e-mail in either plain text, standard LaTeX, or Postscript, a one A4 page abstract to the address of the school, to reach us BY AUGUST 1. Notification of acceptance/rejection will be send to you soon after submission, and not later than AUGUST 15, unless otherwise specified by the workshop organizers. More details on the courses, tutorials and workshops and detailed programme of the School will be placed in due course on our Webpage at http://proof.mth.uct.ac.za/~pjipsen/luatcs99 and sent to the registered participants with the 3rd announcement. 2.3) CREDITS: The courses offered at the school can be taken for official credit and recognized (by prior arrangements with respective heads of departments) as modules for graduate courses, after successful completion of assignments given by the respective lecturers. II. TIME: December 1-10, 1999. 9 working days, and a free/relocation day on December 5. (Note that this is an early summer time in the Southern hemisphere.) III. PLACES AND ACCOMMODATION: Part I: December 1-4 1999, RAU-Island. This is a fairly large island in the Vaal Dam, some 100 km south of Johannesburg. The island is a nature reserve, with various game on it to be seen: springboks, blesboks, gemsboks, zebras, gnus, etc. Besides the wilderness, it also has conference, accommodation, and recreation facilities including: 3 lecture rooms with boards and overhead projectors (one of them with an aircon); full board (accommodation and 3 meals a day), barbecue area, swimming pool, rugby field, volley-ball court etc. ARRIVAL AND REGISTRATION: November 30. We shall provide bus transportation for all participants from RAU campus to the Island on that day. There will be two buses, the first leaving at 12.00, and the second at 16.00. We can transport, upon prior request, participants from the Johannesburg International Airport to RAU on November 30, between 10.00 and 15.00h. (Please book your trip to Johannesburg so as to reach RAU campus in time, because there is no regular transport to the Island.) On December 5 all participants will be transported back to RAU campus. ACCOMMODATION: The accommodation on the island is somewhat primitive (yet satisfactory, at least in summer time) and includes a few individual rooms (which will be reserved for invited lecturers), while the participants will be accommodated in two large sleeping barracks (for men and women) each with toilet and shower facilities. The FULL PACKAGE (transportation by bus-boat between RAU and the Island, accommodation, 3 meals and refreshments for 5 days) will cost R550 pp. Note that the access between the mainland and the island is by a special boat only, which can be hired at a cost. NB: Because of the limited accommodation facilities on the island, the number of participants in the first part of the school will be limited, so early registration for that part is essential. PART II: December 6-10, 1999, RAU campus. The university campus is situated in Auckland Park, a relatively quiet and safe suburb off the business center of Johannesburg. It has very good conference facilities, and the participants will be provided with computers and access to Internet during this part of the event. For more info about RAU, visit its Web site at http://www.rau.ac.za. ARRIVAL AND REGISTRATION: December 5. There will be a Welcome reception at RAU during and after the registration of that evening. ACCOMMODATION: We offer 3 main options for the accommodation during the 2nd part of the school: A) Hotel. The following special rates have been negotiated with Randburg Towers Hotel (3 star, near Waterfront in Randburg, about 30 min drive to RAU), between which and RAU we shall provide twice daily bus transport. Single rooms: R244 pp/pd, incl. breakfast. Double and twin rooms: R230 per room/pd, excl. breakfast @ R29 per person. All rooms are with bath en suite, aircon, telephone, and TV. B) There are limited possibilities for accommodation in guest-houses within walking distance from the university, offering good, more intimate environment, with prices ranging from R200-300 pp/pd, breakfast included. The guest-houses have limited capacities and will be booked on the basis of first registered - first booked. C) Student hostels of the University of Witwatersrand (Wits), about 10-15 min drive from RAU. A DAILY PACKAGE of single room, breakfast, and bus transportation to and from RAU during December 5-10 will cost R100 pp/pd. In addition, dinners can be booked at the hostels at R25. The last night for which we have booked the hostels is December 10/11. Those who wish to stay there longer should make their own arrangements. For more luxurious accommodation and additional options, check out our Web-page, but please note that if you choose an accommodation not listed above, you should make your own booking and transport arrangements. IV. GRANTS: We offer a limited number of student grants covering, partly or fully, registration fee and the local expenses of participants who are academically deserving and need financial support for the attendance of the school. Graduate students and young researchers from disadvantaged communities, interested in the subjects of the School are encouraged to apply. The grant applications should include: i) letter of application; ii) short curriculum vitae iii) short description of completed and currently studied graduate courses, topic(s) of master/doctoral theses (if applicable), and research interests. iv) reference from the supervisor. The applications should reach us soon as possible and NOT LATER THAN JULY 1, 1999, electronically or per ordinary mail to our postal address given at the end of this announcement. V. PRE-REGISTRATION: The registration form is attached separately or can be downloaded from our Web page. Please complete and send it per e-mail, fax or mail, to reach us BY SEPTEMBER 1. VI. PAYMENTS: 1) REGISTRATION FEE covering the attendance of the courses, tutorials and workshops, up to 6 sets of course readers per part, and refreshments. The EARLY fees, payable by SEPTEMBER 1, 1999 are as follows (at present 1US $ trades for approx. 6 rands): -) Students: R 100 (Part 1), R100 (Part 2), R200 (both). -) Academic participants: R 200 (part 1), R200 (part 2), R400 (both). -) Accompanying persons: R 50 (part 1), R50 (part 2), R100 (both). (excl. course readers). -) Other participants: R 300 (part 1), R300 (part 2), R600 (both). NB: FROM SEPTEMBER 1, ALL FEES ABOVE GO UP BY 20%. Deadline for payment: NOVEMBER 1, 1999. 2) An ACCOMMODATION DEPOSIT of R200 is payable at pre-registration, or NOT LATER THAN NOVEMBER 1, 1999. The remaining part of the accommodation will be settled directly by the participants (in the hotels and guest-houses) or paid to the organizers on arrival (for the Island and Wits hostels). 3) Cancellation policy: before November 1: full refund, less administrative costs. After November 1: 50% of the registration fee plus the deposit, if still refundable to us. 4) The methods of payment are indicated in the registration form. VII. Summary of DEADLINES: 1) For grant applications: JULY 1. 2) For submissions to the workshops and the open sessions: AUGUST 1. 3) For notification AUGUST 15 (unless otherwise specified by the organizers). 4) For registration and payment of EARLY fees: SEPTEMBER 1. 5) For FULL payment of registration fees and accommodation deposit: NOVEMBER 1. VIII. OTHERS: All prices below are payable on arrival. 1) Lunch packages of 5 lunches will be arranged during the second part of the school at R150. 2) A banquet will be organized on December 8 at R70 per person. 3) One-day outings will be organized on December 11 to Gold Reef City (Johannesburg), and to the Rhino and Lion Nature reserve and Sterkfontein Caves (about 30-40 km away from Johannesburg) each at approx. R50 pp. Details will be included in the 3rd announcement and placed on the Web. If you are interested in additional touring, excursions, entertainment and other recreational activities in South Africa you can contact Brenda or Tania from Melville Travel at Meltrav(a)yebo.co.za, tel. ++27-11-726-7166, fax: ++27-11-726-7485, or any other South African travel agency. Visit our Webpage for more details. IX. FURTHER INFORMATION AND ENQUIRES: For updates and further information, check out our Webpage at: http://proof.mth.uct.ac.za/~pjipsen/luatcs99 For all correspondence, enquires, and to be included on the mailing list, please write to: luatcs99(a)na.rau.ac.za or send a letter to: LUATCS'99 Department of Mathematics Rand Afrikaans University PO BOX 524 Auckland Park 2006 South Africa You can also contact us directly: Val Goranko at vfg(a)na.rau.ac.za or Peter Jipsen at pjipsen(a)maths.uct.ac.za or Isabella Burger at icb(a)na.rau.ac.za. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% LUATCS '99 REGISTRATION FORM ========== ================= Wherever requested to indicate choices, please mark with an X in the brackets or leave blank. The completed registration form should reach us by SEPTEMBER 1 per e-mail, fax, or ordinary mail. 1. PERSONAL INFORMATION Title, surname, and first name(s):..................................... Affiliation:........................................................... Address:............................................................... ....................................................................... Telephone:............. Fax:................... E-mail address:................................ Student[ ] Academic[ ] Other[ ] (Please choose one of these.) Accompanying persons: Yes[ ] / No[ ] If yes: Name(s):.............................................. 2. DETAILS ON PARTICIPATION 2.i) Which parts of the school would you like to attend? Part 1 [ ] Part 2 [ ] Both parts [ ] 2.ii) Which courses and tutorials/workshops do you intend to attend? (This is just preliminary info for us. You can change your mind later.) Part 1 (1-4 Dec): Blackburn[ ] Gumm[ ] Melton[ ] Schlingloff[ ] Valeriote[ ] Venema[ ] Part 2 (6-10 Dec): Andreka/Nemeti[ ] Chaochen[ ] Davey[ ] Dawar[ ] de Rijke[ ] Gehrke[ ] Hirsch[ ] Hodges[ ] Jacobs/Rutten[ ] Jech[ ] van Benthem[ ] Vardi[ ] Zucker[ ] 2.iii) Which sets of course notes/readers do you want to receive? (The cost of 6 sets per part is included in the registration fee; the rest will cost up to R20 per set - payable on arrival.) Part 1 (1-4 Dec): Blackburn[ ] Gumm[ ] Melton[ ] Schlingloff[ ] Valeriote[ ] Venema[ ] Part 2 (6-10 Dec): Andreka/Nemeti[ ] Chaochen[ ] Davey[ ] Dawar[ ] de Rijke[ ] Gehrke[ ] Hirsch[ ] Hodges[ ] Jacobs/Rutten[ ] Jech[ ] van Benthem[ ] Vardi[ ] Zucker[ ] 2.iv) Do you intend to give a talk in a workshop or an open session? Workshop[ ] / Open session[ ] / None [ ] If yes, please give a title and specify the workshop (if applicable): ................................................................. 3. TRAVEL 3.i) Arrival date and time, airline and flight number (if already known): ............................................................ 3.ii) Departure date and time:................................... Do you need transportation from and to Johannesburg bus station or airport? Station[ ] / Airport[ ] 4. ACCOMMODATION (If you have accompanying persons, please book for them, too.) 4.i) Part 1: December 1-4. Arrival and registration day: Nov 30. Departure: Dec 5. RAU Island: total package of R550 per person, including accommodation, 3 meals a day, refreshments, and bus/boat transport to and from the island. 4.ii) Part 2: Dec 6-10, RAU Campus. Arrival and registration day: Dec 5. Departure: evening of Dec 10, or later; for the hostels: not later than Dec 11 unless arranged individually. Please indicate your preferences for accommodation in a priority order, choosing from the options below. All prices are per room per night, for single rooms including breakfast, for double rooms excluding breakfast (@R29 per person). 1: 2: 3: If sharing a double room in the hotel, the name of your roommate: Note that a R200 accommodation deposit is required, payable with registration fee. A) Hotel SINGLE DOUBLE R244 R230 B1) Guest-house at R200 - R250. B2) Guest-house at R250 - R300. C) Student hostel: R100. D) My own arrangement. 5. VARIA. If you have accompanying persons, please book for them as well, by putting a number in the brackets. All payments are due on arrival. 5.i) Would you like lunch package(s) during Dec 6-10 (@ R150 per package)? Yes [ ] No[ ]. Please specify any dietary restrictions: 5.ii) Would you like to attend the banquet on Dec 8 (@ R70 per person)? Yes [ ] No [ ]. 5.iii) Would you like to join the outing on Saturday, Dec 11 (@ approx. R50)? - to Gold Reef City, Johannesburg [ ] - to the Rhino and Lion Nature Reserve and Sterkfontein Caves [ ]. 6. PAYMENTS. 6.i) Please indicate the registration fee applicable to you (IF PAYABLE AFTER SEPTEMBER 1, PLEASE ADD 20% TO THE RATES BELOW) here: [ ] Part 1 Part 2 Both *Student R100 R100 R200 Academic R200 R200 R400 Accomp. person R50 R50 R100 Other R300 R300 R600 *Please attach proof. TOTAL PAYMENT DUE: (Deposit and registration fee) [ ] 6.ii) MEANS OF PAYMENT. A) Personal or bank cheque PAYABLE IN SOUTH AFRICAN RANDS, made out to: RAU LUATCS '99. Send to: LUATCS'99, Department of Mathematics, PO Box 524, Auckland Park 2006, SOUTH AFRICA. Cheque enclosed : Yes[ ] / Will be sent later [ ]. B) Please debit my credit card: Card type: Visa[ ] Master[ ] Euro[ ] American Express[ ] Diners Club [ ] Card number : Expiry date : Name as it appears on the card: Authorisation for total amount: C) Bank Transfer To: ABSA Bank, Auckland Park, Branch number 33510524, Account number : 284 0000 136. PLEASE NOTE: if you use bank transfer, your surname and initials as well as this reference number: 9331 8659 05 MUST APPEAR on the deposit slip, of which a copy must be sent to us. 7) REMARKS (if any): SIGNATURE:............................... DATE:...............

1 0

OOSDS99 Call for papers
by Natalia Ioustinova 21 May '99

21 May '99

======================================================================== This message contains public information, only, and the receiver is allowed, and invited, to copy it and distribute it further. Our apologies if you received duplicates of this message due to the mailing list aliases. You can also visit the OOSDS'99 web site at http://www.tec.informatik.uni-rostock.de/IuK/congr/oosds99/ ======================================================================== CALL FOR PAPERS OOSDS'99 Workshop on Object-Oriented Specification Techniques for Distributed Systems and Behaviours Paris, France, September 27, 1999 http://www.tec.informatik.uni-rostock.de/IuK/congr/oosds99/ ======================================================================== SCOPE OF WORKSHOP: ================= The workshop is focused on specification languages for distributed systems which are extensions of object-oriented languages or have an object-oriented kind of base structure. The aim is to bring together researchers interested in incorporating object-oriented concepts and formal methods for specification of distributed systems and behaviours. TOPICS (NOT EXCLUSIVE LIST): ============================ Object-oriented approaches to specification of distributed systems and behaviours. Semantic models for concurrency and object-orientation (e.g. based on the lambda-calculus, process algebra, pi-calculus, linear logic). Characteristic examples of object-oriented specification from real application domains (e.g. distributed algorithms, workflow specification, communication protocols). Logic reasoning on distributed systems and behaviours. SUBMISSION: =========== The deadline for submission is September 2, 1999. Submission is in electronic form only. Submission may be of two forms: Extended abstracts: up to 3 pages. Papers and reports: up to 6 pages. In both cases a separate page with the following information: title, author(s), corresponding author, contact information and a 12-15 lines summary should be included. The papers and/or abstracts should be sent by e-mail to oosds99(a)informatik.uni-rostock.de. Selection for presentation will be carried out by the organizers. Emphasis is put on the potential of the submission to stimulate discussions in the above-mentioned scope. Notification of acceptance is expected for September 14, 1999. PUBLICATION: ============ The accepted submissions will be published electronically, i.e. they will remain available from the workshop web page. Furthermore, selected papers will be invited for post workshop publication. RELATED EVENTS: ============== This workshop is organized as a satellite workshop of PPDP'99, The 1999 International Conference on Principles and Practice of Declarative Programming, Paris, France, September 29-October 1, 1999. http://www.dmi.ens.fr/~fages/PPDP99/ ORGANIZATION COMMITTEE: ======================= Clemens H. Cap (Rostock University, Germany) Natalia Ioustinova (Rostock University, Germany) Javier Oliver (Technical University of Valencia, Spain) Nobuko Yoshida (University of Sussex, UK) ADDITIONAL INFORMATION: ======================= WEB: http://www.tec.informatik.uni-rostock.de/IuK/congr/oosds99/ MAIL: oosds99(a)informatik.uni-rostock.de

1 0

Illness of John Isbell
by John Duskin 17 May '99

17 May '99

The many readers of the "Categories" list will be saddened to hear that our friend and colleague and long time contributor to the list, John Isbell, is critically ill in Millard Fillmore Hospital here in Buffalo, suffering from a very serious blood infection. At present, his condition is stable, but remains critical. His family and friends here in Buffalo know that you join us in wishing him a speedy and complete recovery.

1 0

Recursive types in polymorphic lambda calculus
by Philip Wadler 15 May '99

15 May '99

There is a fairly standard encoding of recursive types into polymorphic lambda calculus, given by rec X.F[X] = all X.(F[X] -> X) -> X where F[X] is a type in which the type variable X appears only covariantly. Recall that every covariant type corresponds to a covariant functor, so for every h:X->Y we have F[h]:F[X]->F[Y]. If we abbreviate T = rec X.F[X], then the key functions on this type are given by the polymorphic lambda terms: fold : all X.(F[X] -> X) -> T -> X fold = Lam X.lam k:F[X]->X.lam t:T.t{X}(k) in : F[T] -> T in = lam u:F[T].Lam X.lam k:F[X]->X.k(F[fold{X}(k)](u)) out : T -> F[T] out = fold{F[T]}(F[in]) Questions: Who first had this insight? Where is a good place to find this spelled out in the literature? Please send results to me, and I will summarize them for the list. Cheers, -- P

1 0

WoLLIC'99 - Call for Participation
by Ruy de Queiroz 13 May '99

13 May '99

PROGRAMME AND CALL FOR PARTICIPATION 6th Workshop on Logic, Language, Information and Computation (WoLLIC'99) May 25-28, 1999 http://www.di.ufpe.br/~wollic/wollic99/ Hotel Simon, Itatiaia National Park, Rio de Janeiro, Brazil (In conjunction with "XII Encontro Brasileiro de Logica - EBL'99") SCIENTIFIC SPONSORSHIP Interest Group in Pure and Applied Logics European Association for Logic, Language and Information (FoLLI) Association for Symbolic Logic (ASL) Sociedade Brasileira de Computaco (SBC) Sociedade Brasileira de Logica (SBL) FUNDING CAPES, CNPq, Facolta di Scienze, Univ. di Verona ORGANISATION Departamento de Informatica, Universidade Federal de Pernambuco Facolta` di Scienze, Universita` degli Studi di Verona Centro de Logica, Epistemologia e Historia da Ciencia, Univ.Campinas PROGRAMME TUESDAY MAY 25th, 1999 (Tutorial Day) Tutorials: 08:00-10:00 (with a 10min break) Introduction to Game Semantics by Samson Abramsky 10:00-10:15 Coffee/tea break 10:15-12:15 (with a 10min break) Markov Decision Processes and Bayesian Networks by Craig Boutilier 12:15-14:00 Lunch break 14:00-16:00 (with a 10min break) A Crash Course in Distributive Lattices by Francisco Miraglia 16:00-16:15 Coffee/tea break 16:15-18:15 (with a 10min break) Stability and Finite Model Theory by John Baldwin 18:15-18:30 Coffee/tea break 18:30-20:30 (with a 10min break) Bounded Arithmetic, Nonstandard Models by Alan Woods WEDNESDAY MAY 26th, 1999 Morning: Logic and Computation 08:30 OPENING 09:00-10:00 (Invited talk WoLLIC'99/EBL'99) Chair: John Baldwin Concurrent Games and Full Completeness by Samson Abramsky, Division of Informatics, Edinburgh University, UK 10:00-10:15 Coffee/tea break 10:15-11:15 3 contributed papers (20min each) Chair: Ruy de Queiroz 10:15-10:35 omega-continuos cpo's, omega-algebraic cpo's, SFP domains and retract of SFP domains as information systems by Benjamin Callejas Bedregal, Departamento de Informatica e Matematica Aplicada, Universidade Federal do Rio Grande do Norte, Brazil 10:35-10:55 Alpha Conversion in Simply Typed Lambda Calculus by Ana Bove, Department of Computing Science, Chalmers University of Technology, Goteborg, Sweden, and Paula Severi, Centro de Matematica, Facultad de Ciencias, Universidad de la Republica, Uruguay 10:55-11:15 Dependence Analysis Through Type Inference by Ozan Hafizogullari and Christoph Kreitz, Department of Computer Science, Cornell University, USA 11:15-11:30 Coffee/tea break 11:30-12:30 (Invited talk EBL'99/WoLLIC'99) Chair: Valeria de Paiva (TBA) by Paulo Veloso, Departamento de Informatica, Pontificia Universidade Catolica do Rio de Janeiro, Brazil 12:30-14:00 Lunch break Afternoon: Logic and Information 14:00-15:00 (Invited talk) Chair: Alan Woods Abstraction and Decomposition Techniques for Markov Decision Processes by Craig Boutilier, Department of Computer Science, University of British Columbia, Canada 15:00-15:15 Coffee/tea break 15:15-16:15 3 contributed papers (20min each) Chair: Ana Teresa C. Martins 15:15-15:35 A little note about Maxichoice and Epistemic Entrenchment by Eduardo Ferme, Departamento de Computacion, Universidad de Buenos Aires, Argentina 15:35-15:55 Irrevocable Belief Revision and Epistemic Entrenchment by Eduardo Ferme, Departamento de Computacion, Universidad de Buenos Aires, Argentina 15:55-16:15 A logic-based system for controlling inconsistencies in evolutionary databases by Walter A. Carnielli, Centro de Logica, Universidade Estadual de Campinas, Brazil, and Sandra de Amo, Departamento de Informatica, Universidade Federal de Uberlandia, Minas Gerais, Brazil THURSDAY MAY 27th, 1999 Morning: Logic, Model Theory and Complexity Theory 09:00-10:00 (Invited talk WoLLIC'99/EBL'99) Chair: Francisco Miraglia Finite and Infinite Model Theory by John Baldwin, Department of Mathematics, Statistics and Computer Science, University of Illinois at Chicago, USA 10:00-10:15 Coffee/tea break 10:15-11:15 3 contributed papers (20min each) Chair: E. Hermann Hauesler 10:15-10:35 Model theory of the recursively enumerable many-one degrees by Andre O. Nies, Department of Mathematics, University of Chicago, USA 10:35-10:55 On clausal models by Dusan Guller, Institute of Informatics, Comenius University, Slovakia 10:55-11:15 (tba) by (tba) 11:15-11:30 Coffee/tea break 11:30-12:30 (Invited talk) Chair: Craig Boutilier Intrinsic theories: a methodology for reasoning about functional programs and their computational complexity by Daniel Leivant, Department of Computer Science, Indiana University, USA 12:30-14:00 Lunch break Afternoon: Categorical Logic and Non-Classical Logics 14:00-15:00 (Invited talk WoLLIC'99/EBL'99) Chair: Samson Abramsky A Lattice-Theoretic Concept of Logical Connective by Francisco Miraglia, Instituto de Matematica e Estatistica, Universidade de Sao Paulo, Brazil 15:00-15:15 Coffee/tea break 15:15-16:15 3 contributed papers (20min each) Chair: Mario Benevides 15:15-15:35 Hybrid logic is the bounded fragment of first order logic by Carlos Areces, University of Amsterdam, The Netherlands, Patrick Blackburn, Universitaet des Saarlandes, Germany, and Maarten Marx, University of Amsterdam, The Netherlands 15:35-15:55 A Dynamic Modal Arrow Logic for the Interpretation of Verb Stems and Voice Affixes in Tagalog by Ralf Naumann and Anja Latrouite, Seminar fuer Allgemeine Sprachwissenschaft, Universitaet Duesseldorf, Germany 15:55-16:15 The Taming (Timing) of the States by Angelo Montanari, Adriano Peron and Alberto Policriti, Dipartimento di Matematica e Informatica, Universita` di Udine, Italy FRIDAY MAY 28th, 1999 Morning: Logic and Proof Theory 09:00-10:00 (Invited talk WoLLIC'99/EBL'99) Chair: Daniel Leivant Bounded Arithmetic from a Rational Perspective by Alan Woods, Department of Mathematics, University of Western Australia, Australia 10:00-10:15 Coffee/tea break 10:15-11:15 3 contributed papers (20min each) Chair: Luiz Carlos Pereira 10:15-10:35 A Cut-Free Gentzen Formulation of Modal Logic S5 by Torben Brauner, Centre for Philosophy and Science-Theory, Aalborg University, Denmark 10:35-10:55 A Sequent Calculus for a Paraconsistent Default Logic by Ana Teresa de C. Martins, Tarcisio Pequeno and Marcelino Pequeno, Departamento da Computacao, Universidade Federal do Ceara', Brazil 10:55-11:15 A sequent calculus for Lukasiewicz's three-valued logic based on Suszko's bivalent semantics by Jean-Yves Beziau, LNCC/CNPq, National Laboratory for Scientific Computing, Rio de Janeiro, Brazil 11:15-11:30 Coffee/tea break 11:30-12:30 (Invited talk EBL'99/WoLLIC'99) Chair: (tba) (TBA) by (to be announced) 12:30 CLOSING ------

1 0

FroCoS'2000: First Call for Papers
by Christophe Ringeissen 12 May '99

12 May '99

[We apologize for multiple copies] First Call for Papers Third International Workshop ``Frontiers of Combining Systems'' FroCoS'2000 March 22-24, 2000, Nancy, France http://www.loria.fr/conferences/frocos2000/ In various areas of computer science, such as logic, computation, program development and proof, artificial intelligence, there is an obvious need for using specialized formalisms and inference mechanisms for special tasks. In order to be usable in practice, these specialized systems must be combined with each other, and they must be integrated into general purpose systems. The development of general techniques for the combination and integration of special systems has been initiated in many areas. The two previous international workshops on ``Frontiers of Combining Systems'' were held in Munich (1996) and in Amsterdam (1998). Like its predecessors, FroCoS'2000 is intended to offer a common forum for research activities in the general area of combination and integration of systems, and on their practical use. Suggested, but not exclusive topics of interest for the workshop are: * combination of logics * combination of constraint solving techniques, of decision procedures, of term rewriting systems * combination of deduction systems and computer algebra * integration of decision procedures and other solving processes into constraint programming and deduction systems * modelisation of hybrid systems * logic modelling of multi-agent systems. We expect to attract high quality original papers that cover relevant aspects of these topics. All submissions will be thoroughly evaluated. On the basis of the referee reports, papers will be selected for presentation at the conference and for the published post-conference proceedings. Program Committee: F. Baader (RWTH Aachen) D. Basin (U. Freiburg) F. Benhamou (U. Nantes) T. Fruehwirth (LMU Muenchen) F. Giunchiglia (ITC-IRST Trento) B. Gramlich (TU Wien) H. Kirchner (LORIA Nancy) C. Kreitz (Cornell U.) T. Mossakowski (U. Bremen) J. Pfalzgraf (U. Salzburg) M. de Rijke (U. Amsterdam) C. Ringeissen (LORIA Nancy) T. Scott (U. Paderborn/INRIA) M. Wallace (IC-Parc London) Program Chairs: H. Kirchner and C. Ringeissen LORIA & INRIA-Lorraine Campus Scientifique - BP 239 54506 Vandoeuvre-les-Nancy Cedex France E-mail: frocos(a)loria.fr Local Organization: C. Bergeret, A.-L. Charbonnier, A. Demange, H. Kirchner, C. Ringeissen, L. Vigneron. Paper Submissions: Authors are encouraged to use LaTeX and the standard article class/style file (10pt). The primary means of submission will be electronic, in PostScript format. Papers should be compressed, then uuencoded, and e-mailed to the program chairs. Papers should not exceed 15 pages, and should be received via e-mail by October 1, 1999. Results must be unpublished, and not submitted for publication elsewhere. Submissions should start with title, author(s) (names, correspondence addresses, e-mail addresses), and abstract. Important Dates: Paper Submissions: October 1, 1999 E-mail for paper submissions: frocos(a)loria.fr Notification of Acceptance: December 20, 1999 Final Versions due: February 5, 2000 Conference: March 22-24, 2000 FroCoS'2000 is just before ETAPS'2000 (Berlin, March 25-April 2,2000) so that attendance to both conferences can be suitably combined. Information on FroCoS'2000 is available by WWW: http://www.loria.fr/conferences/frocos2000/

1 0

FMCS 99
by robin＠cpsc.ucalgary.ca 12 May '99

12 May '99

************************************************* * * * FFFFF M M CCC SSSS 9999 9999 * * F MM MM C S 9 9 9 9 * * FFFFF M MM M C SSS 99999 9999 * * F M N C S 9 9 * * F M M CCC SSSS 9999 9999 * * * **********************FMCS 99******************** CALL FOR PARTICIPATION: The Department of Computer Science at the University of Calgary is hosting the Foundational Methods in Computer Science workshop on June 3rd - 6th, 1999 at the Kananaskis Field Station in Alberta, Canada. The workshop is an informal meeting to bring together researchers in mathematics and computer science with a focus on the application of category theory in computer science. It is a three day meeting, that starts with a day of tutorials aimed at students and newcomers to category theory, followed by a day and a half of research talks. The meeting this year has a little website (the schedule and speakers will be announced on the site) see: http://www.cpsc.ucalgary.ca/~fmcs99 The workshop will have approximately the same format as last year, with a day of tutorials on friday June 4 and shorter research presentations on June 5 and 6. Tutorials will be given by: Ernie Manes More monads ... Rick Blute Linear Logic Phil Mulry Partial maps David Benson Sketches and complexity Due to the location (in the foothills of the Rockies) we shall be adopting a mountain conference schedule: lectures will run 9:00am - 12:00pm, packed lunches (a chance for walks and talks etc.), supper at 5:30pm, and lectures resume 7:00pm - 10:00pm. The area offers walks of all standards in some of the most stunning mountain scenery of the Rockies. In June the evenings still get quite cool. We do have limited support for student participation (for which one must apply) as usual student participation and talks are encouraged. If you would like to attend this year please visit the web site and send in your registration form! I look forward to seeing you at FMCS ... Robin Cockett

1 0

PROBMIV'99: Final Call for Papers
by Marta Z Kwiatkowska 11 May '99

11 May '99

[Please circulate this to anyone interested. Apologies for multiple copies.] _________________________________________________________________________ 2nd CALL FOR PAPERS PROBMIV'99 2nd International Workshop on Probabilistic Methods in Verification http://fmt.cs.utwente.nl/probmiv99/ a satellite to CONCUR'99 Eindhoven, 23rd Aug 1999 (to coincide with EXPRESS'99, another satellite) _________________________________________________________________________ SCOPE OF THE WORKSHOP Probability inherently features in software and hardware systems, either as a means to derive efficient solutions (e.g. randomization), or as a result of unreliable or unpredictable behaviour (e.g. fault-tolerant systems, computer networks, etc). *Probabilistic verification* encompasses a range of theoretical, algorithmic and programming methods that assist in establishing the correctness of probabilistic systems against specifications. Typically this involves calculating the probability bounds for a temporal logic formula being satisfied, based on an appropriate probability space on computations, but also includes properties such as cost analysis and long-run average. Additionally, probabilistic verification can provide guarantees the specifications hold with satisfactory probability in cases when conventional model checking is not feasible. The idea of this workshop is to bring together researchers that apply probabilistic methods across the whole spectrum of verification. The meeting aims to enable cross-fertilisation of ideas and techniques between areas that are usually not in regular contact through conferences, from semantics, probability theory, performance analysis and computational linear algebra, through randomized algorithms, probabilistic logics, model checking, abstract interpretation, to practical experimental work, tools and applications. This is the second workshop of this kind. The first meeting, PROBMIV'98 was held in 1998 as a satellite to LICS. In 1999, the workshop takes place as a satellite to CONCUR. _________________________________________________________________________ INVITED SPEAKERS Rance Cleaveland, SUNY at Stony Brook Bengt Jonsson, University of Uppsala Kim G. Larsen, Aalborg University Oded Maler, Verimag _________________________________________________________________________ STEERING AND PROGRAM COMMITTEE Rajeev Alur, University of Pennsylvania Christel Baier, University of Mannheim Luca de Alfaro, University of California at Berkeley Michael Huth, Kansas State University Joost-Pieter Katoen, University of Twente Marta Kwiatkowska, University of Birmingham (chair) Roberto Segala, University of Bologna Prakash Panangaden, McGill University _________________________________________________________________________ SUBMISSION GUIDELINES We are seeking papers on the following example (non-exclusive) topics: * Modelling and verification of probabilistic and stochastic systems, including real-time and hybrid systems * Formal models and verification techniques for randomized algorithms * Semantics of probabilistic and stochastic processes * Probabilistic logics * Design of verification support tools * Tool demonstrations * Case studies Submissions may be of two forms: short abstracts of up to 4 pages or full papers of 10-15 pages (previously unpublished). Simultaneous submission to other conferences or journals is *only* allowed for short abstracts. Because of the informal character of the workshop, we encourage work in progress reports. Authors should send their papers preferably electronically to the address probmiv99(a)cs.bham.ac.uk (as platform-independent PostScript files printable on A4 paper and 8-1/2" x 11" paper, plus a plain text message containing the submissions's title, abstract, and the main author's address including e-mail and FAX) by the deadline shown below. Alternatively, authors may instead send 3 copies of the hardcopy of their paper to Marta Kwiatkowska (Chair) School of Computer Science University of Birmingham Edgbaston, B15 2TT, UK Tel +44 (121) 414-7264 (voice) FAX +44 (121) 414-4281 mzk(a)cs.bham.ac.uk All submissions will be refereed in the normal manner. Preliminary proceedings, excluding short abstracts, will be published electronically and as a Technical Report of the University of Birmingham, to be available at the workshop. We are currently investigating the possibility of publishing proceedings after the workshop as a volume of ENTCS jointly with the EXPRESS'99 workshop. _________________________________________________________________________ IMPORTANT DATES 17 May 1999 ***Submissions due*** 21 June 1999 Notification of acceptance or rejection 19 July 1999 Final versions due for preliminary proceedings _________________________________________________________________________ LOCAL ORGANISATION Holger Hermanns, University of Twente Erik de Vink, Free University Amsterdam _________________________________________________________________________ FURTHER INFORMATION For more information please see URLs PROBMIV'99 http://fmt.cs.utwente.nl/probmiv99/ CONCUR'99 http://www.win.tue.nl/concur99/ EXPRESS'99 http://www.docs.uu.se/~victor/Express/express99.shtml PROBMIV'98 http://www.cs.bham.ac.uk/~mzk/probmiv98.html _________________________________________________________________________

1 0

Summer address for categories
by Marta Bunge 11 May '99

11 May '99

----------------------------------------------------------------------------- Marta Bunge wishes to communicate her mailing address and personal fax/phone for the period June 1st-August 31st 1999. Mailing Address: c/o Margarita Desengrinis, Ag. Dimitriou 6, 49100 CORFU, Greece. Personal Fax/Telephone: 663 41584. An email address will be added later if it becomes available. ---------------------------------------------------------------------------- Marta Bunge Dept.of Mathematics & Statistics bunge(a)math.mcgill.ca McGill University Phone: 514-933-6191(H)/398-3810(O) Sherbrooke Street West 805 Fax: 514-933-8741(H)/398-3899(O) Montreal, QC http://www.math.mcgill.ca/~bunge Canada H3A 2K6

1 0