LICS'94 Program and Registration

[This announcement is being sent to email lists.  Our apologies for
multiple copies.]

                     Ninth Annual IEEE Symposium
                    July 3-7, 1994, Paris, France


[This information is available on the world-wide web at
 Postscript, dvi, latex and plain text versions of the conference
 brochure are available via anonymous ftp from research.att.com in
 directory /dist/lics.]

Please address registration form and inquiries to

        LICS'94 Secretariat
        Claudie Thenault
        Relations Exterieures
        Domaine de Voluceau BP 105
        78153 Le Chesnay Cedex
            Phone: 33 (1) 39 63 56 75
            Fax: 33 (1) 39 63 56 38
            E-mail: symposia@inria.fr 

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".

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
            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

For cancellations made before June 1, payments will be refunded less
60FF for fees; no refunds will be made after June 1.

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

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.

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.

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.

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.

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)


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
    Witold Charatonik (Wroclaw) & Leszek Pacholski (Polish Academy of

10:25 Systems of set constraints with negative constraints are
    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
    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


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)



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)

    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)




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

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.


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.