The Community for Technology Leaders
Logic in Computer Science, Symposium on (1999)
Trento, Italy
July 2, 1999 to July 5, 1999
ISSN: 1043-6871
ISBN: 0-7695-0158-3

Reviewers (PDF)

pp. x
Invited Talk:
Session 1: Chair: M. Otto

Two-Variable Descriptions of Regularity (Abstract)

Eric Rosen , RWTH Aachen
Erich Grädel , RWTH Aachen
pp. 14

The Two-Variable Guarded Fragment with Transitive Relations (Abstract)

H. Ganzinger , Max-Planck-Institut f?r Informatik
M. Veanes , Max-Planck-Institut f?r Informatik
C. Meyer , Max-Planck-Institut f?r Informatik
pp. 24

Logics with Aggregate Operators (Abstract)

Lauri Hella , University of Helsinki
Limsoon Wong , Kent Ridge Digital Labs
Leonid Libkin , Bell Laboratories
Juha Nurmonen , University of Leicester
pp. 35

Guarded Fixed Point Logic (Abstract)

Erich Grädel , RWTH Aachen
Igor Walukiewicz , Warsaw University
pp. 45
Session 2: Chair: D. SanGiorgi

Towards a Theory of Bisimulation for Local Names (Abstract)

Julian Rathke , University of Sussex
Alan Jeffrey , DePaul University
pp. 56

Weak Bisimulation and Open Maps (Abstract)

Marcelo Fiore , University of Sussex
Glynn Winskel , University of Aarhus
Gian Luca Cattani , University of Cambridge
pp. 67

Elementary Axioms for Categories of Classes (Abstract)

Alex K. Simpson , University of Edinburgh
pp. 77
Session 3: Chair: M. Dezani

Region Analysis and the Polymorphic Lambda Calculus (Abstract)

Nevin Heintze , Bell Laboratories, Lucent Technologies
Jon G. Riecke , Bell Laboratories, Lucent Technologies
Anindya Banerjee , Stevens Institute of Technology
pp. 88

Pattern Matching as Cut Elimination (Abstract)

Delia Kesner , Universite de Paris-Sud
Serenella Cerrito , Universite de Paris-Sud
pp. 98

Some Computational Properties of Intersection Types (Abstract)

Antonio Bucciarelli , Universit? di Roma "La Sapienza"
Silvia de Lorenzis , Universit? di Roma "La Sapienza"
Ivano Salvo , Universit? di Roma "La Sapienza"
Adolfo Piperno , Universit? di Roma "La Sapienza"
pp. 109

Type Inference for Recursive Definitions (Abstract)

Assaf J. Kfoury , Boston University
Santiago M. Pericas-Geertsen , Boston University
pp. 119
Invited Talk:

Plausibility Measures and Default Reasoning: An Overview (Abstract)

Joseph Y. Halpern , Cornell University
Nir Friedman , Hebrew University
pp. 130
Session 4: Chair: M. Abadi

Subtyping Recursive Types in Kernel Fun - Abstract (Abstract)

Dario Colazzo , University of Pisa
Giorgio Ghelli , University of Pisa
pp. 137

Proof Techniques for Cryptographic Processes (Abstract)

Michele Boreale , Universit? di Roma "La Sapienza"
Rocco de Nicola , Universit? di Firenze
Rosario Pugliese , Universit? di Firenze
pp. 157

On Hoare Logic and Kleene Algebra with Tests (Abstract)

Dexter Kozen , Cornell University
pp. 167
Session 5: Chair: G. Dowek

Full Abstraction and Universality via Realisability (Abstract)

Thomas Streicher , Technische Universit?t Darmstadt
Alexander Rohr , Technische Universit?t Darmstadt
Michael Marz , Technische Universit?t Darmstadt
pp. 174

On Bunched Predicate Logic (Abstract)

David J. Pym , University of London
pp. 183

Abstract Syntax and Variable Binding (Abstract)

Daniele Turi , University of Edinburgh
Gordon Plotkin , University of Edinburgh
Marcelo Fiore , University of Sussex
pp. 193
Session 6: Chair: M. Okada

A New Approach to Abstract Syntax Involving Binders (Abstract)

Andrew Pitts , Cambridge University
Murdoch Gabbay , Cambridge University
pp. 214

Paramodulation with Non-Monotonic Orderings (Abstract)

Miquel Bofill , Technical University of Catalonia
Albert Rubio , Technical University of Catalonia
Robert Nieuwenhuis , Technical University of Catalonia
Guillem Godoy , Technical University of Catalonia
pp. 225

Full Completeness of the Multiplicative Linear Logic of Chu Spaces (Abstract)

Vaughan Pratt , Stanford University
Gordon Plotkin , University of Edinburgh
Harish Devarajan , Stanford University
Dominic Hughes , Stanford University
pp. 234
Invited Talk:
Session 7: Chair: M. Grohe

First-Order Logic vs. Fixed-Point Logic in Finite Set Theory (Abstract)

Albert Atserias , University of California at Santa Cruz
Phokion G. Kolaitis , University of California at Santa Cruz
pp. 275

Entailment of Atomic Set Constraints is PSPACE-Complete (Abstract)

Joachim Niehren , Universit?t des Saarlandes
Jean-Marc Talbot , Max-Planck Institut Informatik
Martin Müller , Universit?t des Saarlandes
pp. 285
Session 8: Chair: S. Weinstein

Working with Arms: Complexity Results on Atomic Representations of Herbrand Models (Abstract)

Reinhard Pichler , Technische Universit?t Wien
Georg Gottlob , Technische Universit?t Wien
pp. 306

Counting and Addition cannot Express Deterministic Transitive Closure (Abstract)

Matthias Ruhl , Massachusetts Institute of Technology
pp. 326
Session 9: Chair: N. Shankar

Parametric Quantitative Temporal Reasoning (Abstract)

E. Allen Emerson , University of Texas at Austin
Richard J. Trefler , University of Texas at Austin
pp. 336

Modular Temporal Logic (Abstract)

Denis Thérien , McGill University
Augustin Baziramwabo , Universite de Montreal
Pierre McKenzie , Universite de Montreal
pp. 344

On the Verification of Broadcast Protocols (Abstract)

Alain Finkel , ENS de Cachan
Javier Esparza , Technische Universit?t M?nchen
Richard Mayr , University of Edinburgh
pp. 352

On the Expressive Power of CTL (Abstract)

Faron Moller , Uppsala University
Alexander Rabinovich , Tel Aviv University
pp. 360
Invited Talk:
Session 10: Chair: E. Robinson

Parikh's Theorem in Commutative Kleene Algebra (Abstract)

Dexter C. Kozen , Cornell University
Mark W. Hopkins , Adaptive Micro Systems, Inc.
pp. 394

The Higher-Order Recursive Path Ordering (Abstract)

J.-P. Jouannaud , Universit? de Paris Sud
A. Rubio , University Polit?cnica de Catalunya
pp. 402
Session 11: Chair: V. Danos

A Fully Abstract Game Semantics for Finite Nondeterminism (Abstract)

Guy McCusker , University of Sussex
Russell Harmer , Imperial College, London
pp. 422

Concurrent Games and Full Completeness (Abstract)

Samson Abramsky , University of Edinburgh
Paul-André Melliès , University Paris 7
pp. 431
Session 12: Chair: A. Asperti

Correctness of Multiplicative Proof Nets is Linear (Abstract)

Stefano Guerrini , Universit? di Roma I, "La Sapienza"
pp. 454
Invited Talk:

Author Index (PDF)

pp. 477
96 ms
(Ver 3.1 (10032016))