Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science
LICS, 2001.

@proceedings{LICS-2001,
	address       = "Boston, Massachusetts, USA",
	ee            = "http://www.computer.org/csdl/proceedings/lics/2001/1281/00/index.html",
	isbn          = "0-7695-1281-X",
	publisher     = "{IEEE Computer Society}",
	title         = "{Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science}",
	year          = 2001,
}

Contents (42 items)

6 ×#logic
4 ×#calculus
4 ×#semantics
3 ×#game studies
3 ×#monad
3 ×#normalisation
3 ×#on the
3 ×#verification
2 ×#bound
2 ×#problem

LICS-2001-MitchellRST #analysis #calculus #probability #process #protocol #security

Probabilistic Polynominal-Time Process Calculus and Security Protocol Analysis (JCM, AR, AS, VT), pp. 3–5.

LICS-2001-Blanqui #calculus

Definitions by Rewriting in the Calculus of Constructions (FB), pp. 9–18.

LICS-2001-RuessS

Deconstructing Shostak (HR, NS), pp. 19–28.

LICS-2001-StumpBDL #array

A Decision Procedure for an Extensional Theory of Arrays (AS, CWB, DLD, JRL), pp. 29–37.

LICS-2001-GodoyN #constraints #deduction #monad #on the

On Ordering Constraints for Deduction with Built-In Abelian Semigroups, Monoids and Groups (GG, RN), pp. 38–47.

LICS-2001-DasD #approximate

Successive Approximation of Abstract Transition Relations (SD, DLD), pp. 51–58.

LICS-2001-Stoller #bound #protocol

A Bound on Attacks on Payment Protocols (SDS), pp. 61–70.

LICS-2001-KirousisK #complexity

A Dichotomy in the Complexity of Propositional Circumscription (LMK, PGK), pp. 71–80.

LICS-2001-Ganzinger #concept #decidability #problem #semantics #word

Relating Semantic and Proof-Theoretic Concepts for Polynominal Time Decidability of Uniform Word Problems (HG), pp. 81–90.

LICS-2001-FioreT #semantics

Semantics of Name and Value Passing (MPF, DT), pp. 93–104.

LICS-2001-Laird #exception #game studies #semantics

A Fully Abstract Game Semantics of Local Exceptions (JL), pp. 105–114.

LICS-2001-EscardoS

A Universal Characterization of the Closed Euclidean Interval (MHE, AKS), pp. 115–125.

LICS-2001-Gurevich #state machine

Logician in the Land of OS: Abstract State Machines in Microsoft (YG), pp. 129–136.

LICS-2001-Avigad #first-order #logic

Eliminating Definitions and Skolem Functions in First-Order Logic (JA), pp. 139–146.

LICS-2001-SzwastT #on the #problem #transitive

On the Decision Problem for the Guarded Fragment with Transitivity (WS, LT), pp. 147–156.

LICS-2001-ArnoldLM #infinity #monad

The Hierarchy inside Closed Monadic Σ₁ Collapses on the Infinite Binary Tree (AA, GL, JM), pp. 157–166.

LICS-2001-HuuskonenH #logic #on the #order

On Definability of Order in Logic with Choice (TH, TH), pp. 167–172.

LICS-2001-Thomas #challenge #logic

The Engineering Challenge for Logic (WT), pp. 173–176.

LICS-2001-CookK #higher-order #reasoning #theorem #using

A Second-Order System for Polytime Reasoning Using Graedel’s Theorem (SAC, AK), pp. 177–186.

LICS-2001-BarringtonILST

The Crane Beach Conjecture (DAMB, NI, CL, NS, DT), pp. 187–196.

LICS-2001-AdlerI #bound #exclamation

An n! Lower Bound on Formula Size (MA, NI), pp. 197–206.

LICS-2001-Terui #calculus #normalisation

Light Affine Calculus and Polytime Strong Normalization (KT), pp. 209–220.

LICS-2001-Pfenning #proving #type system

Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory (FP), pp. 221–230.

LICS-2001-Xi #dependent type #termination #verification

Dependent Types for Program Termination Verification (HX), pp. 231–242.

LICS-2001-Appel

Foundational Proof-Carrying Code (AWA), pp. 247–256.

LICS-2001-KozenT #correctness #linear #logic

Intuitionistic Linear Logic and Partial Correctness (DK, JT), pp. 259–268.

LICS-2001-AsarinB #hybrid #turing machine

Perturbed Turing Machines and Hybrid Systems (EA, AB), pp. 269–278.

LICS-2001-AlfaroHM #source code #verification

From Verification to Control: Dynamic Programs for ω-Regular Objectives (LdA, TAH, RM), pp. 279–290.

LICS-2001-AlurT #game studies #generative #ltl

Deterministic Generators and Games for LTL Fragments (RA, SLT), pp. 291–300.

LICS-2001-AltenkirchDHS #evaluation #normalisation #λ-calculus

Normalization by Evaluation for Typed λ Calculus with Coproducts (TA, PD, MH, PJS), pp. 303–310.

LICS-2001-YoshidaBH #normalisation #π-calculus

Strong Normalisation in the π-Calculus (NY, MB, KH), pp. 311–322.

LICS-2001-Jeffrey #induction #lts #type system

A Symbolic Labelled Transition System for Coinductive Subtyping of Fμ≤ Types (AJ), pp. 323–333.

LICS-2001-Salibra #semantics #λ-calculus

A Continuum of Theories of λ Calculus without Semantics (AS), pp. 334–343.

LICS-2001-JaninL #calculus #monad #μ-calculus

Relating Levels of the μ-Calculus Hierarchy and Levels of the Monadic Hierarchy (DJ, GL), pp. 347–356.

LICS-2001-LangeS #game studies #logic #satisfiability

Focus Games for Satisfiability and Completeness of Temporal Logic (ML, CS), pp. 357–365.

LICS-2001-ManoliosT #branch #liveness #safety

Safety and Liveness in Branching Time (PM, RJT), pp. 366–374.

LICS-2001-Abiteboul #semistructured data #theory and practice

Semistructured Data: from Practice to Theory (SA), pp. 379–386.

LICS-2001-KupfermanV #distributed

Synthesizing Distributed Systems (OK, MYV), pp. 389–398.

LICS-2001-BouajjaniMT #algorithm #permutation #verification

Permutation Rewriting and Algorithmic Verification (AB, AM, TT), pp. 399–408.

LICS-2001-BrunsG #logic #query

Temporal Logic Query Checking (GB, PG), pp. 409–417.

LICS-2001-AlonMNSV #database #relational #xml

Typechecking XML Views of Relational Databases (NA, TM, FN, DS, VV), pp. 421–430.

LICS-2001-BenediktLSS #approach #string

A Model-Theoretic Approach to Regular String Relations (MB, LL, TS, LS), pp. 431–440.