Logical Methods in Computer Science, Volume 4

Volume 4, Number 1, 2008

• Martin W. Bunder, Wil Dekkers:
  Are there Hilbert-style Pure Type Systems?
  
• Radha Jagadeesan, Alan Jeffrey, Corin Pitcher, James Riely:
  Lambda-RBAC: Programming with Role-Based Access Control.
  
• Neil D. Jones, Nina Bohr:
  Call-by-Value Termination in the Untyped lambda-Calculus.
  
• Andrew M. Pitts, Mark R. Shinwell:
  Generative Unbinding of Names.
  
• Qiqi Yan:
  Lower Bounds for Complementation of omega-Automata Via the Full Automata Technique.
  
• Jonathan Hayman, Glynn Winskel:
  Independence and Concurrent Separation Logic.
  
• Qin Ma, Luc Maranget:
  Algebraic Pattern Matching in Join Calculus.
  
• Alexis Bès:
  An Application of the Feferman-Vaught Theorem to Automata and Logics for Words over an Infinite Alphabet.
  
• Alessio Guglielmi, Tom Gundersen:
  Normalisation Control in Deep Inference via Atomic Flows.
  

Volume 4, Number 2, 2008

• Wojciech Moczydlowski:
  Normalization of IZF with Replacement.
  
• Franck van Breugel, Babita Sharma, James Worrell:
  Approximating a Behavioural Pseudometric without Discount for Probabilistic Systems.
  
• Andreas Abel:
  Semi-Continuous Sized Types and Termination.
  
• Daniel Hirschkoff, Damien Pous:
  A Distribution Law for CCS and a New Congruence Result for the p-calculus.
  
• Anca Muscholl, Igor Walukiewicz:
  A Lower Bound on Web Services Composition.
  
• Lars Birkedal, Hongseok Yang:
  Relational Parametricity and Separation Logic.
  
• François Laroussinie, Nicolas Markey, Ghassan Oreiby:
  On the Expressiveness and Complexity of ATL.
  
• Hubert Comon-Lundh, Florent Jacquemard, Nicolas Perrin:
  Visibly Tree Automata with Memory and Constraints.
  
• Patricia Bouyer, Kim Guldstrand Larsen, Nicolas Markey:
  Model Checking One-Clock Priced Timed Automata.
  

Volume 4, Number 3, 2008

• Alessandro Ferrante, Aniello Murano, Mimmo Parente:
  Enriched µ-Calculi Module Checking.
  
• Arnon Avron, Anna Zamansky:
  Canonical Calculi with (n, k)-ary Quantifiers.
  
• Martín Hötzel Escardó:
  Exhaustible Sets in Higher-type Computation.
  
• Étienne Lozes, Daniel Hirschkoff, Davide Sangiorgi:
  Separability in the Ambient Logic.
  
• Robert L. Constable, Wojciech Moczydlowski:
  Extracting Programs from Constructive HOL Proofs via IZF Set-Theoretic Semantics.
  
• Milad Niqui:
  Coinductive Formal Reasoning in Exact Real Arithmetic.
  
• Luca de Alfaro, Rupak Majumdar, Vishwanath Raman, Mariëlle Stoelinga:
  Game Refinement Relations and Metrics.
  
• Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz:
  Consistency and Completeness of Rewriting in the Calculus of Constructions.
  
• Jan J. M. M. Rutten:
  Rational Streams Coalgebraically.
  
• Naokata Shikuma, Atsushi Igarashi:
  Proving Noninterference by a Fully Complete Translation to the Simply Typed Lambda-Calculus.
  
• Piero A. Bonatti, Carsten Lutz, Aniello Murano, Moshe Y. Vardi:
  The Complexity of Enriched Mu-Calculi.
  
• Marcin Jurdzinski, Jeremy Sproston, François Laroussinie:
  Model Checking Probabilistic Timed Automata with One or Two Clocks.
  
• Benjamin Werner:
  On the Strength of Proof-irrelevant Type Theories.
  

Volume 4, Number 4, 2008

• Viorica Sofronie-Stokkermans:
  Interpolation in Local Theory Extensions.
  
• Nobuko Yoshida, Kohei Honda, Martin Berger:
  Logical Reasoning for Higher-Order Functions with Local State.
  
• Paolo Baldan, Andrea Corradini, Hartmut Ehrig, Reiko Heckel, Barbara König:
  Bisimilarity and Behaviour-Preserving Reconfigurations of Open Petri Nets.
  
• Yuxin Deng, Rob J. van Glabbeek, Matthew Hennessy, Carroll Morgan:
  Characterising Testing Preorders for Finite Probabilistic Processes.
  
• Paolo Coppola, Ugo Dal Lago, Simona Ronchi Della Rocca:
  Light Logics and the Call-by-Value Lambda Calculus.
  
• Lijun Zhang, Holger Hermanns, Friedrich Eisenbrand, David N. Jansen:
  Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations.
  
• Kousha Etessami, Mihalis Yannakakis:
  Recursive Concurrent Stochastic Games.
  
• Kousha Etessami, Marta Z. Kwiatkowska, Moshe Y. Vardi, Mihalis Yannakakis:
  Multi-Objective Model Checking of Markov Decision Processes.
  
• Chris Heunen:
  Compactly Accessible Categories and Quantum Key Distribution.
  
• Clemens Kupke, Yde Venema:
  Coalgebraic Automata Theory: Basic Results.
  
• Rajeev Alur, Marcelo Arenas, Pablo Barceló, Kousha Etessami, Neil Immerman, Leonid Libkin:
  First-Order and Temporal Logics for Nested Words.
  
• Olivier Danvy, Kevin Millikin:
  A Rational Deconstruction of Landin's SECD Machine with the J Operator.
  
• Samuel R. Buss, Jan Hoffmann, Jan Johannsen:
  Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning.
  
• Matthew Hague, C.-H. Luke Ong:
  Symbolic Backwards-Reachability Analysis for Higher-Order Pushdown Systems.
  
• Filip Murlak:
  The Wadge Hierarchy of Deterministic Tree Languages.
  
• Benedikt Bollig:
  On the Expressive Power of 2-Stack Visibly Pushdown Automata.
  
• Lutz Schröder:
  Bootstrapping Inductive and Coinductive Types in HasCASL.