Jerzy Marcinkowski, Andrzej Tarlecki
Proceedings of the 13th EACSL Annual Conference / 18th International Workshop on Computer Science Logic
CSL, 2004.

@proceedings{CSL-2004,
	address       = "Karpacz, Poland",
	editor        = "Jerzy Marcinkowski and Andrzej Tarlecki",
	isbn          = "3-540-23024-6",
	publisher     = "{Springer International Publishing}",
	series        = "{Lecture Notes in Computer Science}",
	title         = "{Proceedings of the 13th EACSL Annual Conference / 18th International Workshop on Computer Science Logic}",
	volume        = 3210,
	year          = 2004,
}

Contents (38 items)

11 ×#logic
5 ×#proving
4 ×#bound
4 ×#linear
3 ×#calculus
3 ×#game studies
3 ×#on the
3 ×#λ-calculus
2 ×#higher-order
2 ×#model checking

CSL-2004-Atserias #complexity #random #satisfiability

Notions of Average-Case Complexity for Random 3-SAT (AA), pp. 1–5.

CSL-2004-Hyland #abstract interpretation #calculus #proving

Abstract Interpretation of Proofs: Classical Propositional Calculus (MH), pp. 6–21.

CSL-2004-McMillan #model checking

Applications of Craig Interpolation to Model Checking (KLM), pp. 22–23.

CSL-2004-Miller #quantifier

Bindings, Mobility of Bindings, and the “generic judgments”-Quantifier: An Abstract (DM), p. 24.

CSL-2004-Urzyczyn

My (Un)Favourite Things (PU), p. 25.

CSL-2004-ChatterjeeMJ #game studies #nash #on the #probability

On Nash Equilibria in Stochastic Games (KC, RM, MJ), pp. 26–40.

CSL-2004-Bojanczyk #bound #quantifier

A Bounding Quantifier (MB), pp. 41–55.

CSL-2004-Gimbert #game studies #graph #infinity

Parity and Exploration Games on Infinite Graphs (HG), pp. 56–70.

CSL-2004-GanzingerK #equation #proving #reasoning #theorem proving

Integrating Equational Reasoning into Instantiation-Based Theorem Proving (HG, KK), pp. 71–84.

CSL-2004-MetcalfeOG #logic

Goal-Directed Methods for Lukasiewicz Logic (GM, NO, DMG), pp. 85–99.

CSL-2004-DawsonG #termination #theorem

A General Theorem on Termination of Rewriting (JED, RG), pp. 100–114.

CSL-2004-Hyvernat #linear #logic

Predicate Transformers and Linear Logic: Yet Another Denotational Model (PH), pp. 115–129.

CSL-2004-Gianantonio #linear #logic #multi

Structures for Multiplicative Cyclic Linear Logic: Deepness vs Cyclicity (PDG), pp. 130–144.

CSL-2004-StrassburgerL #linear #logic #multi #on the #proving

On Proof Nets for Multiplicative Linear Logic with Units (LS, FL), pp. 145–159.

CSL-2004-ImmermanRRSY #bound #decidability #logic #transitive

The Boundary Between Decidability and Undecidability for Transitive-Closure Logics (NI, AMR, TWR, SS, GY), pp. 160–174.

CSL-2004-ArenasBL #finite #game studies #locality #modelling

Game-Based Notions of Locality Over Finite Models (MA, PB, LL), pp. 175–189.

CSL-2004-AbelM #fixpoint #recursion

Fixed Points of Type Constructors and Primitive Recursion (AA, RM), pp. 190–204.

CSL-2004-Schubert #on the

On the Building of Affine Retractions (AS), pp. 205–219.

CSL-2004-GrooteS #higher-order #linear #λ-calculus

Higher-Order Matching in the Linear λ-calculus with Pairing (PdG, SS), pp. 220–234.

CSL-2004-SchoppS #dependent type #type system

A Dependent Type Theory with Names and Binding (US, IS), pp. 235–249.

CSL-2004-Weber #logic #towards #verification

Towards Mechanized Program Verification with Separation Logic (TW), pp. 250–264.

CSL-2004-AmadioCDJ #bound #bytecode #functional #verification

A Functional Scenario for Bytecode Verification of Resource Bounds (RMA, SCG, SDZ, LJ), pp. 265–279.

CSL-2004-GiacobazziM #proving

Proving Abstract Non-interference (RG, IM), pp. 280–294.

CSL-2004-Maier #liveness #ltl #safety

Intuitionistic LTL and a New Characterization of Safety and Liveness (PM), pp. 295–309.

CSL-2004-Rohde #network

Moving in a Crumbling Network: The Balanced Case (PR), pp. 310–324.

CSL-2004-EmersonK #message passing #model checking

Parameterized Model Checking of Ring-Based Message Passing Systems (EAE, VK), pp. 325–339.

CSL-2004-Skelley #bound #higher-order

A Third-Order Bounded Arithmetic Theory for PSPACE (AS), pp. 340–354.

CSL-2004-Cordon-FrancoFM #induction #recursion

Provably Total Primitive Recursive Functions: Theories with Induction (ACF, AFM, FFLM), pp. 355–369.

CSL-2004-Richerby #logic

Logical Characterizations of PSPACE (DR), pp. 370–384.

CSL-2004-Schroder #logic #similarity #λ-calculus

The Logic of the Partial λ-Calculus with Equality (LS), pp. 385–399.

CSL-2004-Goubault-LarrecqLNZ #encryption #logic #λ-calculus

Complete Lax Logical Relations for Cryptographic λ-Calculi (JGL, SL, DN, YZ), pp. 400–414.

CSL-2004-Vouillon #type system

Subtyping Union Types (JV), pp. 415–429.

CSL-2004-KorovinaV #hybrid

Pfaffian Hybrid Systems (MVK, NV), pp. 430–441.

CSL-2004-Kameyama #axiom #continuation

Axioms for Delimited Continuations in the CPS Hierarchy (YK), pp. 442–457.

CSL-2004-RychlikowskiT #constraints #set

Set Constraints on Regular Terms (PR, TT), pp. 458–472.

CSL-2004-Lynch #proving #theorem proving

Unsound Theorem Proving (CL), pp. 473–487.

CSL-2004-AvelloneFFM #calculus #implementation #logic #performance

A Space Efficient Implementation of a Tableau Calculus for a Logic with a Constructive Negation (AA, CF, GF, UM), pp. 488–502.

CSL-2004-Ciabattoni #automation #calculus #generative #logic

Automated Generation of Analytic Calculi for Logics with Linearity (AC), pp. 503–517.