2. LICS 1987: Ithaca, New York, USA

Invited Speaker

• Robin Milner: Some Uses of Maximal Fixed Points (Abstract of Invited Lecture). 3

Session 1

• Val Tannen, Albert R. Meyer: Polymorphism is conservative over simple types (Preliminary Report). 7-17
• Joseph A. Goguen, José Meseguer: Order-Sorted Algebra solves the Constructor-Selector, Multiple. 18-29
• N. P. Mendler: Recursive Types and Type Constraints in Second-Order Lambda Calculus. 30-36
• Mitchell Wand: Complete Type Inference for Simple Objects. 37-44

Session 2

• Samson Abramsky: Domain Theory in Logical Form. 47-53
• David Harel, Amir Pnueli, Jeanette P. Schmidt, Rivi Sherman: On the Formal Semantics of Statecharts (Extended Abstract). 54-64
• R. A. G. Seely: Modelling Computations: A 2-Categorical Framework. 65-71
• Haim Gaifman, Vaughan R. Pratt: Partial Order Models of Concurrency and the Computation of Functions. 72-85

Session 3

• Nicole Bidoit, Christine Froidevaux: Minimalism subsumes Default Logic and Circumscription in Stratified Logic Programming. 89-97
• Dale Miller, Gopalan Nadathur, Andre Scedrov: Hereditary Harrop Formulas and Uniform Proof Systems. 98-105
• Haim Gaifman, Harry G. Mairson, Yehoshua Sagiv, Moshe Y. Vardi: Undecidable Optimization Problems for Database Logic Programs. 106-115

Invited Speaker

• J. Reynolds: Conjunctive Types and Algol-like Languages. 119

Session 4

• Martín Abadi: The Power of Temporal Proofs. 123-130
• Bowen Alpern, Fred B. Schneider: Proving Boolean Combinations of Deterministic Properties. 131-137
• A. Prasad Sistla, Steven M. German: Reasoning with Many Processes. 138-152
• A. Prasad Sistla, Lenore D. Zuck: On the Eventuality Operator in Temporal Logic. 153-166
• Moshe Y. Vardi: Verification of Concurrent Programs: The Automata-Theoretic Framework. 167-176

Invited Speaker

• Maarten H. van Emden: First-order Predicate Logic as a Common Basis for Relational and Functional Programming (Abstract). 179

Session 5

• Robert L. Constable, Scott F. Smith: Partial Objects In Constructive Type Theory. 183-193
• Robert Harper, Furio Honsell, Gordon D. Plotkin: A Framework for Defining Logics. 194-204
• Douglas J. Howe: The Computational Behaviour of Girard's Paradox. 205-214
• Stuart Allen: A Non-Type-Theoretic Definition of Martin-Löf's Types. 215-221

Session 6

• A. J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn: The Hierarchy of Finitely Typed Functional Programs (Short Version). 225-235
• Neil Immerman, Dexter Kozen: Definability with Bounded Number of Bound Variables. 236-244
• Wolfgang Thomas: On Chain Logic, Path Logic, and First-Order Logic over Infinite Trees. 245-256
• Joseph Y. Halpern, Edward L. Wimmers: Full Abstraction and Expressive Completenes for FP. 257-271

Session 7

• Yoav Shoham: A Semantical Approach to Nonmonotic Logics. 275-279
• Ronald Fagin, Joseph Y. Halpern: I'm OK if You're OK: On the Notion of Trusting Communication. 280-292
• Andreas Goerdt: Hoare Logic for Lambda-Terms as Basis of Hoare Logic for Imperative Languages. 293-299

Session 8

• John C. Mitchell, Eugenio Moggi: Kripke-Style models for typed lambda calculus. 303-314
• Peter J. Freyd, Andre Scedrov: Some Semantic Aspects of Polymorphic Lambda Calculus. 315-319
• Corrado Böhm, Enrico Tronci: X-Separability and Left-Invertibility in lambda-calculus. 320-328

Session 9

• Leo Bachmair, Nachum Dershowitz: Inference Rules for Rewrite-Based First-Order Theorem Proving. 331-337
• Jean H. Gallier, Stan Raatz, Wayne Snyder: Theorem Proving Using Rigid E-Unification Equational Matings. 338-346
• Claude Kirchner, Pierre Lescanne: Solving Disequations. 347-352
• Max Dauchet, Sophie Tison, Thierry Heuillard, Pierre Lescanne: Decidability of the Confluence of Ground Term Rewriting Systems. 353-359