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 BibTeX

Session 1

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

Session 2

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

Session 3

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

Invited Lecture

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

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 BibTeX
Matthias Felleisen, Daniel P. Friedman, Eugene E. Kohlbecker, Bruce F. Duba: Reasoning with Continuations. 131-141 BibTeX
Carl A. Gunter: The Largest First-Order-Axiomatizable Cartesian Closed Category of Domains. 142-148 BibTeX
Joseph Y. Halpern, John H. Williams, Edward L. Wimmers: Good Rewrite Strategies for FP. 149-162 BibTeX
David A. Plaisted: The Denotional Semantics of Nondeterministic Recursive Programs using Coherent Relations. 163-174 BibTeX

Session 5

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

Session 6

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

Invited Lecture

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

Session 7

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

Session 8

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

Session 9

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