Laurent Fribourg
Proceedings of the 10th EACSL Annual Conference / 15th International Workshop on Computer Science Logic
CSL, 2001.

@proceedings{CSL-2001,
	address       = "Paris, France",
	editor        = "Laurent Fribourg",
	isbn          = "3-540-42554-3",
	publisher     = "{Springer-Verlag}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 10th EACSL Annual Conference / 15th International Workshop on Computer Science Logic}",
	volume        = 2142,
	year          = 2001,
}

Contents (42 items)

12 ×#logic
3 ×#automaton
3 ×#commutative
3 ×#higher-order
3 ×#theorem
2 ×#algebra
2 ×#category theory
2 ×#database
2 ×#decidability
2 ×#deduction

CSL-2001-OHearnRY #data type #reasoning #source code

Local Reasoning about Programs that Alter Data Structures (PWO, JCR, HY), pp. 1–19.

CSL-2001-Bussche #database

Applications of Alfred Tarski’s Ideas in Database Theory (JVdB), pp. 20–37.

CSL-2001-Girard #logic

Locus Solum: From the Rules of Logic to the Logic of Rules (JYG), p. 38.

CSL-2001-Kanovich #linear #logic #monad #power of

The Expressive Power of Horn Monadic Linear Logic (MIK), pp. 39–53.

CSL-2001-GuglielmiS #calculus #commutative

Non-commutativity and MELL in the Calculus of Structures (AG, LS), pp. 54–68.

CSL-2001-Mogbil #commutative #correctness #logic #polynomial

Quadratic Correctness Criterion for Non-commutative Logic (VM), pp. 69–83.

CSL-2001-ChenS #complexity

Capture Complexity by Partition (YC, ES), pp. 84–98.

CSL-2001-GroheW #locality #theorem

An Existential Locality Theorem (MG, SW), pp. 99–114.

CSL-2001-Marion

Actual Arithmetic and Feasibility (JYM), pp. 115–129.

CSL-2001-Schweikardt #database #order

The Natural Order-Generic Collapse for ω-Representable Databases over the Rational and the Real Ordered Group (NS), pp. 130–144.

CSL-2001-PowerT #algebra

An Algebraic Foundation for Higraphs (JP, KT), pp. 145–159.

CSL-2001-KorovinaK #higher-order #semantics

Semantic Characterisations of Second-Order Computability over the Real Numbers (MVK, OVK), pp. 160–172.

CSL-2001-RobinsonR

An Abstract Look at Realizability (ER, GR), pp. 173–187.

CSL-2001-DanosH

The Anatomy of Innocence (VD, RH), pp. 188–202.

CSL-2001-Bezem #higher-order #logic programming #source code

An Improved Extensionality Criterion for Higher-Order Logic Programs (MB), pp. 203–216.

CSL-2001-StarkN #logic #state machine

A Logic for Abstract State Machines (RFS, SN), pp. 217–231.

CSL-2001-Eijck

Constrained Hyper Tableaux (JvE), pp. 232–246.

CSL-2001-LutzSW #logic

Modal Logic and the Two-Variable Fragment (CL, US, FW), pp. 247–261.

CSL-2001-Koriche #approximate #first-order #logic #reasoning

A Logic for Approximate First-Order Reasoning (FK), pp. 262–276.

CSL-2001-DawarGK #fixpoint #logic

Inflationary Fixed Points in Modal Logic (AD, EG, SK), pp. 277–291.

CSL-2001-AlechinaMPR #category theory #logic #semantics

Categorical and Kripke Semantics for Constructive S4 Modal Logic (NA, MM, VdP, ER), pp. 292–307.

CSL-2001-Rasmussen #deduction #logic

Labelled Natural Deduction for Interval Logics (TMR), pp. 308–323.

CSL-2001-BoerE #decidability #logic #navigation

Decidable Navigation Logics for Object Structures (FSdB, RMvE), pp. 324–338.

CSL-2001-CharatonikT #decidability #mobile #model checking

The Decidability of Model Checking Mobile Ambients (WC, JMT), pp. 339–354.

CSL-2001-GalotaV #automaton #theorem

A Generalization of the Büchi-Elgot-Trakhtenbrot Theorem (MG, HV), pp. 355–368.

CSL-2001-Finkel #automaton #effectiveness

An Effective Extension of the Wagner Hierarchy to Blind Counter Automata (OF), pp. 369–383.

CSL-2001-Klaedtke

Decision Procedure for an Extension of WS1S (FK), pp. 384–398.

CSL-2001-Akama #algebra #combinator #logic #towards #λ-calculus

Limiting Partial Combinatory Algebras towards Infinitary λ-Calculi and Classical Logic (YA), pp. 399–413.

CSL-2001-RoccaR #logic

Intersection Logic (SRDR, LR), pp. 414–428.

CSL-2001-Schroder

Life without the Terminal Type (LS), pp. 429–442.

CSL-2001-AbramskyL #modelling #λ-calculus

Fully Complete Minimal PER Models for the Simply Typed λ-Calculus (SA, ML), pp. 443–457.

CSL-2001-Martin #induction

A Principle of Induction (KM), pp. 458–468.

CSL-2001-BaazM #on the #theorem

On a Generalisation of Herbrand’s Theorem (MB, GM), pp. 469–483.

CSL-2001-Goubault-Larrecq #recursion

Well-Founded Recursive Relations (JGL), pp. 484–497.

CSL-2001-Schmidt-Schauss #unification

Stratified Context Unification Is in PSPACE (MSS), pp. 498–512.

CSL-2001-ArmandoRR

Uniform Derivation of Decision Procedures by Superposition (AA, SR, MR), pp. 513–527.

CSL-2001-Rosu #category theory #deduction #equation

Complete Categorical Equational Deduction (GR), pp. 528–538.

CSL-2001-Ohsaki #automaton #commutative #equation

Beyond Regularity: Equational Tree Automata for Associative and Commutative Theories (HO), pp. 539–553.

CSL-2001-Courtieu #normalisation

Normalized Types (PC), pp. 554–569.

CSL-2001-KopylovN #markov #type system

Markov’s Principle for Propositional Type Theory (AK, AN), pp. 570–584.

CSL-2001-Schurmann #encoding #higher-order #recursion

Recursion for Higher-Order Encodings (CS), pp. 585–599.

CSL-2001-Matthes #induction #rank

Monotone Inductive and Coinductive Constructors of Rank 2 (RM), pp. 600–614.