Table of Contents

A Universal Turing Machine Stål Aanderaa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

Recursive Inseparability in Linear Logic Stål Aanderaa and Herman Ruge Jervell . . . . . . . . . . . . . . . . . 5

The Basic Logic of Proofs Sergei Artëmov and Tyko Straßen . . . . . . . . . . . . . . . . . . . . 14

Algorithmic Structuring of Cut-Free Proofs Matthias Baaz and Richard Zach . . . . . . . . . . . . . . . . . . . . . 29

Optimization Problems: Expressibility, Approximation Properties and Expected Asymptotic Growth of Optimal Solutions Thomas Behrendt, Kevin Compton and Erich Grädel . . . . . . . . . 43

Linear λ-Calculus and Categorical Models Revisited Nick Benton, Gavin Bierman, Valeria de Paiva and Martin Hyland . 61

A Self-Interpreter of Lambda Calculus Having a Normal Form Alessandro Berarducci and Corrado Böhm . . . . . . . . . . . . . . . . 85

An “Ehrenfeucht-Fraïssé Game” for Fixpoint Logic and Stratified Fixpoint Logic Uwe Bosse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 100

The Class of Problems that Are Linearly Equivalent to Satisfiability, or a Uniform Method for Proving NP-Completeness Nadia Creignou . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115

Model Building by Resolution Christian G. Fermüller and Alexander Leitsch . . . . . . . . . . . . . 134

Comparative Transition System Semantics Tim Fernando . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149

Reasoning with Higher Order Partial Functions Antonio Gavilanes-Franco, Francisca Lucio-Carrasco and Mario Rodríguez-Artalejo . . . . . . . . . . . . . . . . . . . . . . . . . 167

Communicating Evolving Algebras Paola Glavan and Dean Rosenzweig . . . . . . . . . . . . . . . . . . . 182

On the Completeness of Narrowing as the Operational Semantics of Functional Logic Programming Juan Carlos González-Moreno, María Teresa Hortalá-González and Mario Rodríguez-Artalejo . . . . . . . . . . . . . . . . . . . . . . . . . 216 Inductive Definability with Counting on Finite Structures

Erich Grädel and Martin Otto . . . . . . . . . . . . . . . . . . . . . . 231

Linear Time Algorithms and NP-Complete Problems Etienne Grandjean . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 248

The Semantics of the C Programming Language Yuri Gurevich and James K. Huggins . . . . . . . . . . . . . . . . . . 274

A Theory of Classes for a Functional Language with Effects Furio Honsell, Ian A. Mason, Scott Smith and Carolyn Talcott …. 309

Logical Definability of NP-Optimization Problems with Monadic Auxiliary Predicates Clemens Lautemann . . . . . . . . . . . . . . . . . . . . . . . . . . . . 327

Universes in the Theories of Types and Names Markus Marzetta . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 340

Notes on Sconing and Relators John C. Mitchell and Andre Scedrov . . . . . . . . . . . . . . . . . . . 352

Solving 3-Satisfiability in Less than 1,579^{n} Steps Ingo Schiermeyer . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 379

Kleene’s Slash and Existence of Values of Open Terms in Type Theory Jan M. Smith . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 395

Negation-Complete Logic Programs Robert F. Stärk . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 403

Logical Characterizations of Bounded Query Classes II: Polynomial-Time Oracle Machines Iain A. Stewart . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 410

On Asymptotic Probabilities of Monadic Second Order Properties Jerzy Tyszkiewicz . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 425