LICS'99 accepted papers

LICS'99 accepted papers




A Fragment Calculus --  towards a model of Separate Compilation,
Linking and Binary Compatibility, 
  -- Sophia Drossopoulou, Susan Eisenbach, David Wragg 

A New Approach to Abstract Syntax Involving Binders, 
  -- MJ Gabbay, AM Pitts

A Superposition Decision Procedure for the Guarded Fragment with
Equality, 
  -- Harald Ganzinger, Hans de Nivelle 

A fully abstract game semantics for finite nondeterminism, 
  -- Russell Harmer, Guy McCusker

Abstract Syntax and Variable Binding, 
  -- Marcelo Fiore, Gordon Plotkin, Daniele Turi

Concurrent Games and Full Completeness, 
  -- Samson Abramsky, Paul-Andre Mellies

Correctness of Multiplicative Proof Nets is Linear, 
  -- Stefano Guerrini

Counting and Addition cannot express Deterministic Transitive Closure, 
  -- Matthias Ruhl

Elementary Axioms for Categories of Classes, 
  -- Alex K. Simpson

Entailment of Atomic Set Constraints is PSPACE-Complete, 
  -- Joachim Niehren, Martin Mueller, Jean-Marc Talbot 

Extensional Equality in Intensional Type Theory, 
  -- Thorsten Altenkirch

First-Order Logic vs. Fixed-Point Logic in Finite Set Theory, 
  -- Albert Atserias, Phokion G. Kolaitis

Full Abstraction via Realisability, 
  -- Michael Marz, Alexander Rohr, Thormas Streicher

Full completeness of the multiplicative linear logic of Chu spaces,
  -- Harish Devarajan, Gordon Plotkin, Vaughan Pratt 

Guarded Fixed Point Logic, 
  -- Erich Graedel, Igor Walukiewicz

Linear types and non-size-increasing polynomial time computation, 
  -- Martin Hofmann

Logics with Aggregate Operators, 
  -- Lauri Hella, Leonid Libkin, Juha Nurmonen, Limsoon Wong

Logics with Counting, Auxiliary Relations, and Lower Bounds for
Invariant Queries, 
  -- Leonid Libkin

Modular Temporal Logic, 
  -- Augustin Baziramwabo, Pierre McKenzie, Denis Therien

Non-deterministic Games and Program Analysis: An application to
security, 
  -- Pasquale Malacaria, Chris Hankin 

On Bunched Predicate Logic, 
  -- David J. Pym

On Hoare Logic and Kleene Algebra with Tests, 
  -- Dexter Kozen

On the Expressive Power of CTL*, 
  -- Faron Moller, Alex Rabinovich

On the Verification of Broadcast Protocols, 
  -- Javier Esparza, Alain Finkel, Richard Mayr

Parametric Quantitative Temporal Reasoning, 
  -- E. Allen Emerson, Richard J. Trefler

Paramodulation with Non-Monotonic Orderings, 
  -- Miquel Bofill, Guillem Godoy, Robert Nieuwenhuis, Albert Rubio  

Parikh's Theorem in Commutative Kleene Algebra, 
  -- Dexter Kozen, Mark W. Hopkins

Pattern Matching as Cut Elimination, 
  -- Serenella Cerrito, Delia Kesner

Proof techniques for Cryptographic Processes, 
  -- Michele Boreale, Rocco De Nicola, Rosario Pugliese

Reasoning about common knowledge with infinitely many agents, 
  -- Richard Shore, Joseph Halpern

Region analysis and the polymorphic lambda calculus, 
  -- Anindya Banerjee, Nevin Heintze, Jon G. Riecke

Semantical analysis of higher-order abstract syntax, 
  -- Martin Hofmann

Some Computational Properties of Intersection Types, 
  -- A.Bucciarelli, S.De Lorenzis, A.Piperno, I.Salvo

Subtyping Recursive Types in Kernel Fun, 
  -- Dario Colazzo, Giorgio Ghelli

The Higher-order Recursive Path Ordering, 
  -- Jean-Pierre Jouannaud, Albert Rubio

The Two-Variable Guarded Fragment with Transitive Relations, 
  -- Harald Ganzinger, Christoph Meyer, Margus Veanes

Towards a theory of bisimulation for local names, 
  -- Alan Jeffrey, Julian Rathke

Two-Variable Descriptions of Regularity, 
  -- Erich Graedel, Eric Rosen

Type Inference for Recursive Definitions, 
  -- Assaf J. Kfoury, Santiago Pericas

Weak Bisimulation and Open maps, 
  -- Marcelo Fiore, Gian Luca Cattani, Glynn Winskel

Weak Bounded Arithmetic, the Diffie-Hellman Problem and Constable's
Class K, 
  -- Jan Johannsen

Working with arms: complexity results on atomic representations of
Herbrand models, 
  -- Georg Gottlob, Reinhard Pichler