Selected Papers of the 2005 IEEE Symposium on Logic in Computer Science


Editor: Prakash Panangaden

1. Relational Parametricity and Control

Hasegawa, Masahito.
We study the equational theory of Parigot's second-order λμ-calculus in connection with a call-by-name continuation-passing style (CPS) translation into a fragment of the second-order λ-calculus. It is observed that the relational parametricity on the target calculus […]

2. Tarski's influence on computer science

Feferman, Solomon.
The influence of Alfred Tarski on computer science was indirect but significant in a number of directions and was in certain respects fundamental. Here surveyed is the work of Tarski on the decision procedure for algebra and geometry, the method of elimination of quantifiers, the semantics of […]

3. Generalized Majority-Minority Operations are Tractable

Dalmau, Victor.
Generalized majority-minority (GMM) operations are introduced as a common generalization of near unanimity operations and Mal'tsev operations on finite sets. We show that every instance of the constraint satisfaction problem (CSP), where all constraint relations are invariant under a (fixed) GMM […]

4. Semantics of Separation-Logic Typing and Higher-order Frame Rules for<br> Algol-like Languages

Birkedal, Lars ; Torp-Smith, Noah ; Yang, Hongseok.
We show how to give a coherent semantics to programs that are well-specified in a version of separation logic for a language with higher types: idealized algol extended with heaps (but with immutable stack variables). In particular, we provide simple sound rules for deriving higher-order frame […]

5. On the decidability and complexity of Metric Temporal Logic over finite words

Ouaknine, Joel ; Worrell, James.
Metric Temporal Logic (MTL) is a prominent specification formalism for real-time systems. In this paper, we show that the satisfiability problem for MTL over finite timed words is decidable, with non-primitive recursive complexity. We also consider the model-checking problem for MTL: whether […]