Proceedings 16th Annual IEEE Symposium on Logic in Computer Science (PDF)

Foreword (PDF)

Conference Organization (PDF)

Additional Reviewers (PDF)

Probabilistic Polynomial-Time Process Calculus and Security Protocol Analysis (Abstract)

Definitions by Rewriting in the Calculus of Constructions (Abstract)

Deconstructing Shostak (Abstract)

A Decision Procedure for an Extensional Theory of Arrays (Abstract)

On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups (Abstract)

Successive Approximation of Abstract Transition Relations (Abstract)

A Bound on Attacks on Payment Protocols (Abstract)

Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems (Abstract)

Semantics of Name and Value Passing (Abstract)

A Fully Abstract Game Semantics of Local Exceptions (Abstract)

A Universal Characterization of the Closed Euclidean Interval (Abstract)

Logician in the Land of OS: Abstract State Machines in Microsoft (Abstract)

Eliminating Definitions and Skolem Functions in First-Order Logic (Abstract)

A continuum of theories of lambda calculus without semantics (Abstract)

The Hierarchy inside Closed Monadic S1 Collapses on the Infinite Binary Tree (Abstract)

On Definability of Order in Logic with Choice (Abstract)

The Engineering Challenge for Logic (PDF)

A Second-Order System for Polytime Reasoning Using Gr?del's Theorem (Abstract)

The Crane Beach Conjecture (Abstract)

An n! Lower Bound on Formula Size (Abstract)

Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory (Abstract)

Dependent Types for Program Termination Verification (Abstract)

The Dolev-Yaho Intruder is the Most Powerful Attacker (PDF)

Semantics of machine Instructions at Multiple Levels of Abstraction (PDF)

A proof-Carrying Authorization System (PDF)

Recursive Programming Languages for Complexity Classes (PDF)

Interior-Point Approach to Parity Games (PDF)

Recent Progress in Proof Mining (PDF)

On the Complexity of Confluence for Ground Rewrite Systems (PDF)

Computing the Density of Regular Languages (PDF)

Integrating Simplification Techniques in SAT Algorithms (PDF)

Basic Completion Modulo with Simplification (PDF)

Finite Visit Sequential Deterministic Tree Automata (PDF)

Foundational Proof-Carrying Code (Abstract)

Intuitionistic Linear Logic and Partial Correctness (Abstract)

Perturbed Turing Machines and Hybrid Systems (Abstract)

Deterministic Generators and Games for Ltl Fragments (Abstract)

Normalization by Evaluation for Typed Lambda Calculus with Coproducts (Abstract)

A Symbolic Labelled Transition System for Coinductive Subtyping of F_{\mu\leq} Types (Abstract)

A Continuum of Theories of Lambda Calculus without Semantics (Abstract)

Focus Games for Satisfiability and Completeness of Temporal Logic (Abstract)

Safety and Liveness in Branching Time (Abstract)

Self-Verifying Systems, the Incompleteness Theorem and the Tangibility Reflection Principle (PDF)

Repairing the Interpolation Theorem in First-Order Modal Logic (PDF)

A Game involving Epistemic Logic and Probability (PDF)

A Theory of Advanced Transactions in the Situation Calculus (PDF)

Semistructured Data: From Practice to Theory (Abstract)

Synthesizing Distributed Systems (Abstract)

Permutation Rewriting and Algorithmic Verification (Abstract)

Temporal Logic Query Checking (Abstract)

Typechecking XML Views of Relational Databases (Abstract)

A Model-Theoretic Approach to Regular String Relations (Abstract)

Author Index (PDF)