2. LICS 1987: Ithaca, New York, USA

Invited Speaker

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

Session 1

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

Session 2

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

Session 3

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

Invited Speaker

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

Session 4

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

Invited Speaker

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

Session 5

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

Session 6

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

Session 7

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

Session 8

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

Session 9

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