The Latex source of the complete registration/ program flyer will be emailed upon request. Fifth Annual IEEE Symposium on Logic in Computer Science June 4-7, 1990 Philadelphia, PA Sponsored by IEEE Technical Committee on Mathematical Foundations of Computing in cooperation with Association for Computing Machinery Association for Symbolic Logic European Association for Theoretical Computer Science INQUIRIES: --------- Email registration forms followed by regularly posted checks will be gratefully received. Further travel information will be sent by email upon request to lics@cs.cmu.edu. Other queries: Registration: (215) 898-4405, jean@central.cis.upenn.edu Campus Accomodations: (215) 898-3547 Announcements: lics@cs.cmu.edu ON-CAMPUS ACCOMODATIONS ======================= Conference accomodations are available both on campus and at a commercial hotel. The conference auditorium is located half way between the two, five minutes walk from either one. Campus accomodations will be in Harnwell House, 3820 Locust Walk, a 26 story air-conditioned residence hall, with a permanently staffed front desk. Conference participants will be lodged in furnished 2--4 bedroom apartments with a shared bathroom, some with a living room and/or kitchenette, no television or phone. Pay phones are available in the lobby. A limited number of private apartments are available for married couples. On-campus room and board are available only as a package for lodging from Sunday the 3rd (check in time 3 pm) to Thursday the 7th (check out 1 pm) with meals from breakfast on Monday to lunch on Thursday. A meal-only package for those staying elsewhere is available with registration, and will also be available on a limited basis at the start of the conference. For campus accommodations information contact: Conference Housing Office, 3901 Locust Walk, Philadelphia, PA 19104-6180, (215) 898-3547 HOTEL ACCOMMODATIONS ==================== A limited number of rooms have been reserved at a reduced rate at the Penn Tower Hotel. The rate is $77 for single or double occupancy. One or two children, 12 or younger, may stay with parent(s) free of charge. This rate is available from Sunday June 3rd to Thursday the 7th. Reservations should be addressed directly to: Penn Tower Hotel Civic Center Boulevard at 34th Street Philadelphia, PA 19104-4385 (800) 356-7366, or (215) 387-8333 The last day for reservation at conference rate is May 3rd. A one night deposit is required by personal check in $US or by a major credit card. In correspondence with the hotel please indicate dates of arrival and departure. REGISTRATION AND CAMPUS ACCOMODATION FORM ========================================= Registration fees include conference proceedings and all events. Subsidies from institutional sponsors allow the LICS organizers to offer full participation privileges to student registrants. The reduced rate applies to authors, members of a sponsoring organization (IEEE Computer Society, ACM, EATCS, ASL), and members of the organizing and program committees. Early registration deadline is May 11. Cancellations after May 11 will be subject to a $25 charge for campus housing, and to a $25 charge for LICS registration. Fees are non-refundable after May 18. The LICS Organizers have limited funds available for subsidy of attendees unable to obtain travel grants. Persons desiring such subsidy should contact the Conference Chair, indicating their circumstances and amount of subsidy desired. By May 11 After May 11 Full $260 $330 Reduced $210 $270 Full-time student $60 $100 PLEASE TYPE OR PRINT: Last Name:___________________________________________________ First Name:__________________________________________________ Affiliation:_________________________________________________ Street Address:______________________________________________ City ________________________________________________________ State/Zip:___________________________________________________ Country _____________________________________________________ Phone(s):____________________________________________________ E-mail:______________________________________________________ PLEASE FILL IN AND CHECK AS APPROPRIATE: Reason for reduced rate:_____________________________________ Full-time student at: _______________________________________ Reservation request: Single Married couples Campus Housing $176 $352 Meal Package only $56 O Male O Female O Smoker O Non-smoker O Vegetarian O I'll room with____________________________________________ Return this form with a check in $US, for the total of your registration and optional package, made out to "IEEE Fifth LICS Symposium", to LICS, c/o J. Gallier Dept. of Computer & Information Science University of Pennsylvania 200 South 33rd Street Philadelphia, PA 19104-6389 DISCOUNTED FLIGHTS ================== USAir has been designated as the official carrier of LICS '90, and will offer to LICS '90 participants discounts for travel to Philadelphia from the continental US and Canada, during the period June 1--10, 1990. For travel from the continental US, (excluding first class and government contract fares), subject to applicable fare restrictions, For travel from Canada, with a 2 night minimum stay requirement. There may be discounts on other USAir international fares. To obtain a USAir fare discount, you or your travel agent should call USAir's Convention Office, at (800) 334-8644 (Monday through Friday, 8 am -- 9 pm EST), and refer to Gold File No. 393570. From Canada call (800) 428-4322, ext. 7702. CONFERENCE EVENTS ================= Registration Desk: ----------------- A registration desk will operate in the Penn Tower Hotel on Sunday, June 3, 7 -- 9:30 pm. From Monday through Wednesday, there will be a registration and information desk outside Meyerson Hall Auditorium, from 8:30 am to 5 pm. Talks: ----- All technical talks will be presented in Meyerson Hall Auditorium, in the basement of the Fine Arts Building. Contributed talks will be 20 minutes long, with 5 additional minutes for questions. Session 6 is a special session of invited papers on Automated Deduction, organized by Mark Stickel. These presentations will be 30 minutes long. Sunday Reception: ---------------- On June 3 there will be a welcome reception from 7 to 9:30 pm, at the Penn Tower Hotel. Free soft drinks and light snacks will be served, and a cash bar will be available. Monday Reception and Business Meeting: ------------------------------------- On June 4 there will be a reception at the University Museum (at 33rd and Spruce Streets), in the Upper Egyptian Gallery and Chinese Rotunda, with drinks and light dinner buffet from 6:30 to 8:30 pm. A business meeting for all attendees will follow from 8:30 pm with wine and soft drinks. Wednesday Banquet: ----------------- On June 6 there will be a banquet at the Franklin Institute.

