Date: Wed, 02 May 90 07:46:52 -0400

This is a reminder that the deadline for 
early (and cheaper!) registration for LICS '90 is  5/11/90.

Please, REGISTER AS SOON AS POSSIBLE (and send your check)!

LIMITED funding is still available for exceptional cases,
with priority given to students. Send mail to:


	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 -- SIGACT
	Association for Symbolic Logic
	European Association for Theoretical Computer Science


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.  [A LaTeX source for this
registration/program flyer will be emailed upon request.]

Other queries:

Registration: (215) 898-4405, jean@central.cis.upenn.edu
Campus Accomodations:   (215) 898-3547
Announcements:   lics@cs.cmu.edu


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

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


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

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


Last Name:___________________________________________________

First Name:__________________________________________________


Street Address:______________________________________________

City ________________________________________________________


Country _____________________________________________________




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


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.


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.


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.


MONDAY, June 4

SESSION 1. 9:00--10:40. Chair: John Mitchell.

Type reconstruction in finite-rank fragments of polymorphic 
	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 
	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)


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


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)


The life and work of Alan Turing,
	R. Gandy (Oxford)


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)



Academic Press, publisher of Information and Computation
GTE Laboratories
Hewlett-Packard Laboratories
IBM Research (Almaden and Yorktown Heights)
Mitre Corporation
The University of Pennsylvania
Xerox PARC


LICS General Chair: Albert R. Meyer

1990 Conference Chair: Jean Gallier

1990 Program Chair: John C. Mitchell

Publicity Chair: Daniel Leivant

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.


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.