default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID16th LICS 2001: Boston, Massachusetts, USA
- 16th Annual IEEE Symposium on Logic in Computer Science, Boston, Massachusetts, USA, June 16-19, 2001, Proceedings. IEEE Computer Society 2001, ISBN 0-7695-1281-X
Invited Talk
- John C. Mitchell, Ajith Ramanathan, Andre Scedrov, Vanessa Teague:
Probabilistic Polynominal-Time Process Calculus and Security Protocol Analysis. 3-5
Session 1
- Frédéric Blanqui:
Definitions by Rewriting in the Calculus of Constructions. 9-18 - Harald Rueß, Natarajan Shankar:
Deconstructing Shostak. 19-28 - Aaron Stump, Clark W. Barrett
, David L. Dill, Jeremy R. Levitt:
A Decision Procedure for an Extensional Theory of Arrays. 29-37 - Guillem Godoy, Robert Nieuwenhuis:
On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups. 38-47
Invited Talk
- Satyaki Das, David L. Dill:
Successive Approximation of Abstract Transition Relations. 51-58
Session 2
- Scott D. Stoller:
A Bound on Attacks on Payment Protocols. 61-70 - Lefteris M. Kirousis, Phokion G. Kolaitis:
A Dichotomy in the Complexity of Propositional Circumscription. 71-80 - Harald Ganzinger:
Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems. 81-90
Session 3
- Marcelo P. Fiore, Daniele Turi:
Semantics of Name and Value Passing. 93-104 - James Laird:
A Fully Abstract Game Semantics of Local Exceptions. 105-114 - Martín Hötzel Escardó, Alex K. Simpson:
A Universal Characterization of the Closed Euclidean Interval. 115-125
Invited Talk
- Yuri Gurevich:
Logician in the Land of OS: Abstract State Machines in Microsoft. 129-136
Session 4
- Jeremy Avigad:
Eliminating Definitions and Skolem Functions in First-Order Logic. 139-146 - Wieslaw Szwast, Lidia Tendera:
On the Decision Problem for the Guarded Fragment with Transitivity. 147-156 - André Arnold, Giacomo Lenzi, Jerzy Marcinkowski:
The Hierarchy inside Closed Monadic Sigma1 Collapses on the Infinite Binary Tree. 157-166 - Taneli Huuskonen, Tapani Hyttinen:
On Definability of Order in Logic with Choice. 167-172
Invited Talk
- Wolfgang Thomas:
The Engineering Challenge for Logic. LICS 2001: 173-176
Session 5
- Stephen A. Cook, Antonina Kolokolova:
A Second-Order System for Polytime Reasoning Using Graedel's Theorem. 177-186 - David A. Mix Barrington, Neil Immerman, Clemens Lautemann, Nicole Schweikardt, Denis Thérien:
The Crane Beach Conjecture. 187-196 - Micah Adler, Neil Immerman:
An n! Lower Bound on Formula Size. 197-206
Session 6
- Kazushige Terui:
Light Affine Calculus and Polytime Strong Normalization. 209-220 - Frank Pfenning:
Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. 221-230 - Hongwei Xi:
Dependent Types for Program Termination Verification. 231-242
Short Paper Session
Invited Talk
- Andrew W. Appel:
Foundational Proof-Carrying Code. 247-256
Session 7
- Dexter Kozen, Jerzy Tiuryn:
Intuitionistic Linear Logic and Partial Correctness. 259-268 - Eugene Asarin, Ahmed Bouajjani:
Perturbed Turing Machines and Hybrid Systems. 269-278 - Luca de Alfaro, Thomas A. Henzinger, Rupak Majumdar:
From Verification to Control: Dynamic Programs for Omega-Regular Objectives. 279-290 - Rajeev Alur, Salvatore La Torre:
Deterministic Generators and Games for LTL Fragments. 291-300
Session 8
- Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, Philip J. Scott:
Normalization by Evaluation for Typed Lambda Calculus with Coproducts. 303-310 - Nobuko Yoshida, Martin Berger, Kohei Honda:
Strong Normalisation in the pi-Calculus. 311-322 - Alan Jeffrey:
A Symbolic Labelled Transition System for Coinductive Subtyping of Fµ< Types. 323-333 - Antonino Salibra:
A Continuum of Theories of Lambda Calculus without Semantics. 334-343
Session 9
- David Janin, Giacomo Lenzi:
Relating Levels of the Mu-Calculus Hierarchy and Levels of the Monadic Hierarchy. 347-356 - Martin Lange, Colin Stirling:
Focus Games for Satisfiability and Completeness of Temporal Logic. 357-365 - Panagiotis Manolios, Richard J. Trefler:
Safety and Liveness in Branching Time. 366-374
Short Papers
- Serge Abiteboul:
Semistructured Data: from Practice to Theory. 379-386
Session 10
- Orna Kupferman, Moshe Y. Vardi:
Synthesizing Distributed Systems. 389-398 - Ahmed Bouajjani, Anca Muscholl, Tayssir Touili:
Permutation Rewriting and Algorithmic Verification. 399-408 - Glenn Bruns, Patrice Godefroid:
Temporal Logic Query Checking. 409-417
Session 11
- Noga Alon, Tova Milo, Frank Neven, Dan Suciu, Victor Vianu:
Typechecking XML Views of Relational Databases. 421-430 - Michael Benedikt, Leonid Libkin, Thomas Schwentick, Luc Segoufin:
A Model-Theoretic Approach to Regular String Relations. 431-440
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2025-11-28 23:53 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
