The Community for Technology Leaders
Logic in Computer Science, Symposium on (1995)
San Diego, California
June 26, 1995 to June 29, 1995
ISSN: 1043-6871
ISBN: 0-8186-7050-6
TABLE OF CONTENTS

Committees (PDF)

pp. xi
Invited Speaker I

A Complete Proof Systems for QPTL (Abstract)

Amir Pnueli , Department of Computer Science Weizmann Institute of Science, Israel
Yonit Kesten , Department of Computer Science Weizmann Institute of Science, Israel
pp. 2
Session 1: Program Logics I: Chair: D. Kozen

Completeness of Kozen's Axiomatisation of the Propositional Mu-Calculus (Abstract)

Igor Walukiewicz , BRICS, Department of Computer Science University of Aarhus
pp. 14

Once and For All (Abstract)

Orna Kupferman , Department of Computer Science The Technion, Israel
Amir Pnueli , Department of Computer Science Weizmann Institute of Science, Israel
pp. 25

Complete Proof Systems for First Order Interval Temporal Logic (Abstract)

Bruno Dutertre , Department of Computer Science, Royal Holloway, University of London, United Kingdom
pp. 36
Session 2: Finite Models I I: Chair: V. Tannen

The Infinitary Logic of Sparse Random Graphs (Abstract)

James F. Lynch , Clarkson University
Jerzy Tyszkiewicz , Mathematische Grundlagen der Informatik, Aachen, Germany
pp. 46

Generalized Quantifiers and 0-1 Laws (Abstract)

Anuj Dawar , Department of Computer Science University of Wales, Swansea, U.K.
Erich Grädel , Mathematische Grundlagen der Informatik, Aachen, Germany
pp. 54

Relativized Logspace and Generalized Quantifiers Over Finite Structures (Abstract)

Georg Gottlob , Institut fuer Informationssysteme Technische Universitaet Wien, Wien, Austria
pp. 65

First-Order Queries on Finite Structures Over the Reals (Abstract)

Jan Paredaens , University of Antwerp (UIA)
Jan Van den Bussche , INRIA Rocquencourt, France
Dirk Van Gucht , Indiana University
pp. 79
Session 3: Model Checking and Verification: Chair: P. Sistla

On the complexity of modular model checking (Abstract)

M.Y. Vardi , Dept. of Comput. Sci., Rice Univ., Houston, TX, USA
pp. 101
Invited Speaker II

The Semantic Challenge of Verilog HDL (Abstract)

Mike Gordon , University of Cambridge, U.K.
pp. 136
Session 4: Theorem. Proving and AI:Chair: T. Henzinger

Uniform proofs and disjunctive logic programming (Abstract)

G. Nadathur , Dept. of Comput. Sci., Chicago Univ., IL, USA
D.W. Loveland , Dept. of Comput. Sci., Chicago Univ., IL, USA
pp. 148

Structural Cut Elimination (Abstract)

Frank Pfenning , Department of Computer Science Carnegie Mellon University, Pennsylvania
pp. 156

Paramodulation without Duplication (Abstract)

Christopher Lynch , INRIA Lorraine et CRIN Campus Scientifique, Cedex France
pp. 167

Complexity of Normal Default Logic and Related Modes of Nonmonotonic Reasoning (Abstract)

A. Nerode , Mathematical Sciences Institute Cornell University, New York
V. W. Marek , Computer Science Department, University of Kentucky, Lexington, KY
J.B. Remmel , Mathematics Department, University of California, La Jolla, California
pp. 178
Session 5: Concurrency I: Chair: C. Brown

Control Structures (Abstract)

Robin Milner , Computer Laboratory, University of Cambridge UK
Alex Mifsud , Dept of Computer Science, University of Malta, Msida, Malta
John Power , Computer Science Dept, University of Edinburgh, UK
pp. 188

Configuration Structures (Abstract)

R.J. Van Glabbeek , Computer Science Department,Stanford University, Stanford, CA, USA
G.D. Plotkin , Department of Computer Science, University of Edinburgh, UK
pp. 199

A Typed Calculus of Synchronous Processes (Abstract)

Rajagopal Nagarajan , Imperial College of Science Technology and Medicine
Simon Gay , Imperial College of Science Technology and Medicine
pp. 210

Modal ?-Types for Processes (Abstract)

Marino Miculan , Dipartimento di Matematica ed Informatica, Universita di Udine, Via delle Scienze, Italy
Fabio Gadducci , Dipartimento di Informatica -- Universita di Pisa Corso Italia, Italy
pp. 221
Session 6: Semantics I: Chair: M. Abadi

Games and Full Abstraction for the Lazy Lambda-Calculus (Abstract)

Guy McCusker , Imperial College of Science, Technology and Medicine, London, United Kingdom
Samson Abramsky , Imperial College of Science, Technology and Medicine, London, United Kingdom
pp. 234

Domain Theory in Stochastic Processes (Abstract)

Abbas Edalat , Department of Computing, Imperial College, London
pp. 244

