3. LICS 1988: Edinburgh, Scotland, UK

Proceedings of the Third Annual Symposium on Logic in Computer Science (LICS '88), Edinburgh, Scotland, UK, July 5-8, 1988. IEEE Computer Society, ISBN 0-8186-0853-6

Session 1

Phokion G. Kolaitis, Moshe Y. Vardi: 0-1 Laws and Decision Problems for Fragments of Second-Order Logic. 2-11 BibTeX
Kevin J. Compton, Claude Laflamme: An Algebra and a Logic for NC¹. 12-21 BibTeX
Michael L. Tiomkin: Proving unprovability. 22-26 BibTeX

Invited Talk

C. A. R. Hoare, Michael J. C. Gordon: Partial Correctness of C-MOS Switching Circuits: An Exercise in Applied Logic. 28-36 BibTeX

Session 2

Kim B. Bruce, Giuseppe Longo: A Modest Model of Records, Inheritance and Bounded Quantification. 38-50 BibTeX
Roberto M. Amadio: A fixed point extension of the second order lambda-calculus: observable equivalences and models. 51-60 BibTeX
Paola Giannini, Simona Ronchi Della Rocca: Characterization of typings in polymorphic type discipline. 61-70 BibTeX

Session 3

A. J. Kfoury, Jerzy Tiuryn, Pawel Urzyczyn: On the Computational Power of Universally Polymorphic Recursion. 72-81 BibTeX
Val Tannen: Combining Algebra and Higher-Order Types. 82-90 BibTeX
Corrado Böhm, Adolfo Piperno: Characterizing X-Separability and One-Side Invertibility in lambda-beta-Omega-Calculus. 91-101 BibTeX

Session 4

Nachum Dershowitz, Mitsuhiro Okada: Proof-Theoretic Techniques for Term Rewriting Theory. 104-111 BibTeX
Gabriel M. Kuper, Ken McAloon, Krishna V. Palem, Kenneth J. Perry: Efficient Parallel Algorithms for Anti-Unification and Relative Complement. 112-120 BibTeX
Alexandre Boudet, Jean-Pierre Jouannaud, Manfred Schmidt-Schauß: Unification in Free Extensions of Boolean Rings and Abelian Groups. 121-130 BibTeX

Session 5

Mitchell Wand: Corrigendum: Complete Type Inference for Simple Objects. 132 BibTeX
Pierpaolo Degano, Rocco De Nicola, Ugo Montanari: On the Consistency of ``Truly Concurrent'' Operational and Denotational Semantics (Extended Abstract). 133-141 BibTeX
Glynn Winskel: A Category of Labelled Petri Nets and Compositional Proof System (Extended Abstract). 142-154 BibTeX
José Meseguer, Ugo Montanari: Petri Nets Are Monoids: A New Algebraic Foundation for Net Theory. 155-164 BibTeX
Martín Abadi, Leslie Lamport: The Existence of Refinement Mappings. 165-175 BibTeX

Session 6

Mads Dam: Relevance Logic and Concurrent Composition. 178-185 BibTeX
D. J. Walker: Bisimulations and Divergence. 186-192 BibTeX
Rance Cleaveland, Matthew Hennessy: Priorities in Process Algebras. 193-202 BibTeX
Kim Guldstrand Larsen, Bent Thomsen: A Modal Process Logic. 203-210 BibTeX

Session 7

Sergei G. Vorobyov: On the Arithmetic Inexpressiveness of Term Rewriting Systems. 212-217 BibTeX
Jean H. Gallier, Wayne Snyder, Paliath Narendran, David A. Plaisted: Rigid E-Unification is NP-Complete. 218-227 BibTeX
Leo Bachmair: Proof by Consistency in Equational Theories. 228-233 BibTeX

Invited Talk

Albert R. Meyer: Semantical Paradigms: Notes for an Invited Lecture, with Two Appendices by Stavros S. Cosmadakis. 236-253 BibTeX

Session 8

Thierry Coquand: Categories of Embeddings. 256-263 BibTeX
Thomas Ehrhard: A Categorical Semantics of Constructions. 264-273 BibTeX
Peter J. Freyd, Jean-Yves Girard, Andre Scedrov, Philip J. Scott: Semantic Parametricity in Polymorphic Lambda Calculus. 274-279 BibTeX

Session 9

Bard Bloom: Can LCF Be Topped? Flat Lattice models of Typed Lambda Calculus (Preliminary Report). 282-295 BibTeX
Robert Cartwright, Alan J. Demers: The Topology of Program Termination. 296-308 BibTeX
Carl A. Gunter, Achim Jung: Coherence and Consistency in Domains (Extended Outline). 309-317 BibTeX

Session 10

Rob Gerth, Michael Codish, Yossi Lichtenstein, Ehud Y. Shapiro: Fully Abstract Denotational Semantics for Flat Concurrent Prolog. 320-335 BibTeX
Marianne Baudinet: Proving Termination Properties of Prolog Programs: A Semantic Approach. 336-347 BibTeX
Michael J. Maher: Complete Axiomatizations of the Algebras of Finite, Rational and Infinite Trees. 348-357 BibTeX

Session 11

Robert L. Constable, Scott F. Smith: Computational Foundations of Basic Recursive Function Theory. 360-371 BibTeX
Timothy Griffin: Notational definition-a formal account. 372-383 BibTeX
Anne Salvesen, Jan M. Smith: The Strength of the Subset Type in Martin-Löf's Type Theory. 384-391 BibTeX
Paul F. Mendler, Peter Aczel: The notion of a Framework and a framework for LTC. 392-399 BibTeX

Session 12

Damian Niwinski: Fixed Points vs. Infinite Generation. 402-409 BibTeX
Ronald Fagin, Joseph Y. Halpern, Nimrod Megiddo: A Logic for Reasoning about Probabilities. 410-421 BibTeX
David E. Muller, Ahmed Saoudi, Paul E. Schupp: Weak Alternating Automata Give a Simple Explanation of Why Most Temporal and Dynamic Logics are Decidable in Exponential Time. 422-427 BibTeX
Michal Grabowski, Hardi Hungar: On the Existence of Effective Hoare Logics. 428-435 BibTeX