[This announcement is being sent to email lists. Our apologies for multiple copies.] LOGIC IN COMPUTER SCIENCE (LICS) ******************************** Ninth Annual IEEE Symposium July 3-7, 1994, Paris, France ADVANCE REGISTRATION AND PROGRAM INFORMATION ============================================ [This information is available on the world-wide web at http://www.research.att.com/lics/ Postscript, dvi, latex and plain text versions of the conference brochure are available via anonymous ftp from research.att.com in directory /dist/lics.] CONFERENCE OFFICE. ================= Please address registration form and inquiries to LICS'94 Secretariat Claudie Thenault INRIA-Rocquencourt Relations Exterieures Domaine de Voluceau BP 105 78153 Le Chesnay Cedex FRANCE Phone: 33 (1) 39 63 56 75 Fax: 33 (1) 39 63 56 38 E-mail: symposia@inria.fr REGISTRATION ============ The registration form should be sent to the conference office. Registration without payment (or purchase order) enclosed will not be considered. For early registration, payment must be received by June 5. Fees will be returned in full for any written cancellation received before June 24. No refund will be made after this date. A table of registration fees can be found on the registration form. The member rate applies to members of ACM, IEEE, EATCS and INRIA, members of the organizing and program committees and authors of accepted papers. The student rate applies to full time students; a copy of the registrant's 1993-94 student card should be included with the registration form. The registration fee includes conference participation, a copy of the proceedings, coffee breaks and an invitation to the welcome reception. There is a separate charge for the banquet. Payment must be in French currency, and can be made by bank cheque, postal cheque, or foreign draft made payable to "Agent Comptable de l'INRIA", by bank transfer to Tresorerie Generale des Yvelines, Versailles, account number 10071-78000-00044009 15389, by postal transfer to CCP Paris---30041-00001-09099 45 B 020-31, or by institutional purchase order. We have applied for permission to allow registration by credit card, and hope to have confirmation of this possibility by May 1. Participants wishing to use this facility should contact our office at that time, preferably by email addressed to symposia@inria.fr. Bank transfers should specify registrant's name and "Conference reference LICS94". ACCOMMODATION ============= Reservations can be made through the Wagonlit Travel Agency. The accommodation form should be sent with deposit before June 1 to: Wagonlit Travel Departement Congres & Evenements 50 Rue de Londres 75008 Paris FRANCE Tel: 33 (1) 44 90 33 10 Fax: 33 (1) 44 90 33 15 There are two categories of hotels available, as well as inexpensive student lodging (no age limit) in an international center in Clichy (north Paris). Paris is very popular in the summer, so reservations should be made as soon as possible. A deposit is compulsory for hotel reservations, and student lodging must be entirely prepaid. Payment must be in French currency, and can be made by bank cheque, Eurocheque, or foreign draft made payable to "Wagonlit Travel", by bank transfer to the account 00021935201/61 B.N.P. Paris Saint Lazare, bank code 30004, branch code 0819, "Wagonlit Travel---code comptable 04/670", or by credit card. Hotel deposits will be forwarded to the hotel less 60FF for reservation fees. The participant's bank charges must be added to the amount transferred. For cancellations made before June 1, payments will be refunded less 60FF for fees; no refunds will be made after June 1. LOCATION ======== The Conference is being hosted by the Conservatoire National des Arts et Metiers (CNAM) and will be part of its Bicentennial celebration. CNAM is a well-known engineering school where professionals are taught by professionals. It houses the famous Musee National Des Arts et Techniques, and is located at 292 Rue Saint Martin in the old center of Paris, on the right bank of the river Seine. It is walking distance from Les Halles, the Centre National d'Art et de Culture Georges-Pompidou (Beaubourg), the Hotel de Ville (City Hall) and the cathedral Notre-Dame de Paris. The nearest Metro station is Arts et Metiers. Paris normally enjoys pleasant summer weather in early July. Days are warm, but nights may be cool. For general information on Paris, contact the Paris Tourist Information Office, 127 Champs Elysees, 75008 Paris, phone number 33 (1) 49 52 53 54. RECEPTIONS ========== A Welcome Reception will be held on Sunday evening (17:00-19:00) in a gallery of CNAM. The Conference Banquet will be held in the palace housing the Senate, the upper chamber of the French Parliament. The palace was built in the beginning of the 17th century for Marie de Medicis, widow of King Henry IV. It is located in the well-known Jardins du Luxembourg. To reserve a place at the banquet, the appropriate column on the registration form must be marked; a banquet reservation on site will not be possible. LOCAL ARRANGEMENTS ================== Lunches are at the participants' own expense. Participants may eat in cafes and restaurants in CNAM's vicinity. Telephone messages will be delivered to participants during breaks. Access to email will be possible from CNAM. The organizers cannot be held liable to conference participants for injury, damage or loss of their personal property. It is suggested that participants make their own insurance arrangements. REGISTRATION DESK ================= A registration and information desk located at the conference site will operate on Sunday, July 3, from 15:00 to 18:00, and on the remaining conference days from 8:00 to 18:00. TRAVEL ====== Paris has two airports, Roissy-Charles de Gaulle, 30km north of Paris, and Orly, 20km south of Paris. A frequent Air France bus service goes from Roissy to Place Charles de Gaulle-Etoile or Porte Maillot in central Paris (the cost is about 48FF); from Orly the bus goes to Invalides and stops on demand at Montparnasse (32FF). There is also train service. From Roissy, the RER B line goes to Gare du Nord or Chatelet; from Orly, the Orlyval goes to Antony where there is a connection to the RER B (32FF). A taxi from Orly to central Paris costs about 150FF; from Roissy, 200FF. The Metro offers a convenient way to get around the city. Each trip (with unlimited transfers) costs one ticket. Tickets can be bought individually, but a carnet of 10 is more practical. RER lines to the suburbs connect with the Metro and cost more. Both Metro and RER tickets can be purchased from ticket booths or machines. A 40-45% discount may be obtained from AIR INTER for French domestic blue and white flights, depending on the days of departure. A voucher can be requested on the registration form. Participants requiring a visa for entry into France are strongly advised to make their application in their home countries at least two months prior to departure date. LICS'94 REGISTRATION FORM ************************* Last Name __________________________________________________ First Name _________________________________________________ Affiliation ________________________________________________ Street Address _____________________________________________ _______________________________________________________ City _______________________________________________________ State/Zip __________________________________________________ Country ____________________________________________________ Phone(s) ___________________________________________________ Fax ________________________________________________________ E-mail _____________________________________________________ REGISTRATION RATES. The fees below are in French currency and include 18.6% VAT. Please circle the applicable fees. through June 5 from June 6 Regular 2200 2600 Member 1700 2100 Student 1000 1200 Banquet 300 300 Total Fee ___________________________________________________ Rate justification __________________________________________ Full-time student at ________________________________________ I need an AIR INTER discount form: Yes / No Payment (circle one): Cheque (Bank/Foreign Draft) / Purchase Order / Bank Transfer (include copy) LICS'94 ACCOMMODATION FORM ************************** to be returned before Jun 1 Last Name __________________________________________________ First Name _________________________________________________ Company ____________________________________________________ Street Address _____________________________________________ _______________________________________________________ City _______________________________________________________ State/Zip __________________________________________________ Country ____________________________________________________ Phone(s) ___________________________________________________ Fax ________________________________________________________ 1A. HOTEL. Please reserve: *...twin bed room shared by 2 persons *...single room in a hotel of ________ stars, for ________ nights, from _________________ to _________________(a.m.). Average rates in French currency, per room and per night, room only, taxes and service included: Category Single/Twin Deposit 2** 385/500 460 3*** 550/700 760 1B. YOUTH HOSTEL. Please reserve: *...bed in a twin bed room, bathroom and toilets outside the room, compulsory stay of 4 nights (July 3 to 7, 1994), continental breakfast included, full prepayment compulsory, fixed rate per person 4 nights: 600FF. 2. PAYMENT. Deposit/prepayment of ____________ FF Circle one: Visa / Eurocard / Mastercard / Cheque (Bank/Euro/Foreign Draft) / Bank Transfer (include copy) Credit card # __________________________ Exp. __________ Signature _____________________________ Date ___________ CONFERENCE PROGRAM ****************** SUNDAY, July 3 ============== REGISTRATION (15:00-18:00) WELCOME RECEPTION (17:00-19:00) MONDAY, July 4 ============== REGISTRATION (8:00-9:00) OPENING ADDRESSES (9:00-9:25) INVITED LECTURE I (9:25-10:25) Chair: Robert Constable (Cornell) Rod Burstall (Edinburgh), Lambda-terms, proofs and refinement SESSION 1: FINITE MODEL THEORY (10:50-12:30) Chair: Daniel Leivant (Indiana) 10:50 McColm's Conjecture, Yuri Gurevich (Michigan), Neil Immerman (U Mass) & Saharon Shelah (Hebrew U & Rutgers) 11:15 The expressive power of finitely many generalized quantifiers, Anuj Dawar (Swansea) & Lauri Hella (Helsinki) 11:40 Generalized quantifiers for simple properties, Martin Otto (RWTH Aachen) 12:05 How to define a linear order on finite models, Lauri Hella (Helsinki), Phokion Kolaitis (UC Santa Cruz), & Kerkk Luosto (Helsinki) LUNCH (12:30-14:00) SESSION 2: CONCURRENCY (14:00-15:15) Chair: Vaughan Pratt (Stanford) 14:00 Finitary fairness, Rajeev Alur (Bell Labs) & Thomas Henzinger (Cornell) 14:25 Bisimulation is not (first-order) equationally axiomatisable, Peter Sewell (Edinburgh) 14:50 Foundations of timed concurrent constraint programming, Vijay Saraswat (Xerox PARC), Radha Jagadeesan (Loyola) & Vineet Gupta (Stanford) SESSION 3: SEMANTICS I (15:40-16:55) Chair: Achim Jung (Darmstadt) 15:40 A fully abstract semantics for concurrent graph reduction, Alan Jeffrey (Sussex) 16:05 An axiomatization of computationally adequate domain-theoretic models of FPC, Marcelo Fiore & Gordon Plotkin (Edinburgh) 16:30 On strong stability and higher-order sequentiality, Loic Colson & Thomas Ehrhard (Marne-la-Vallee) SESSION 4: DOMAIN THEORY (17:10-18:00) Chair: Carl Gunter (U Penn) 17:10 Linear types, approximation and topology, Michael Huth, Achim Jung & Klaus Keimel (Darmstadt) 17:35 Domain theory and integration, Abbas Edalat (Imperial Coll.) BUSINESS MEETING (20:00) TUESDAY, July 5 =============== TUTORIAL I (8:30-9:45) Chair: Moshe Vardi (Rice) Ed Clarke (CMU), Model Checking SESSION 5: CONSTRAINTS (10:00-10:50) Chair: Harald Ganzinger (MPI Saarbrucken) 10:00 Negative set constraints with equality: an easy proof of decidability, Witold Charatonik (Wroclaw) & Leszek Pacholski (Polish Academy of Sciences) 10:25 Systems of set constraints with negative constraints are NEXPTIME-complete, Kjartan Stefansson (Cornell) SESSION 6: MODAL AND TEMPORAL LOGICS I (11:15-12:30) Chair: Dexter Kozen (Cornell) 11:15 A compositional proof system for the modal mu-calculus, Hendrik Reif Andersen (TU Denmark), Colin Stirling (Edinburgh) & Glynn Winskel (Aarhus) 11:40 On the parallel complexity of model-checking in the modal mu-calculus, Shipei Zhang, Oleg Sokolsky & Scott Smolka (SUNY Stony Brook) 12:05 Complexity transfer for modal logic, Edith Hemaspaandra (Le Moyne) LUNCH (12:30-14:00) SESSION 7: TYPES I (14:00-15:15) Chair: Paris Kanellakis (Brown) 14:00 Typability and type-checking in the second-order lambda-calculus are equivalent and undecidable, J.B. Wells (Boston U) 14:25 Efficient inference of object types, Jens Palsberg (Northeastern) 14:50 Type inference and extensionality, Adolfo Piperno (Roma) & Simona Ronchi della Rocca (Torino) SESSION 8: CONSTRUCTIVE MATHEMATICS (15:40-16:55) Chair: Daniel Leivant (Indiana) 15:40 A groupoid model refutes uniqueness of identity types, Martin Hofmann (Edinburgh) & Thomas Streicher (LMU Muenchen) 16:05 A non-elementary speed-up in proof length by structural clause form transformation, Matthias Baaz, Christian Fermueller & Alexander Leitsch (TU Wien) 16:30 Upper and lower bounds for tree-like cutting planes proofs, Russell Impagliazzo (UC San Diego), Toniann Pitassi (UC San Diego) & Alasdair Urquhart (Toronto) SESSION 9: COMPLEXITY AND DATABASES (17:10-18:00) Chair: David McAllester (MIT) 17:10 The power of reflective relational machines, Serge Abiteboul (INRIA), Christos Papadimitriou (UC San Diego) & Victor Vianu (UC San Diego) 17:35 A syntactic characterization of NP-completeness, J. Antonio Medina & Neil Immerman (U Mass) EVENING LECTURE (19:30-20:30) Chair: Jean-Pierre Jouannaud (Paris Sud & CNRS) Corrado Boehm (Roma), An algebraic view of the lambda-calculus WEDNESDAY, July 6 ================= TUTORIAL II (8:30-9:45) Chair: Samson Abramsky (Imperial Coll.) Gerard Berry (CMA), The semantics of synchronous concurrent languages SESSION 10: LOGIC PROGRAMMING (10:00-10:50) Chair: Krzysztof Apt (CWI) 10:00 The declarative semantics of the Prolog selection rule, Robert Staerk (U Muenchen) 10:25 Semantics of meta-logic in an algebra of programs, Antonio Brogi & Franco Turini (Pisa) SESSION 11: LINEAR LOGIC (11:15-12:30) Chair: Samson Abramsky (Imperial Coll.) 11:15 A multiple-conclusion meta-logic, Dale Miller (U Penn) 11:40 Proof search in first-order linear logic and other cut-free sequent calculi, Patrick Lincoln & N. Shankar (SRI) 12:05 Linear logic, totality and full completeness, Ralph Loader (Oxford) LUNCH (12:30-14:00) SESSION 12: TYPES II (14:00-15:15) Chair: Frank Pfenning (CMU) 14:00 The emptiness problem for intersection types, Pawel Urzyczyn (Warsaw) 14:25 Subtyping and parametricity, Gordon Plotkin (Edinburgh), Martin Abadi (DEC SRC) & Luca Cardelli (DEC SRC) 14:50 On the Church-Rosser property for expressive type systems and its consequences for their metatheoretic study, Herman Geuvers (Nijmegen) & Benjamin Werner (Cornell & INRIA) SESSION 13: SEMANTICS II (15:40-16:55) Chair: Prakash Panangaden (McGill) 15:40 A semantics of object types, Martin Abadi & Luca Cardelli (DEC SRC) 16:05 Passivity and independence, Uday Reddy (Illinois) 16:30 A general semantics for evaluation logic, Eugenio Moggi (Genova) SESSION 14: CATEGORY THEORY (17:10-18:00) Chair: Glynn Winskel (Aarhus) 17:10 Reflexive graphs and parametric polymorphism, Edmund Robinson (Sussex) & Giuseppe Rosolini (Genova) 17:35 Categories, allegories and circuit design, Carolyn Brown (Sussex) & Graham Hutton (Chalmers) BANQUET THURSDAY, July 7 ================ INVITED LECTURE II (9:00-10:00) Chair: Gerard Huet (INRIA) Henk Barendregt (Nijmegen), Results and problems related to proof-checking SESSION 15: REWRITING (10:00-10:50) Chair: Jean-Pierre Jouannaud (Paris Sud & CNRS) 10:00 Rewrite techniques for transitive relations, Leo Bachmair & Harald Ganzinger, (Max-Planck-Institut) 10:25 Normalised rewriting and normalised completion, Claude Marche (CNRS & INRIA) SESSION 16: LAMBDA-CALCULUS (11:15-12:30) Chair: Jean-Jacques Levy (INRIA) 11:15 Modularity of strong normalization and confluence in the algebraic lambda-cube, Franco Barbanera (Torino), Maribel Fernandez (Paris Sud & CNRS), & Herman Geuvers (Nijmegen) 11:40 Cyclic lambda graph rewriting Zena Ariola (U Oregon) & Jan Willem Klop (CWI) 12:05 Paths in the lambda-calculus, Andrea Asperti (Bologna), Vincent Danos (CNRS & Paris 7), Cosimo Laneve (INRIA & CMA), & Laurent Regnier (CNRS) LUNCH (12:30-14:00) SESSION 17: MODAL AND TEMPORAL LOGIC II (14:00-15:15) Chair: Colin Stirling (Edinburgh) 14:00 A trace based extension of linear time temporal logic, P.S. Thiagarajan (SPIC Madras) 14:25 Axioms for knowledge and time in distributed systems with perfect recall, Ron van der Meyden (NTT Tokyo) 14:50 Compositional verification of real-time systems, Edward Chang (Stanford), Zohar Manna (Stanford), & Amir Pnueli (Weizmann Institute) SESSION 18: LOGIC IN ARTIFICIAL INTELLIGENCE (15:40-16:55) Chair: Peter Schroeder-Heister (Tuebingen) 15:40 Logical bilattices and inconsistent data, Ofer Arieli & Arnon Avron (Tel Aviv) 16:05 A modal logic for subjective default reasoning, Shai Ben-David & Rachel Ben-Eliyahu (Technion) 16:30 Language completeness of the Lambek calculus, Mati Pentus (Moscow State) SESSION 19: AUTOMATED DEDUCTION} (17:10-18:00) Chair: Gerard Huet (INRIA) 17:10 Rigid E-unifiability is NEXPTIME-complete, Jean Goubault (Bull) 17:35 Higher-order narrowing, Christian Prehofer (TU Muenchen) END OF CONFERENCE CONFERENCE ORGANIZATION *********************** LICS General Chair: Robert L. Constable 1994 Conference Co-chairs: Gerard Huet & Jean-Pierre Jouannaud 1994 Program Chair: Samson Abramsky Publicity Co-chairs: Amy Felty & Douglas Howe 1994 Local Arrangements: A. Theis-Viemont & C. Thenault PROGRAM COMMITTEE: ================== S. Abramsky, K. Apt, H. Ganzinger, C. Gunter, A. Jung, P. Kannelakis, D. Kozen, D. Leivant, J.-J. Levy, D. McAllester, P. Panangaden, F. Pfenning, V. Pratt, P. Schroeder-Heister, C. Stirling, G. Winskel. ORGANIZING COMMITTEE: ===================== M. Abadi, S. Abramsky, S. Artemov, A. Borodin, A. Bundy, S. Buss, E. Clarke, R. Constable (Chair), A. Felty, U. Goltz, Y. Gurevich, S. Hayashi, D. Howe, G. Huet, J.-P. Jouannaud, D. Kapur, C. Kirchner, P. Kolaitis, R. Kosaraju, D. Kozen, D. Leivant, A.R. Meyer, D. Miller, J. Mitchell, Y. Moschovakis, M. Okada, P. Panangaden, A. Pitts, G. Plotkin, J. Remmel, S. Ronchi della Rocca, G. Rozenberg, A. Scedrov, D. Scott, J. Tiuryn, M.Y. Vardi.