A Fully Abstract Semantics for a Concurrent Functional Language with Monadic Types (Abstract)

Alan Jeffrey , School of Cognitive and Computing Sciences,Sussex Univ., UK
pp. 255
Intited Speaker III
Session 7: Lambda Calculus amd Types: Chair: J. Tiuryn

Equality Between Functionals in the Presence of Coproducts (Abstract)

Daniel J. Dougherty , Department of Mathematics Wesleyan University USA
Ramesh Subrahmanyam , Department of Mathematics Wesleyan University USA
pp. 282

A logic of subtyping (Abstract)

K. Milsted , CNRS, Ecole Normale Superieure, Paris, France
S. Soloviev , CNRS, Ecole Normale Superieure, Paris, France
G. Loop , CNRS, Ecole Normale Superieure, Paris, France
pp. 292

Normalization and Extensionality (Abstract)

Adolfo Piperno , Universita di Roma "La Sapienza"
pp. 300

New Notions of Reduction and Non-Semantic Proofs of Strong Beta- Normalization in Typed Lambda Calculi (Abstract)

A.J. Kfoury , Boston University Department of Computer Science Boston, MA
J.B. Wells , Boston University Department of Computer Science Boston, MA
pp. 311
Session 8: Finite Models II: Chair: P. Kolaitis

Finitely Monotone Properties (Abstract)

Alexei P. Stolboushkin , Department of Mathematics University of California, Los Angeles
pp. 324

Tree Canonization and Transtive Closure (Abstract)

Kousha Etessami , Department of Computer Science University of Massachusetts at Amherst
Neil Immerman , Department of Computer Science University of Massachusetts at Amherst
pp. 331

Ptime Canonization for Two Variables with Counting (Abstract)

Martin Otto , Mathematische Grundlagen der Informatik, Germany
pp. 342

When do Fixed Point Logics Capture Complexity Classes? (Abstract)

Anil Seth , The Institute of Mathematical Sciences C.I.T. Campus, Madras-600113, INDIA
pp. 353
Session 9: Unification and Rewriting: Chair: L. Bachmair

Higher-order Unification via Explicit Substitutions (Abstract)

Therese Hardin , INRIA-Rocquencourt
Gilles Dowek , INRIA-Rocquencourt
Claude Kirchner , INRIA-Rocquencourt
pp. 366

Orderings, AC-theories and Symbolic Constraint Solving (Abstract)

A. Rubio , Technical Univ. Catalonia, Barcelona, Spain
H. Comon , CNRS, Univ. Paris-Sud, France
R. Nieuwenhuis , Technical Univ. Catalonia, Barcelona, Spain
pp. 375
Session 10 Model Checking II: Chair: EA. Emerson

Efficient On-the-Fly Model Checking for CTL (Abstract)

Rance Cleaveland , Department of Computer Science, North Carolina State University, Raleigh, NC
Girish Bhat , Department of Computer Science, North Carolina State University, Raleigh, NC
Orna Grumberg , Department of Computer Science, The Technion, Haifa, ISRAEL
pp. 388

Partial Model Checking (Abstract)

Henrik Reif Andersen , Department of Computer Science, Technical University of Denmark
pp. 398

Hardware Verification, Boolean Logic Programming, Boolean Functional Programming (Abstract)

Enrico Tronci , Dip. Matematica Pura ed Applicata, Universita' di L'Aquila, Coppito, L'Aquila, Italy
pp. 408
Session 11: Concurrency II: Chair: U. Goltz

Compositionality via Cut-Elimination: Hennessy-Milner Logic for an Arbitrary GSOS (Abstract)

Alex K. Simpson , LFCS, Department of Computer Science University of Edinburgh,UK
pp. 420

Compositional Testing Preorders for Probabilistic Processes (Abstract)

Wang Yi , Department of Computer Systems, Uppsala University, Sweden
Bengt Jonsson , Department of Computer Systems, Uppsala University, Sweden
pp. 431
Session 12: Semantics II: Chair: L. Ong

Games Semantics for Full Propositional Linear Logic (Abstract)

Francois Lamarche , Department of Computing, Imperial College of Science and Technology,London UK
pp. 464
Session 13: Linear Logic: Chair: D. Miller

Decision Problems For Second-Order Linear Logic (Abstract)

Patrick Lincoln , SRI International
Natarajan Shankar , SRI International
Andre Scedrov , University of Pennsylvania
pp. 476

The Complexity of Neutrals in Linear Logic (Abstract)

Max I. Kanovich , Tohoku University, Japan
pp. 486

Decidability of Linear Affine Logic (Abstract)

A.P. Kopylov , Department of Mathematics and Mechanics Moscow State University, Moscow, Russia
pp. 496
Invited Speaker IV

Origins and Metamorphoses of The Trinity: Logic, Nets, Automata (Abstract)

Boris Trakhtenbrot , Tel Aviv University, Ramat Aviv 69978, Israel
pp. 506

Author Index (PDF)

pp. 518
87 ms
(Ver )