From 6:30 pm you are invited to visit scientific exhibits at the Institute. The banquet will start around 7:30 pm, and will include a historical talk about Alan Turing, by Robin Gandy of Oxford University.

****************** CONFERENCE PROGRAM ****************** MONDAY, June 4 -------------- SESSION 1. 9:00--10:40. Chair: John Mitchell. --------- Type reconstruction in finite-rank fragments of polymorphic lambda-calculus, A.J. Kfoury (Boston U) & J. Tiuryn (Warsaw) Polymorphism, set theory, and call-by-value, E. Robinson (Sussex) & G. Rosolini (Parma) Universal domains in the theory of denotational semantics of programming languages, M. Droste & R. G"obel (Essen) The classification of continuous domains, A. Jung (TH Darmstadt & Imperial Coll.) SESSION 2. 11:10--12:25. Chair: Krzysztof Apt. --------- A decision procedure for a class of set constraints, N. Heintze (CMU) & J. Jaffar (IBM/Watson) A constraint sequent calculus, J.-L. Lassez (IBM/Watson) & K. McAloon (CUNY) Solving inequations in term algebras, H. Comon (Paris XI) SESSION 3. 2:25--3:40. Chair: Jon Barwise. --------- The dynamic logic of permission, R. van der Meyden (Rutgers) A theory of non-monotonic rule systems, W. Marek (Kentucky) & A. Nerode (Cornell) The semantics of reflected proof, S. Allen, R. Constable, D. Howe & W. Aitken (Cornell) SESSION 4. 4:20--6:00. Chair: Glynn Winskel. --------- Equation solving through an operational semantics of context, K. Larsen & L. Xinxin (Aalborg) Three logics for branching bisimulation, R. De Nicola (IEI-CNR) & F. Vaandrager (CWI) Reactive, generative, and stratified models of probabilistic processes, R. van Glabbeek (CWI), S. Smolka (Stony Brook), B. Steffen (Aarhus) & C. Tofts (Edinburgh) The nonexistence of finite axiomatisations for CCS congruences, F. Moller (Edinburgh) TUESDAY, June 5 --------------- SESSION 5. 9:00--10:40. Chair: Steve Cook. --------- 0-1 Laws for infinitary logics, Ph. Kolaitis (UCSC) & M. Vardi (IBM/Almaden) Implicit definability on finite structures and unambiguous computations, Ph. Kolaitis (UCSC) Alogtime and a conjecture of S.A. Cook, P. Clote (Boston Coll.) On the expression of monadic second-order graph next properties without quantifications over sets of edges, B. Courcelle (Bordeaux I) SESSION 6. 11:10--12:40. Chair: Mark Stickel. special session on automated deduction -------------------------------------- Searching for fixed point combinators with the kernel method, W. McCune (Argonne NL) Theorem proving with ordered equations, N. Dershowitz (Illinois/Urbana) Automated reasoning in geometry using algebraic methods, S.-Ch. Chou (UT/Austin) SESSION 7. 2:25--3:40. Chair: Ugo Montanari. --------- Normal process representatives, V. Gehlot & C. Gunter (U Penn) A categorical linear framework for Petri nets, C. Brown & D. Gurr (Edinburgh) A linear semantics for allowed logic programs, S. Cerrito (Paris XI) SESSION 8. 4:20--6:00. Chair: Jean-Pierre Jouannaud. --------- Programming in equational logic: beyond strong sequentiality, R.C. Sekar & I.V. Ramakrishnan (Stony Brook) The theory of ground rewrite systems is decidable, M. Dauchet & S. Tison (Lille-Flandres-Artois) Well rewrite orderings, P. Lescanne (CRIN) A constructive proof of Higman's Lemma, C. Murthy & J. Russell (Cornell) WEDNESDAY, June 6 ----------------- SESSION 9. 9:00--10:40. Chair: Jean Gallier. --------- Syntactic theories and unification, C. Kirchner & F. Klay (INRIA/Lorraine & CRIN) Proof transformations for equational theories, T. Nipkow (Cambridge) A new AC unification algorithm with an algorithm for solving diophantine equations, A. Boudet, E. Contejean & H. Devie (Paris XI) On subsumption and semiunification in feature algebras, J. D"orre (Stuttgart) & W. Rounds (U Michigan) SESSION 10. 11:10--12:25. Chair: Susumu Hayashi. ---------- Completeness for typed lazy inequalities, S. Cosmadakis (IBM/Watson), A.R. Meyer (MIT) & J. Riecke (MIT) Conditional lambda-theories and the verification of static properties of programs, M. Wand & Zh.-Y. Wang (Northeastern) Single-threaded polymorphic lambda calculus, J. Guzman & P. Hudak (Yale) SESSION 11. 2:25--3:40. Chair: Andre Scedrov. ---------- Extensional PERs, P. Freyd (U Penn), P. Mulry (Colgate), G. Rosolini (Parma) & D. Scott (CMU) A PER model of polymorphism and recursive types, M. Abadi (DEC/SRC) & G.D. Plotkin (Edinburgh) Effective domains and intrinsic structure, W. Phoa (Cambridge) SESSION 12. 4:20--6:00. Chair: Edmund Clarke. ---------- A logic of concrete time intervals, H. Lewis (Harvard) Real-time logics: complexity and expressiveness, R. Alur & T. Henzinger (Stanford) Explicit clock temporal logic, E. Harel, A. Pnueli & O. Lichtenstein (Weizmann) Model-checking for real-time systems, R. Alur (Stanford), C. Courcoubetis (Bell Labs) & D. Dill (Stanford) BANQUET ------- The life and work of Alan Turing, R. Gandy (Oxford) THURSDAY, June 7 ---------------- SESSION 13. 9:00--10:40. Chair: Paris Kanellakis. ---------- Symbolic model checking: 10^20 states and beyond, J.R. Burch, E.M. Clarke & K.L. McMillan (CMU); D.L. Dill & L.J. Hwang (Stanford) When is "partial" adequate? A logic-based proof technique using partial specifications, R. Cleaveland (NC State) & B. Steffen (Aarhus) Modelling shared state in a shared action model, K. Goldman & N. Lynch (MIT) On the limits of efficient temporal decidability, A. Emerson (UT/Austin & MCC), M. Evangelist (MCC) & J. Srinivasan (UT/Austin & MCC) SESSION 14. 11:10--12:25. Chair: Daniel Leivant. ---------- On the power of bounded concurrency: reasoning about programs, D. Harel (Weizmann), R. Rosner (Weizmann) & M. Vardi (IBM/Almaden) New foundations for fixpoint computations, R. Crole & A. Pitts (Cambridge) Recursive types reduced to inductive types, P. Freyd (U Penn) END OF CONFERENCE INSTITUTIONAL SPONSORS ---------------------- Academic Press, publisher of Information and Computation DEC SRC GTE Laboratories Hewlett-Packard Laboratories IBM Research (Almaden and Yorktown Heights) Mitre Corporation The University of Pennsylvania Xerox PARC CONFERENCE ORGANIZATION ======================= LICS General Chair: Albert R. Meyer 1990 Conference Chair: Jean Gallier 1990 Program Chair: John C. Mitchell Publicity Chair: Daniel Leivant PROGRAM COMMITTEE: ----------------- K.R. Apt, J. Barwise, E. Clarke, S. Cook, S. Hayashi, P. Kanellakis, J.-P. Jouannaud, D. Leivant, J.C. Mitchell (Chair), U. Montanari, A. Pitts, E. Sandewall, A. Scedrov, M. Stickel, and G. Winskel. ORGANIZING COMMITTEE: -------------------- M. Abadi, J. Barwise, A. Chandra, E. Dijkstra, E. Engeler, J. Gallier, J. Goguen, D. Gries, Y. Gurevich, D. Johnson, G. Kahn, J.W. Klop, D. Kozen, D. Leivant, Z. Manna, A.R. Meyer (General Chair), G. Mints, J.C. Mitchell, Y. Moschovakis, C. Papadimitriou, R. Parikh, G. Plotkin, G. Rozenberg, D. Scott, and R. de Vrijer.