| 1987 | The Hierarchy of Finitely Typed Functional Programs (Short Version) | A. J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn |
| 1987 | Definability with Bounded Number of Bound Variables | Neil Immerman, Dexter Kozen |
| 1987 | The Computational Behaviour of Girard's Paradox | Douglas J. Howe |
| 1987 | A Framework for Defining Logics | Robert Harper, Furio Honsell, Gordon D. Plotkin |
| 1987 | On the Formal Semantics of Statecharts (Extended Abstract) | David Harel, Amir Pnueli, Jeanette P. Schmidt, Rivi Sherman |
| 1987 | Full Abstraction and Expressive Completenes for FP | Joseph Y. Halpern, Edward L. Wimmers |
| 1987 | Order-Sorted Algebra solves the Constructor-Selector, Multiple | Joseph A. Goguen, Jos Meseguer |
| 1987 | Hoare Logic for Lambda-Terms as Basis of Hoare Logic for Imperative Languages | Andreas Goerdt |
| 1987 | Theorem Proving Using Rigid E-Unification Equational Matings | Jean H. Gallier, Stan Raatz, Wayne Snyder |
| 1987 | Partial Order Models of Concurrency and the Computation of Functions | Haim Gaifman, Vaughan R. Pratt |
| 1987 | Undecidable Optimization Problems for Database Logic Programs | Haim Gaifman, Harry G. Mairson, Yehoshua Sagiv, Moshe Y. Vardi |
| 1987 | Some Semantic Aspects of Polymorphic Lambda Calculus | Peter J. Freyd, Andre Scedrov |
| 1987 | I'm OK if You're OK: On the Notion of Trusting Communication | Ronald Fagin, Joseph Y. Halpern |
| 1987 | First-order Predicate Logic as a Common Basis for Relational and Functional Programming (Abstract). | Maarten H. van Emden |
| 1987 | Decidability of the Confluence of Ground Term Rewriting Systems | Max Dauchet, Sophie Tison, Thierry Heuillard, Pierre Lescanne |
| 1987 | Partial Objects In Constructive Type Theory | Robert L. Constable, Scott F. Smith |
| 1987 | Polymorphism is conservative over simple types (Preliminary Report) | Val Tannen, Albert R. Meyer |
| 1987 | X-Separability and Left-Invertibility in lambda-calculus | Corrado Bhm, Enrico Tronci |
| 1987 | Minimalism subsumes Default Logic and Circumscription in Stratified Logic Programming | Nicole Bidoit, Christine Froidevaux |
| 1987 | Inference Rules for Rewrite-Based First-Order Theorem Proving | Leo Bachmair, Nachum Dershowitz |
| 1987 | Proving Boolean Combinations of Deterministic Properties | Bowen Alpern, Fred B. Schneider |
| 1987 | A Non-Type-Theoretic Definition of Martin-Lf's Types | Stuart Allen |
| 1987 | Domain Theory in Logical Form | Samson Abramsky |
| 1987 | The Power of Temporal Proofs | Martn Abadi |
| 1986 | An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report) | Moshe Y. Vardi, Pierre Wolper |