arvind@utcsri.UUCP (Arvind Gupta) (03/03/87)
From: gries@gvax.cs.cornell.edu (David Gries)
Subject: Logics in Computer Science Conference
To: Possible attendees of Logics in Computer Science Conference
From David Gries and Dexter Kozen
25 February 1987
Below is a tentative --but quite close-to-being-fixed-- schedule for the
1987 Logics In Computer Science Conference, to be held in Ithaca 22-25 June.
Come and enjoy not only the conference but the beautiful finger-lakes region
at a wonderful time of the year. Information concerning registration for the
conference and other matters is being developed by Dexter and will be
distributed at a later date.
We are still undecided whether to have a "demonstration" session during
the conference, in which people could demonstrate their software systems
dealing with various aspects of logic. In order to make the decision, we
need input from you, and quite fast. If you know someone who might want
to demonstrate software, please email gries@gvax.cs.cornell.edu as soon as
possible, indicating (0) the software you would demonstrate, (1) the
computing equipment you need, and (3) the supporting system software needed
to run your software. We have available vaxes, microvaxes, suns,
dandelions, dandetigers, symbolics, RTs, macintoshes, and PCs.
If you know others that might want to demonstrate software, please give
them a copy of this note soon. A similar one is being sent to other people
as well as committee members).
Please print this announcement and give it to your colleagues.
Thanks very much.
Monday, 22 June 1987
09:00 Session Chair: A. Pnueli
Invited speaker: R. Milner
09:45 Break
10:00 Session Chair: L. Cardelli
Polymorphism is Conservative Over Simple Types.
V. Breazu-Tannen, A. Meyer
Order-Sorted Algebra Solves the Constructor-Selector Problem.
J. Goguen, J. Messeguer
Recursive Types and Type Constraints in Second-Order Lambda Calculus.
N. Mendler
Complete Type Inference for Simple Objects.
M. Wand
12:00 Lunch
13:30 Session Chair: D. Harel
Domain Theory in Logical Form.
S. Abramsky
On the Formal Semantics of Statecharts.
D. Harel, A. Pnueli, J. Schmidt, R. Sherman
Modeling Computations: A 2-Categorical Framework.
R. Seely
Partial Order Models of Concurrency and the Computation of Functions.
H. Gaifman, V. Pratt
15:30 Break
15:45 Session Chair: Y. Gurevich
Minimalism Subsumes Default Logic and Circumscription in Stratified
Logic Programming.
N. Bidoit, C. Froidevaux
Hereditary Harrop Formulas and Uniform Proof Systems.
D. Miller, G. Nadathur, A. Scedrov
Undecidable Optimization Problems for Database Logic Programs.
H. Gaifman, H. Mairson, Y. Sagiv, M. Vardi
17:15 Break
Tuesday, 23 June 1987
09:00 Session Chair: P. Scott
Invited speaker: J. Reynolds
09:45 Break
10:00 Session Chair: S. Brookes
The Power of Temporal Proofs.
M. Abadi
Proving Boolean Combinations of Deterministic Properties.
B. Alpern, F. Schneider
Reasoning with Many Processes
A. Sistla, S. German
On the Eventuality Operator in Temporal Logic
A. Sistla, L. Zuck
Verification of Concurrent Programs: The Automata-Theoretic Framework.
M. Vardi
12:30 Lunch
14:00 Program (wine-tour and picnic?)
Wednesday, 24 June 1987
09:00 Session Chair: J. Goguen
Invited speaker: to be announced
09:45 Break
10:00 Session Chair: M. Fitting
Partial Objects in Constructive Type Theory.
R. Constable, S. Smith
A Framework for Defining Logics.
R. Harper, F. Honsell, G. Plotkin
The Computational Behaviour of Girard's Paradox.
D. Howe
A Non-Type-Theoretic Definition of Martin-Lof's Types.
S. Allen
12:00 Lunch
13:30 Session Chair: G. Plotkin
The Hierarchy of Finitely Typed Functional Programs.
A. Kfoury, J. Tiuryn, P. Urzyczyn
Definability with Bounded Number of Bound Variables.
N. Immerman, D. Kozen
On Chain Logic, Path Logic, and First-Order Logic over Infinite
Trees.
W. Thomas
Full Abstraction and Expressive Completeness for FP.
J. Halpern, E. Wimmers
15:30 Break
15:45 Session Chair: A. Nerode
A Semantical Approach to Nonmonotonic Logics.
Y. Shoham
I'm OK if You're OK: On the Notion of Trusting Communication.
R. Faigin, J. Halpern
Hoare Logic for Lambda-Terms as Basis of Hoare Logic for Imperative
Languages.
A. Goerdt
17:15 Break
Thursday, 25 June 1987
09:00 Session Chair: G. Longo
Kripke-Style Models for Typed Lambda Calculus.
J. Mitchell, E. Moggi
Some Semantic Aspects of Polymorphic Lambda Calculus.
P. Freyd, A. Scedrov
X-Separability and Left-Invertibility in X-Calculus.
C. Bohm, E. Tronci
10:30 Break
10:45 Session Chair: J. Jouannaud
Inference Rules for Rewrite-Based First-Order Theorem Proving.
L. Bachmair
Theorem Proving Using Rigid E-Unification: Equational Matings.
J. Gallier, S. Raatz, W. Snyder
Solving Disequations.
C. Kirchner, P. Lescanne
Decidability of the Confluence of Ground Term Rewriting Systems.
M. Dauchet, T. Heuillard, P. Lescanne, S. Tison
12:45 Lunch