Subject: ? trees Date: Mon, 6 May 91 15:16:34 EDT From: barr@triples.Math.McGill.CA (Michael Barr) Call a rooted tree supercalifragilistic if no node has isomorphic daughters. There must be a standard word for this; does anyone know what it is? A related question. Let T denote the set of binary rooted trees. There is an idempotent retraction that identifies isomorphic sibs and then repeats this process until you produce a supercalifragilistic tree. This retract is compatible with the morphism T --> 1 + T^2/2! (that means the symmetric square or set of one and two element subsets) that takes a bare root to 1 and a proper tree to its set of daughters. Does anyone know if there are any further retracts that are compatible with that morphism? Michael Subject: re supercalifragilistic trees From: Paul Taylor Date: Wed, 8 May 91 11:09:58 BST of course there's a standard word - from set theory - extensional! Subject: Trakhtenbrot Symposium Program, June 10-12, Tel-Aviv ADVANCE PROGRAM An International Symposium on Theoretical Computer Science in honor of BORIS A. TRAKHTENBROT on the occasion of his Retirement and Seventieth Birthday sponsored by The Moise & Frida Eskenasy Institute of Computer Sciences TEL AVIV UNIVERSITY, JUNE 10-12, 1991 MONDAY June 10 9:00 REGISTRATION 9:30 OPENING SESSION (Schreiber Bldg., Ramneceanu Hall) Amiram Yehudai, Tel-Aviv U., Organizing Chair Dan Amir, Vice Rector, Tel-Aviv University David Horn, Dean, Raymond and Beverly Sackler Faculty of Exact Sciences Albert R. Meyer, MIT, Symposium Chair 10:00 J. Barzdins (U. Latvia) Inductive synthesis: old and new approaches 10:35 Break 11:05 Eli Shamir (Hebrew U.) PAC learning of fuzzy concept classes by quantizing the underlying domain 11:40 Michail A. Taitslin (Tver' U., USSR) Datalog and expert systems 12:15 LUNCH break 14:00 Arnon Avron (Tel-Aviv U.) Problems of decidability and safety in databases 14:35 Jean-Jacques Levy (INRIA, France) Explicit substitutions and Pascal compiling schemes 15:10 Break 15:40 Robert Constable (Cornell U. and Weizmann Inst.) Constructive type theory as a foundation for computer science 16:15 Gordon D. Plotkin (Edinburgh U.) Resumption semantics for dataflow nets 16:50 End of session 17:00-18:30 RECEPTION (in front of Schreiber Bldg.) TUESDAY June 11 9:00 REGISTRATION 9:30 B.A. (Boaz) Trakhtenbrot (Tel-Aviv U.) To be announced 10:20 Break 10:40 Alex Rabinovich (IBM Watson, USA) The consequence relation of process logic 10:15 Albert R. Meyer (MIT) Systems of concurrent automata 11:50 Vaughan Pratt (Stanford U.) Must schedule-automaton duality entail conflict persistence? 12:25 LUNCH break 14:15 Amir Pnueli (Weizmann Inst.) Fair completeness without ordinals 14:50 Wolfgang Reisig (TU Munich) Concurrent temporal logic 15:25 Break 15:55 Rob van Glabbeek (Stanford U.) Bisimulation semantics for higher-dimensional automata 16:30 Manfred Broy (TU Munich) A functional calculus for nondeterministic interactive systems 17:05 Samson Abramsky (Imperial College, London) Proofs as processes 17:40 End of session WEDNESDAY June 12 9:00 REGISTRATION 9:30 Rusins Freivalds (U. Latvia) Advantages and limitations on advantages of probabilistic machines 10:05 Leonid Levin (Boston U.) Probability in computing 10:40 Break 11:10 Klaus Wagner (U. Wuerzburg, Germany) Complexity classes defined by the local behaviour of nondeterministic machines 11:45 Zvi Galil (Tel-Aviv U. and Columbia U.) Parallel string matching, upper and lower bounds 12:20 LUNCH break 14:15 Nachum Dershowitz (U. Illinois) Infinite rewriting 14:50 Val Breazu-Tannen (U. Pennsylvania) Law-abiding constructors 15:25 Break 15:55 V. Yu. Sazonov (Program Sys. Inst., Pereslavl-Zalessky, USSR) Some dependence-independence, conservativity and expressibility results on weak theories without exponentiation 16:30 Yuri Gurevich (U. Michigan) Evolving algebras 17:05 End of Symposium 20:00 BANQUET The public is invited to attend the lectures and reception without charge. A limited number of banquet tickets may be purchased at registration. Lectures will be 30 minutes long plus 5 minutes for questions and will be held in the Wladimir Schreiber Institute of Mathematics, Room 006, Tel-Aviv University, Ramat Aviv (by the Diaspora Museum). Parking through Gate 1. There will be a post-symposium excursion on Thursday, June 13. SYMPOSIUM CHAIR: Albert R. Meyer (MIT) ORGANIZING COMMITTEE: Zvi Galil (Tel-Aviv U.), Albert R. Meyer (MIT), Amir Pnueli (Weizmann Inst.), Amiram Yehudai (Tel-Aviv U.) Direct inquiries to the ORGANIZING CHAIR: Prof. Amiram Yehudai Computer Science Department Tel-Aviv University Tel-Aviv, Israel 69978 Phone: +972-3-5450037 (office) +972-3-5450040 (messages) +972-3-6423307 (home) FAX: +972-3-6422378 TELEX: 342171 VERSY IL EMAIL: amiram@taurus.bitnet, amiram@math.tau.ac.il Subject: CT91 Schedule Date: Mon, 13 May 91 08:54:20 EDT From: fox@triples.Math.McGill.CA (Thomas F. Fox) PRELIMINARY SCHEDULE OF "CATEGORY THEORY 1991" June 23-30, 1991 McGill University, Montreal Sunday, June 23 1:00-6:00 Registration in Bronfman Bldg. 8:00 (PM) Reception in Thompson House Monday, June 24 8:30 Registration in Bronfman Bldg 9:30 Abramsky, Samson: TBA 11:00 Carboni, Aurelio: Recent developments on affine and Mal'cev categories A:1:30 Chen, Hong (Andy): Categorical programming languages 2:05 Bonacina, M. Paola: A category theory approach to completion-based theorem proving strategies 2:40 Mulry, Philip S.: Strong monads, algebras and fixed points 3:40 Blute, Richard: Linear logic, coherence theorems and dinaturality 4:15 Rosebrugh, Robert: Relational databases and indexed categories B:1:30 Diers, Yves: A new universal construction in the category of commutative rings 2:05 Dula, Giora: A functor from groupoids to rings 2:40 Borceux, Francis: Morita theory for algebraic theories 3:40 Bourn, Dominique: Normalization equivalence, kernel equivalence and affine categories 4:15 Pedicchio, M.C.: Mal'cev categories Tuesday June 25 9:00 Lamarche, Francois: It is time to generalize Grothendieck toposes 10:30 Jardine, John F.: Homotopy theory and coherence A:1:00 Otto, James: Higher order initial models I: from fl to lcc 1:35 Freyd, Peter: Formal Methods 2:10 Rumbos, Beatriz: Transition probability and non-commutativity of states 3:10 Cockett, Robin: The fundamental theorem of data structures for a locos B:1:00 Hardie, Keith: Comparing the classical and coherent homotopy sets under A and over B 1:35 Steiner, Richard: Nerves and tensor products of multiple categories 2:10 Moerdijk, Ieke: Diaconescu's theorem and classifying spaces 3:10 Tierney, Myles: TBA 3:45 Joyal, Andre: TBA 4:20 Bunge, Marta: Indexed categories and distributions on toposes Wednesday June 26 9:00 Pitts, Andrew: Toposes and Heyting algebras 10:30 Isbell, John: Descriptive local theory A:1:00 Lozanov, Rumen: Kleene's theorem for categories 1:35 Benabou, Jean: Some aspects of definability 2:10 Reyes, Gonzalo: TBA 3:10 Picado, Jorge: On two extensions of Dickson's torsion theory B:1:00 Janelidze, Georg: Higher dimensional galois theory: the first version 1:35 Gordon, Robert: Categories enriched over closed bicategories 2:10 Kelly, Gregory M.: Closed and cartesian closed bicategories 3:10 MacDonald, John: Soft adjunctions and 2-level algebras 3:45 Datuashvili, Tamaz: On the category of internal categories in the category of groups with operations 7:00 BANQUET Thursday June 27 9:00 Trnkova, Vera: Functorial selection of morphisms 10:30 Wood, Richard: Adjoint quadra-modules EXCURSION Friday June 28 9:00 Street, Ross: Diagrams for tensor categories with duality 10:30 Pelletier, Joan: Quantales of linear relations A:1:00 Niefield, Susan: Quantales and Boolean quotients 1:35 Rosenthal, Kimmo: Quantaloidal nuclei - the syntactic congruence and tree automata 2:10 Roman, Leopoldo: Quantum logic and Girard quantales 3:10 Flagg, Robert: Quantales and continuity spaces 3:45 Zangurashvili, Dali: Some categorical algebraic properties of functors with values in categories without products 4:20 Squire, Richard: Maximally ordered objects in a topos B:1:00 Pachuashvili, Beso: Cohomologies of Steenrod algebra with coefficients in cohomologies of topological space 1:35 Grandis, Marco: Homological algebra in homological categories 2:10 Pachkoria, Alex: Homological algebra in the category of commutative monoids 3:10 MacLane, Saunders: Monoidal categories, coherence and quantum fields 3:45 Majid, Shahn: Braided groups and duals of monoidal categories 4:20 Lyubashenko, Vladimir: Rational modular tensor categories and CFT Saturday June 29 9:00 Moggi, Eugenio: The mathematical structure of programming languages 10:30 Meloni, Gian Carlo: Topological and relational semantics for predicative classical modalities A:1:00 Richter, Gunther: Categorical descriptions of categories of Hausdorff spaces 1:35 Ageron, Pierre: Cartesian closed categories of accessible categories 2:10 Hu, Hongde: Duality for some accessible categories 3:10 Nel, Louis D.: Existence theorems in analysis via categorical methods 3:45 Koslowski, Juergen: Hereditary and modal closure operators, hulls and cores B:1:00 Sobral, Manuela: Remarks on the change-of-base functor 1:35 Pavlovic, Dusko: Functional comprehension and relative toposes 2:10 Sun, Shu-Hao: Sheaf representations of universal algebras 3:10 Tavakoli, Javad: Omega-valued internal sheaves in a topos 3:45 Jarzembski, Grzegorz: Topological properties of free spectra of categories of mixed structures 4:20 Kock, Anders: Local equivalence relations and their sheaves __________________________________________________________ THE FINAL SCHEDULE WILL BE DETERMINED ON MONDAY JUNE 23. THE FOLLOWING TALKS ARE TENTATIVE: Bauer, F. W.: A strong shape category Betti, Renato: Algebraic categories over topoi Brown, Ronnie: Crossed Differential Graded Algebras Duskin, Jack: TBA Guitart, Rene: Classe caracteristiques des esquisses fibrees Hoehnke, Hans-Juergen: Loop categories Nassopoulos, George F.: An internal characterization of the base category V. Obtulowicz, Adam: Higher level families of structures & their applications Popescu, Nicolae: Valuations on K(X) Pumpluen, D.: Convex spaces Taylor, Paul: TBA Topencharov, Vladimir: Diagonal categories in double and n-tuple categories Trimble, Todd: TBA Vermeulen, Japie: Perfect descent Zawadowski, Marek: Descent techniques in categorical doctrines ALL TALKS WILL BE IN THE BRONFMAN BUILDING OF MCGILL UNIVERSITY AT 1001 SHERBROOKE W., MONTREAL THE RECEPTION SUNDAY EVENING WILL BE HELD IN THOMPSON HOUSE AT 3650 MCTAVISH ST. FURTHER INFORMATION: mt16@musica.mcgill.ca Subject: addresses Date: Wed, 15 May 91 16:53:22 +10 From: kelly_m@maths.su.oz.au (Max Kelly) Michael,Bob - has either of you email addresses for Banaschewski & for Harry Simmons? If not, how about fax or home telephone? Perhaps your BB, Bob. Thanks. Max, 15 May. Date: Fri, 17 May 91 12:37:22 +10 From: kelly_m@maths.su.oz.au (Max Kelly) Let a category A be locally finitely presentable, and let B be a full reflective subcategory for which the inclusion B ---> A is FINITARY - that is, preserves filtered colimits. Is there necessarily in A a set of arrows of the form k:M ---> N, where M and N are finitely presentable, such that B consists of the objects ORTHOGONAL to each k, in the sense that an object a of A is in B if & only if each A(k,a):A(N,a) ---> A(M,a) is invertible? It is easy to see that it suffices to answer the question when A is a presheaf category P; just express A as a finitarily reflective subcategory of such a P. It is of course true that B is locally finitely presentable, & is therefore expressible as the full subcategory of some presheaf category Q, given by the objects of Q orthogonal to a set of arrows between locally-presentables; that is not the point. Max Kelly, 17 May. Subject: Theor. Aspects of Software, Sendai, Japan, 9/24-27/91 Date: Mon, 20 May 91 13:23:34 EDT Reply-To: tacs91@ito.ecei.tohoku.ac.jp, tacs-request@theory.lcs.mit.edu PRELIMINARY PROGRAM and REGISTRATION International Conference on THEORETICAL ASPECTS OF COMPUTER SOFTWARE (TACS'91) September 24-27, 1991 Tohoku University, Sendai, Japan Sponsored by Tohoku University, Sendai, in cooperation with the Information Processing Society of Japan, the Japan Society for Software Science and Technology, the Association for Symbolic Logic, ACM SIGACT and the pending cooperation of the IEEETC on Mathematical Foundations of Computing and ACM SIGPLAN. CONFERENCE CO-CHAIRS Prof. Takayasu Ito Prof. Albert R. Meyer Department of Information Engineering MIT Laboratory for Computer Science Tohoku University 545 Technology Square, NE43-315 Sendai, Japan 980 Cambridge, MA 02139, USA email: tacs91@ito.ecei.tohoku.ac.jp email: tacs-request@theory.lcs.mit.edu FAX: 81 22 267 4404 FAX: (617) 253 3480 PROGRAM COMMITTEE Robert Constable (Cornell U.) Masami Hagiya (Kyoto U.) Susumu Hayashi (Ryukoku U.) Takayasu Ito, Co-Chair (Tohoku U.) J.-L. Lassez (IBM, Yorktown) Albert R. Meyer, Co-Chair (MIT) Gordon D. Plotkin (Edinburgh U.) Amir Pnueli (Weizmann Inst.) Masahiko Sato (Tohoku U.) Dana Scott (Carnegie-Mellon U.) CONFERENCE PROGRAM MONDAY 23 SEPTEMBER Autumnal Equinox Holiday 15:00-20:00 REGISTRATION at Sendai Tokyu Hotel 18:00-19:30 WELCOME RECEPTION at Sendai Tokyu Hotel TUESDAY 24 SEPTEMBER 9:30 OPENING SESSION Takayasu Ito, TACS Co-Chair (Tohoku U.) Albert R. Meyer, TACS Co-Chair (MIT) 10:00 INVITED TALK 1 On the completeness of type-checking Gordon D. Plotkin (Edinburgh U.) 10:50 BREAK 11:20-12:20 SESSION 1 11:20 Type inference in polymorphic type discipline Paola Giannini, Simona Ronchi Della Rocca (U. Torino) 11:50 Monotone recursive definition of predicates and its realizability interpretation Makoto Tatsuta (Tohoku U.) 12:20 LUNCH 13:30 INVITED TALK 2 Adding proof objects and inductive definition mechanisms to Frege structures Masahiko Sato (Tohoku U.) 14:20 BREAK 14:50-15:50 SESSION 2 14:50 From term models to domains Wesley Phoa (Cambridge U.) 15:20 An abstract interpretation of ML equality kinds Carl A. Gunter (U. Pennsylvania) Elsa L. Gunter, David B. MacQueen (AT&T Bell Laboratories) 15:50 BREAK 16:20-17:10 INVITED TALK 3 Full abstraction and the context lemma Albert R. Meyer (MIT Laboratory for Computer Science) 19:00-20:30 RECEPTION at Sendai Tokyu Hotel WEDNESDAY 25 SEPTEMBER 9:30-11:00 SESSION 3 9:30 An efficiency preorder for processes S. Arun-Kumar (Indian Institute of Technology) M. Hennessy (U. Sussex) 10:00 On nets, algebras and modularity Alexander Rabinovich (IBM T.J. Watson Research Center) Boris A. Trakhtenbrot (MIT and Tel Aviv U.) 10:30 Towards a complete hierarchy of compositional dataflow models Bengt Jonsson (Swedish Institute of Computer Science) Joost N. Kok (Utrecht U.) 11:00 BREAK 11:30 INVITED TALK 4 Constructive aspects of classical logics Robert L. Constable (Cornell U.) 12:20 LUNCH 13:30 INVITED TALK 5 Applying formal methods to software development--partially Amir Pnueli (Weizmann Institute of Science) 14:20 BREAK 14:50-15:50 SESSION 4 14:50 Proving termination of general Prolog programs Krzysztof R. Apt (CWI, Amsterdam) Dino Pedreschi (U. Pisa) 15:20 On abstraction and the expressive power of programming languages John C. Mitchell (Stanford U.) 15:50 BREAK 16:20-17:10 INVITED TALK 6 Role of logic programming in the FGCS project Kazuhiro Fuchi (ICOT, Tokyo) 19:00-21:00 BANQUET at Sendai Tokyu Hotel Banquet Speech by Rod Burstall (Edinburgh U.) THURSDAY 26 SEPTEMBER 9:30-11:00 SESSION 5 9:30 Authentication and delegation with smart-cards M. Abadi, M. Burrows, C. Kaufman, B. Lampson (DEC Systems Research Center, Palo Alto) 10:00 Data flow analysis as model checking Bernhard Steffen (RWTH--Aachen) 10:30 On the adequacy of dependence-based representations for programs with heaps Phil Pfeiffer (U. Wisconsin-Madison) Rebecca Parsons Selke (Rice U.) 11:00 BREAK 11:30 INVITED TALK 7 From programming-by-example to proving-by-example Masami Hagiya (Kyoto U.) 12:20 LUNCH 13:30 INVITED TALK 8 Programming with constraints Jean-Louis Lassez (IBM Watson Research Center) 14:20 BREAK 14:50-16:05 SESSION 6 14:50 Polynomial recursion analysis in Pascal like programs Dieter Armbruster (U. Stuttgart) 15:05 Complexity of proving program correctness Hardi Hungar (U. Oldenburg) 15:20 Some normalization properties of Martin-Lof's type theory, and applications David Basin (Edinburgh U.) Doug Howe (Cornell U.) 15:35 Parametricity of extensionally collapsed term models of polymorphism and their categorical properties Ryu Hasegawa (Kyoto U.) 15:50 Programs with continuations and linear logic Shin-ya Nishizaki (Kyoto U.) 16:05 BREAK 16:35-17:35 SESSION 7 16:35 PI-calculus semantics of object-oriented programming languages David Walker (U. Technology, Sydney) 16:50 Wrapper semantics of an object oriented programming language with state Andreas V. Hense (U. Saarlandes, Saarbrucken) 17:05 Sharing actions and attributes in modal action logic Mark Ryan, Jose Fiadeiro, Tom Maibaum (Imperial College, London) 17:20 First order data types and first order logic Ralf Treinen (U. Saarlandes, Saarbrucken) 17:35 BREAK WITH SANDWICH 19:00-20:30 EVENING SESSION 8 Demos and informal presentations FRIDAY 27 SEPTEMBER 9:30-11:00 SESSION 9 9:30 Principal type-schemes of BCI-lambda-terms Sachio Hirokawa (Kyushu U.) 10:00 Intersection and union types F. Barbanera, M. Dezani-Ciancaglini (U. Torino) 10:30 The coherence of languages with intersection types John C. Reynolds (Carnegie Mellon U.) 11:00 BREAK 11:30 INVITED TALK 9 Singleton, union and intersection types in program extraction Susumu Hayashi (Ryukoku U.) 12:20 LUNCH BREAK 13:30-14:30 SESSION 10 13:30 Subtyping + extensionality: confluence of beta-eta reduction in F_(<=) Pierre-Louis Curien (LIENS/CNRS, Paris) Giorgio Ghelli (U. Pisa) 14:00 An extension of system F with subtyping Luca Cardelli (DEC Systems Research Center, Palo Alto) Simone Martini (U. Pisa) John C. Mitchell (Stanford U.) Andre Scedrov (U. Pennsylvania) 14:30 BREAK 15:00 INVITED TALK 10 Will logicians be replaced by machines? Dana S. Scott (Carnegie-Mellon U.) 15:50-16:00 CLOSING SESSION Albert R. Meyer, TACS Co-Chair (MIT) Takayasu Ito, TACS Co-Chair (Tohoku U.) SATURDAY 28 SEPTEMBER Bus Tour to Hiraizumi and Matsushima 9:00 Depart Sendai Tokyu Hotel Hiraizumi (Chusonji Temple with Golden Pavilion) Lunch Matsushima (Famous Views of Pine-covered Islets, Zuiganji Temple) Dinner at a Japanese restaurant 20:30 Return Sendai Tokyu Hotel -------------------------------------------------------------------------- GENERAL INFORMATION TACS'91 will be held on the campus of Tohoku University, Sendai, Japan. Lectures will be presented in the Aoba Memorial Building, Faculty of Engineering located on the Aoba Hill about 3 km west of downtown Sendai. Receptions and a banquet will be held at the Sendai Tokyu Hotel, located in downtown Sendai. A post conference bus tour to Hiraizuki (Chusonji Temple with its golden pavilion) and Matsushima (famous views of pine-covered islets and Zuiganji Temple) will take place on September 28. Sendai is the largest city in the northern part of the Honshu Island of Japan, with a population of about 900,000. The city is known in Japan as the "City of Trees". It is 350 km north from Tokyo and less than 2 hours away by the Tohoku Bullet Train (Tohoku Shinkansen). Sendai is a modern, safe city with a temperate climate blessed by four distinct, beautiful seasons. Conference registration is open to the public. Reservations for the post conference bus tour will be limited. Register and make reservations by returning the completed form below by email, FAX, or airmail. There will also be on-site registration at: Sendai Tokyu Hotel, 15:00-20:00, September 23, Aoba Memorial Bldg., Tohoku Univ., 9:00-17:00 on September 24-27. A proceedings, published as a volume in Springer-Verlag's Lecture Notes in Computer Science, will be given to registrants on arrival. TRANSPORTATION Conference participants arriving at the new TOKYO INTERNATIONAL (NARITA) Airport are advised to take the JR Narita Express train from Narita Airport to Tokyo Station. Then take the Yamabiko super express train of Tohoku Shinkansen (Tohoku Bullet Train) to Sendai from Tokyo. The Yamabiko runs almost every 30 min. and takes less than 2 hours from Tokyo to Sendai. Making reservations at Narita Station for the Yamabiko express is strongly recommended, since it will be the autumnal tourist season. NOTE: No flight service is available from Narita Airport to Sendai Airport, since the train service is superior. The JR Narita Express is a new service started this March, and Tohoku Shinkansen from Tokyo Station is a new service starting at the end of this June. If you are going to travel in Japan before/after the conference it will be convenient and economical to get a JR PASS before your departure. Contact your travel agent for more information. Those arriving at OSAKA INTERNATIONAL Airport can fly to Sendai Airport, and take the Limousine Bus service to Sendai Station. The bus takes about 45 min. to go from the Airport to Sendai Station. You can also take the Tokaido Shinkansen from Osaka to Tokyo Station and change at Tokyo Station to Tohoku Shinkansen for Sendai. Three recommended hotels offer special discount rates to TACS'91 participants: the Sendai Tokyu Hotel, the Sendai Washington Hotel II, and the Sendai Fuji Hotel. They are 1.2 km west of Sendai Station and about 500 Yen by taxi from the station. The receptions and banquet will be held at the Sendai Tokyu Hotel. The other two hotels are located within 5 min. walk of the Sendai Tokyu. CLIMATE The weather in Sendai from the middle of September to the middle of October is usually delightful--mostly sunny with temperatures ranging from the low 50's F (10's C) to the low 70's F (20's C). A light jacket may be needed in the morning and evening. Rain, if any, would rarely be heavy. Date: Tue, 21 May 91 14:13:34 ADT Subject: Constructivity symposium Announcing a Summer Symposium ... CONSTRUCTIVITY IN COMPUTER SCIENCE June 19-22, 1991 San Antonio, Texas Sponsored by Trinity University The University of Chicago The Association for Symbolic Logic Top-Down Agenda: Wednesday, June 19 Friday, June 21 11 AM - 5 PM Registration 7 AM - 8 AM Breakfast 4 PM Welcome 8 AM - noon Paper Sessions 4:15 - 6 PM Paper Session noon - 1 PM Lunch 6:30 PM Reception and dinner 1 PM - 5 PM Paper Sessions 6:30 PM Reception & Banquet Thursday, June 20 Saturday, June 22 7 AM - 8 AM Breakfast 7 AM - 8 AM Breakfast 8 AM - noon Paper Sessions 8 AM - noon Paper Sessons noon - 1 PM Lunch noon Closing 1 PM - 5 PM Paper Sessions The following have been accepted for presentation in the final program: "Extracting Computational Content from Constructive and Classical Proofs," R.L. Constable (Cornell). "Constructive Topology and Combinatorics," T. Coquand (Chalmers Tekniska Hogskola). "Development Transformation Based on Higher Order Type Theory," Lu Jianguo & Xu Jiafu (Nanjing). "Constructivity Issues in Graph Algorithms," M. Langston (Tennessee) & M.R. Fellows (Victoria). "Kripke Semantics for Dependent Type Theory and Realizability," J. Lipton (Pennsylvania). "Classic Proofs as Programs: How, What, and Why," C. Murthy (Cornell). "Computational Logic," M. Napierala (Oregon Graduate Institute of Science and Technology). "Connecting Formal Semantics to Constructive Intuitions," M.J. O'Donnell (Chicago). "Reflective Semantics of Constructive Type Theory," S. Smith (Johns Hopkins). "Axiomatization of Calculus of Constructions," Yong Sun (York). "A Logical View of Assignments," V. Swarup (Mitre) & U.S. Reddy (Illinois at Urbana-Champaign). "Are Subsets Necessary in Martin-Lof Type Theory?" S. Thompson (Kent at Canterbury). "Examples of Semicomputable Sets of Real and Complex Numbers," J.V. Tucker (Swansea) & J.I. Zucker (McMaster). "Some Properties and Applications of the Lawson Topology," S. Yoccoz (Bordeaux). Three papers will constitute an additional "Curriculum Session": "Bringing Mathematics Education into the Algorithmic Age," N. Greenleaf (Columbia). "The Type Structure of CAT," R.E. Prather & J.P. Myers, Jr. (Trinity). "A Simple and Powerful Approach for Studying Constructivity, Computability, and Complexity," K. Weihrauch (Fernuniversitaet). FEES Registration $100 Housing & Meals One person (double occ.) $150 OR One person (single occ.) $180 Lodging, Sat. night $ 15 The symposium is "residential" to promote informal contacts. For someone not residing on-campus, a meal package is available for $45. FOR ADDITIONAL INFORMATION AND REGISTRATION FORMS, contact J. Paul Myers, Jr. Department of Computer Science PHONE: (512)736-7398 Trinity University E-MAIL (BITNET): San Antonio, Texas 78209 pmyers AT trinity USA -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= J. Paul Myers, Jr. Department of Computer Science Trinity University 715 Stadium Drive San Antonio, Texas 78212 (512) 736-7398 -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= Date: Wed, 22 May 91 17:23:43 MET DST From: curien@FRULM63.BITNET (Pierre-Louis Curien) Subject: CATEGORY THEORY AND COMPUTER SCIENCE 91 FOURTH BIENNAL CONFERENCE ON CATEGORY THEORY ANDCOMPUTER SCIENCE (C.T.C.S . ) 3- 6 September 1991 The Fourth of the Biennal Summer Conferences on Category Theory and Computer Science will be held in Paris (France). The main purpose of these conferences is to link research in category theory with computer science. The importance of categories in understanding basic issues in computer science is now well established. Other structures in logic, algebra and topology are also seen as fundamental and the scope of the conference is to cover applications of these structures as well. Proceedings are published in the Springer LNCS series. Organising and Programe Committee : Samson Abramsky, Pierre-Louis Curien, Peter Dybjer, Giuseppe Longo, John Mittchell, David Pitt, Andrew Pitts, Axel Poigne' , David Rydeheard, Don Sannella, Eric Wagner. Invited speakers Albert Burroni Eugenio Moggi Thierry Coquand Ugo Montanari Peter Freyd Robert Tennent Local Arrangements Office C.A.I.M.E.N.S / E.N.S. 45, rue dUUlm 75230 Paris Cedex 05 Te l : (33) (1 ) 43 29 12 25 ext. 3279 Fax : (33) (1) 46 34 05 31 Email : butery@dmi.ens.fr Person in charge : Chantal Butery Sponsorship : MRT (Ministe` re de la recherche et de la technologie), CNRS ( Centre national de la recherche scientifique), (MEN Minist re de l'e'ducation nationale ). Location : The conference will take place at : FIAP Jean Monnet 30, rue Cabanis 75014 Pa France (Me'ro station : Glacie`re) Accommodation, breakfast and self facilities for lunch or dinner will be provided by FIAP and are included in the registration fees (as well as a conference dinner). Accommodation : On the basis of students prices, the FIAP arranged for CTCS participants the possibility of booking double rooms to be shared or single rooms (in a limited number). Both types of rooms are provided with private shower, wash-basin, toilets and telephone. Other events : There will be a conference dinner. FIAP can also provide information on touristic or cultural activities in Paris and Paris area. Accommodation :Please fill and return your registration form to the Local Arrangements Office (CAIMENS / ENS), accompanied with a cheque of the corresponding amount in French Francs payable at CAIMENS. If you find it easier, you can also make a bank transfer to CAIMENS : Bank name and address : Soci e't e' Ge' ne' rale 37, rue Gay-Lussac, 75005 Paris. Account number : 00037266208 with the reference CTCS, and making sure that your name will appear clearly. Acknowledgment will be dispatched in due time. C.T.C.S. - 91 P R O G R A M M E Tuesday (September 3rd) 9:30 - 10:30 P. Freyd, invited talk 10:30 - 11:00 Coffee / Tea Break 11:00 - 11:40 T. Ehrhard & P. Malacaria, Stone Duality for Stable Functions 11:40 - 12:20 R. Amadio, Bifinite Domains: Stable Case Lunch 14:00 - 15:00 R. Tennent , invited talk 15:00 - 1540 A. Edalat & M. Smyth, Categories of Information Systems 15:40 - 16:10 Coffee / Tea Break 16:10 - 16:50 R. Hoofman & H.Schellinx, Collapsing Graph Models by Preorders 16:50 - 17:30 P. OUHearn, Linear Logic and Interference Control Wednesday (September 4th) 9:30 - 10:30 A. Burroni, Invited talk 10:30 - 11:00 Coffee / Tea Break 11:00 - 11:40 S. Hirokawa, BCK-formulas Having Unique Proofs 11:40 - 12:20 R. Blute, Proof Nets and Coherence Theorems Lunch Afternoon free Conference Dinner Thursday (September 5th) 9:30 - 10:30 E. Moggi, Invited talk 10:30 - 11:00 Coffee / Tea Break 11:00 - 11:40 G. Jarzembski, Programs in Partials Algebras - a Categorical Approach 11:40 - 12:20 B. Jay, Tail Recursion from Universal Invariants Lunch 14:00 - 15:00 T. Coquand, Invited talk 15:00 - 15:40 D. Pavlovic, Constructions and Predicates 15:40 - 16:10 Coffee / Tea Break 16:10 - 16:50 B. Jacobs, E. Moggi & T.Streicher Relating Models of Impredicative Type Theories 16:50 - 17:30 W. Phoa, Set-theoretic Polymorphism after Robinson Friday (September 6th) 9:30 - 10:30 U. Montanari, Invited talk 10:30 - 11:00 Coffee / Tea Break 11:00 - 11:40 E. Stark, Dataflow Networks are Fibrations 11:40 - 12:20 P. Degano,S. Kasangian & S.Vigna Applications of the Calculus of Trees to Process Description Languages Lunch END OF CONFERENCE Date: Fri, 24 May 91 16:57:15 ADT Subject: Kan extensions programs ------ kan ver 1.0 ------------------------------------------- Sean Carmody Craig Reilly Bob Walters 16th May 1991 -------------------------------------------------------------- An implementation of the algorithm developed in 1990 by Carmody & Walters to compute (finite) left Kan extensions is now operational (programmed by Reilly and Carmody). It is available by anonymous ftp from Sydney University: ftp maths.su.oz.au (NOTE "maths" not "math") There are also some sample input files as well as a file called KAN.info which gives further details of the program and one called README which describes the sample input files. If you experiment with the program, we would be very interested to hear any comments or suggestions (especially with regards any bugs which you -- hopefully won't -- find). Sean Carmody. (email: carmody_s@maths.su.oz.au) -------------------------------------------------------------- Date: Fri, 24 May 91 17:42:45 ADT From: fox@triples.Math.McGill.CA (Thomas F. Fox) Subject: CT91 Directions CATEGORY THEORY 1991 MORE INFORMATION FOR PARTICIPANTS June 23 - 30, 1991 McGill University, Montreal TALKS: Sixty-four talks have been scheduled, including twelve one hour talks by invited speakers and fifty-five half hour talks in parallel sessions. The first talk will be Monday, June 23 at 9:30. The last talk is scheduled for Saturday, June 29 at 4:20. All talks will be in the Bronfman Building of McGill University at 1001 Sherbrooke St. West. REGISTRATION: A registration desk will be set up in the Bronfman Building at 1001 Sherbrooke Street West on Sunday, June 23 from 1:00 to 6:00. You may also register at the reception Sunday evening or before the first talk on Monday. RECEPTION: On Sunday evening there will be a reception in Thompson House (the Graduate Student Centre) at 3650 McTavish from 8:00 to 11:00. Thompson House will be open to participants and their guests throughout the week as a relaxing meeting place. (If you are a member of a North American faculty club, the facilities of the McGill Faculty Club are also available. Bring your membership card.) BANQUET: There will be a banquet for participants on Wednesday evening. By June 20 we must know the number of people attending the banquet, so if you plan pay your registration fee only upon arrival, please confirm your participation by June 20. Guests (accompanying persons) are welcome at a cost of $35 per person. EXCURSIONS: On Thursday afternoon there will be two excursions available to participants and their guests - a picnic/walk in a nature preserve at Mt. St. Hilaire outside of the city, or a lunch and walking tour of Old Montreal. We will ask you sign up for one or the other at registration. There will be a small charge for accompanying persons. DIRECTIONS FROM AIRPORTS: Montreal has two airports, the North American airport at Dorval, and the International airport at Mirabel. From DORVAL: A taxi to McGill will cost $20. There is an airport bus (cost $8.50) at X:15 and X:45 which stops at the Queen Elizabeth Hotel, five blocks from McGill, ten blocks from the dorms. A taxi from the Queen E to McGill costs $3.50. From MIRABEL: A taxi to McGill will cost $50. There is an airport bus which costs $11.75, and goes to the Queen Elizabeth Hotel (see above). The bus leaves Mirabel on the hour 24 hours a day, and on the half hour from 12:30 to 19:30. BY TRAIN: Central Station is next door to the Queen Elizabeth Hotel, five blocks south of McGill. Take the escalator to Blvd. Rene Levesque and hail a cab or walk north, towards the mountain. BY CAR FROM THE US: From the US, cross the Champlain Bridge. Immediately after the toll booth exit to the right. Follow the signs that say "Centre Ville" and you will find yourself on University Street going north. DORMS: Guests staying in the McGill Dorms may go directly to Bishop Mountain Hall, located at 3935 University St (the northern end of University street). A night guard will be on duty to welcome late arrivals. There is (limited) parking in the dorm complex. We have maps and tourist information available upon request. If you have any questions or need further information, please contact us at the address given below. CATEGORY THEORY 1991 Math Dept, McGill University 805 Sherbrooke St W Montreal, Quebec CANADA H3A 2K6 Email: mt16@musica.mcgill.ca Fax: (1-514) 398-3899 Tel: (1-514) 398-3806 Date: Mon, 27 May 91 15:47:47 EDT From: barr@triples.Math.McGill.CA (Michael Barr) Subject: email address for Hugo Volger? Does anyone have? Michael