The Community for Technology Leaders
Logic in Computer Science, Symposium on (2002)
Copenhagen, Denmark
July 22, 2002 to July 25, 2002
ISSN: 1043-6871
ISBN: 0-7695-1483-9
TABLE OF CONTENTS
Introduction

Foreword (PDF)

pp. ix
FLoC Joint Invited Lecture

Little Engines of Proof (PDF)

Natarajan Shankar , SRI International
pp. 3
Session 1

Automatic Decidability (Abstract)

Christopher Lynch , Clarkson University
Barbara Morawska , Clarkson University
pp. 7
Session 2

Tree-Like Counterexamples in Model Checking (Abstract)

Helmut Veith , Technische Universität Wien
Edmund Clarke , Carnegie Mellon University
Yuan Lu , Broadcom COM
Somesh Jha , University of Wisconsin
pp. 19

Probabilistic Abstraction for Model Checking: An Approach Based on Property Testing (Abstract)

Sophie Laplante , University of Paris-Sud
Sylvain Peyronnet , University of Paris-Sud
Michel de Rougemont , University of Paris II
Richard Lassaigne , University of Paris 7
pp. 30

Semantic Minimization of 3-Valued Propositional Formulae (Abstract)

Mooly Sagiv , Tel-Aviv University
Thomas Reps , University of Wisconsin
Alexey Loginov , University of Wisconsin
pp. 40
Session 3

A Stratified Semantics of General References Embeddable in Higher-Order Logic (Abstract)

Amal J. Ahmed , Princeton University
Roberto Virga , Princeton University
Andrew W. Appel , Princeton University
pp. 75
Session 4

A Syntactic Approach to Foundational Proof-Carrying Code (Abstract)

Nadeem A. Hamid , Yale University
Valery Trifonov , Yale University
Zhaozhong Ni , Yale University
Stefan Monnier , Yale University
Zhong Shao , Yale University
pp. 89

A Fully Abstract May Testing Semantics for Concurrent Objects (Abstract)

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

Semantics and Logic of Object Calculi (Abstract)

Bernhard Reus , University of Sussex
Thomas Streicher , Technical University Darmstadt
pp. 113
Session 5

Efficient Type Inference for Record Concatenation and Subtyping (Abstract)

Tian Zhao , Purdue University
Jens Palsberg , Purdue University
pp. 125

Semantic Subtyping (Abstract)

Giuseppe Castagna , École Normale Supérieure
Véronique Benzaken , Université Paris-Sud
Alain Frisch , École Normale Supérieure
pp. 137

Remarks on Isomorphisms in Typed Lambda Calculi with Empty and Sum Types (Abstract)

Marcelo Fiore , University of Cambridge
Vincent Balat , Université Paris 7
Roberto Di Cosmo , Université Paris 7 and INRIA-Roquencourt
pp. 147
Session 6

On The Lambda Y Calculus (Abstract)

Rick Statman , Carnegie Mellon University
pp. 159

Dense Real-Time Games (Abstract)

Marco Faella , Università degli Studi di Salerno
Salvatore La Torre , Università degli Studi di Salerno and University of Pennsylvania
Aniello Murano , Università degli Studi di Salerno and Rice University
pp. 167
Session 7

Monadic Queries over Tree-Structured Data (Abstract)

Georg Gottlob , Technische Universität Wien
Christoph Koch , Technische Universität Wien
pp. 189
Session 8

The Complexity of First-Order and Monadic Second-Order Logic Revisited (Abstract)

Martin Grohe , University of Edinburgh
Markus Frick , University of Edinburgh
pp. 215

Some Results on Automatic Structures (Abstract)

Sasha Rubin , University of Auckland
Hajime Ishihara , Japan Advanced Institute of Science and Technology
Bakhadyr Khoussainov , University of Auckland
pp. 235
Session 9

Polarized Games (Abstract)

Olivier Laurent , CNRS and University Paris 7
pp. 265
Session 10

The Powerdomain of Indexed Valuations (Abstract)

Daniele Varacca , University of Aarhus and University of Cambridge
pp. 299
Session 11

Complete Problems for Dynamic Complexity Classes (Abstract)

Neil Immerman , University of Massachusetts at Amherst
William Hesse , University of Massachusetts at Amherst
pp. 313
Session 12

Unsatisfiable Random Formulas Are Hard to Certify (Abstract)

Albert Atserias , Universitat Politècnica de Catalunya
pp. 325

The Proof Complexity of Linear Algebra (Abstract)

Stephen Cook , University of Toronto
Michael Soltys , McMaster University
pp. 335
Short Presentations
Session 14

Description Logics: Foundations for Class-based Knowledge Representation (Abstract)

Maurizio Lenzerini , Università di Roma "La Sapienza"
Diego Calvanese , Università di Roma "La Sapienza"
Giuseppe De Giacomo , Università di Roma "La Sapienza"
pp. 359
Session 15

Temporal Logic with Forgettable Past (Abstract)

Philippe Schnoebelen , ENS de Cachan & CNRS UMR
François Laroussinie , ENS de Cachan & CNRS UMR
Nicolas Markey , ENS de Cachan & CNRS UMR and Université Orléans & CNRS
pp. 383
Session 16

The Metric Analogue of Weak Bisimulation for Probabilistic Processes (Abstract)

Josée Desharnais , Université Laval
Vineet Gupta , Stratify Inc.
Radha Jagadeesan , Loyola University-Lake Shore Campus
Prakash Panangaden , McGill University
pp. 413

Linearity in Process Languages (Abstract)

Mikkel Nygaard , University of Aarhus
Glynn Winskel , University of Cambridge
pp. 433
Session 17
Short Presentations
Author Index

Author Index (PDF)

pp. 461
97 ms
(Ver )