1. LICS 1986: Cambridge, Massachusetts

Proceedings of the Symposium on Logic in Computer Science (LICS '86), Cambridge, Massachusetts, June 16-18, 1986. IEEE Computer Society, ISBN 0-8186-0720-3

Invited Lecture

John Alan Robinson: Merging Functional with Relational Programming in a Reduction Setting (Abstract of an Invited Lecture). 2

Session 1

László Csirmaz, Bradd Hart: Program Correctness on Finite Fields. 4-10
Steven M. German, Edmund M. Clarke, Joseph Y. Halpern: True Relative Completeness of an Axiom System for the Language L4 (Abridged). 11-25
Bengt Jonsson, Zohar Manna, Richard J. Waldinger: Towards Deductive Synthesis of Dataflow Networks. 26-37
William C. Rounds, Robert T. Kasper: A Complete Logical Calculus for Record Structures Representing Linguistic Information. 38-43
Albert R. Meyer: Floyd-Hoare Logic Defines Semantics: Preliminary Version. 44-48

Session 2

Lennart Beckman, Rune Gustavsson, Annika Wærn: An Algebraic Model of Parallel Execution of Logic Programs. 50-57
Stephen D. Brookes: A Semantically Based Proof System for Partial Correctness and Deadlock in CSP. 58-65
Luís Monteiro, Fernando C. N. Pereira: A Sheaf-Theoretic Model of Concurrency. 66-76
David B. Benson, Ofer Ben-Shachar: Strong Bisimulation of State Automata. 77-81

Session 3

Christine Mohring: Algorithm Development in the Calculus of Constructions. 84-91
John S. Schlipf: How Uncomputable is General Circumscription? (Extended Abstract). 92-95
J. Shultis: The Design and Implementations of Intuit. 96-104
Ian A. Mason: Equivalence of First Order LISP Programs. Proving Properties of Destructive Programs via Transformation. 105-117

Invited Lecture

Anil Nerode: A Logician Looks at Expert Systems: Areas for Mathematical Research (Abstract of Invited Lecture). 120

Session 4

Roberto M. Amadio, Kim B. Bruce, Giuseppe Longo: The Finitary Projection Model for Second Order Lambda Calculus and Solutions to Higher Order Domain Equations. 122-130
Matthias Felleisen, Daniel P. Friedman, Eugene E. Kohlbecker, Bruce F. Duba: Reasoning with Continuations. 131-141
Carl A. Gunter: The Largest First-Order-Axiomatizable Cartesian Closed Category of Domains. 142-148
Joseph Y. Halpern, John H. Williams, Edward L. Wimmers: Good Rewrite Strategies for FP. 149-162
David A. Plaisted: The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations. 163-174

Session 5

Martín Abadi, Zohar Manna: A Timely Resolution. 176-186
Shang-Ching Chou, Hai-Ping Ko: On Mechanical Theorem Proving in Minkowskian Plane Geometry. 187-192
Joëlle Despeyroux: Proof of Translation in Natural Semantics. 193-205
Claude Kirchner: Computing Unification Algorithms. 206-216

Session 6

Mario Coppo, Maddalena Zacchi: Type inference and logical relations. 218-226
Thierry Coquand: An Analysis of Girard's Paradox. 227-236
Todd B. Knoblock, Robert L. Constable: Formalized Metareasoning in Type Theory. 237-248
N. P. Mendler, Prakash Panangaden, Robert L. Constable: Infinite Objects in Type Theory. 249-255

Invited Lecture

Jean-Yves Girard: Quantitative and Qualitative Semantics (Abstract of Invited Lecture). 258

Session 7

Michael C. Browne: An Improved Algorithm for the Automatic Verification of Finite State Systems Using Temporal Logic. 260-266
E. Allen Emerson, Chin-Laung Lei: Efficient Model Checking in Fragments of the Propositional Mu-Calculus (Extended Abstract). 267-278
Joseph Y. Halpern, Yoav Shoham: A Propositional Model Logic of Time Intervals. 279-292
Johann A. Makowsky, Ildikó Sain: On the Equivalence of Weak Second Order and Nonstandard Time Semantics For Various Program Verification Systems. 293-300
Dominique Perrin, Paul E. Schupp: Automata on the Integers, Recurrence Distinguishability, and the Equivalence and Decidability of Monadic Theories. 301-304

Session 8

Roni Rosner, Amir Pnueli: A Choppy Logic. 306-313
Rohit Parikh: Levels of Knowledge in Distributed Computing. 314-321
Amir Pnueli, Lenore D. Zuck: Probabilistic Verification by Tableaux. 322-331
Moshe Y. Vardi, Pierre Wolper: An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report). 332-344

Session 9

Leo Bachmair, Nachum Dershowitz, Jieh Hsiang: Orderings for Equational Proofs. 346-357
Jean-Pierre Jouannaud, Emmanuel Kounalis: Automatic Proofs by Induction in Equational Theories Without Constructors. 358-366
Deepak Kapur, David R. Musser: Inductive Reasoning with Incomplete Specifications (Preliminary Report). 367-377
Richard Statman: On Translating Lambda Terms into Combinators; The Basis Problem. 378-382