| 1986 | On Translating Lambda Terms into Combinators; The Basis Problem | Richard Statman |
| 1986 | The Design and Implementations of Intuit | J. Shultis |
| 1986 | How Uncomputable is General Circumscription? (Extended Abstract) | John S. Schlipf |
| 1986 | A Complete Logical Calculus for Record Structures Representing Linguistic Information | William C. Rounds, Robert T. Kasper |
| 1986 | A Choppy Logic | Roni Rosner, Amir Pnueli |
| 1986 | Merging Functional with Relational Programming in a Reduction Setting (Abstract of an Invited Lecture) | John Alan Robinson |
| 1986 | Probabilistic Verification by Tableaux | Amir Pnueli, Lenore D. Zuck |
| 1986 | The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations | David A. Plaisted |
| 1986 | Automata on the Integers, Recurrence Distinguishability, and the Equivalence and Decidability of Monadic Theories | Dominique Perrin, Paul E. Schupp |
| 1986 | Levels of Knowledge in Distributed Computing | Rohit Parikh |
| 1986 | A Logician Looks at Expert Systems: Areas for Mathematical Research (Abstract of Invited Lecture). | Anil Nerode |
| 1986 | A Sheaf-Theoretic Model of Concurrency | Lus Monteiro, Fernando C. N. Pereira |
| 1986 | Algorithm Development in the Calculus of Constructions | Christine Mohring |
| 1986 | Floyd-Hoare Logic Defines Semantics: Preliminary Version | Albert R. Meyer |
| 1986 | Infinite Objects in Type Theory | Nax Paul Mendler, Prakash Panangaden, Robert L. Constable |
| 1986 | Equivalence of First Order LISP Programs. Proving Properties of Destructive Programs via Transformation | Ian A. Mason |
| 1986 | On the Equivalence of Weak Second Order and Nonstandard Time Semantics For Various Program Verification Systems | Johann A. Makowsky, Ildik Sain |
| 1986 | Formalized Metareasoning in Type Theory | Todd B. Knoblock, Robert L. Constable |
| 1986 | Computing Unification Algorithms | Claude Kirchner |
| 1986 | Inductive Reasoning with Incomplete Specifications (Preliminary Report) | Deepak Kapur, David R. Musser |
| 1986 | Automatic Proofs by Induction in Equational Theories Without Constructors | Jean-Pierre Jouannaud, Emmanuel Kounalis |
| 1986 | Towards Deductive Synthesis of Dataflow Networks | Bengt Jonsson, Zohar Manna, Richard J. Waldinger |
| 1986 | Good Rewrite Strategies for FP | Joseph Y. Halpern, John H. Williams, Edward L. Wimmers |
| 1986 | A Propositional Model Logic of Time Intervals | Joseph Y. Halpern, Yoav Shoham |
| 1986 | The Largest First-Order-Axiomatizable Cartesian Closed Category of Domains | Carl A. Gunter |