BRICS NS-98-6 Butz et al. (eds.): Abstracts of the Workshop on Proof Theory and Complexity, PTAC ’98 BRICS

Basic Research in Computer Science

Abstracts of the Workshop on

Proof Theory and Complexity

PTAC ’98

Aarhus, Denmark, August 3–7, 1998

Carsten Butz Ulrich Kohlenbach Søren Riis Glynn Winskel (editors)

BRICS Notes Series NS-98-6

ISSN 0909-3206 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Notes Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory NS/98/6/

Abstracts of the Workshop on

Proof Theory and Complexity

PTAC ’98

August 3–7 Aarhus, Denmark

Carsten Butz Ulrich Kohlenbach Søren Riis Glynn Winskel (editors)

Preface

This small booklet contains the titles and abstracts of the talks given at the workshop Proof Theory and Complexity (PTAC’98), hosted by BRICS during the first week of August 98 (August 3 – August 7).

The topic of the workshop will be on proof-theory with connections to issues of complexity in the widest sense including e.g.:

1. Strength (proof-theoretic and mathematical) of subsystems of secondorder arithmetic and type theories.

2. Type-free applicative systems (explicit mathematics).

3. Complexity of Proof Transformations (cut-elimination, normalization, epsilon-substitution etc.).

4. Proofs as Programs.

5. Proof Interpretations and their complexity: Realizability and functional interpretations, game theoretic and categorical interpretations.

6. Bounded arithmetic and connections to complexity theory (including feasible arithmetic and analysis).

7. Proof Complexity of propositional proof systems: resolution, Frege systems, Nullstellensatz proofs etc.

8. Interactive and probabilistic proofs.

There were two preparatory lectures during the week before the workshop (by E. Palmgren and V. Orevkov—abstracts can be obtained from the BRICS homepage), and there are two special lectures in connection with the workshop that take place during this week (by A. Feferman and A. Wigderson).

The editors

Programme Committee

Carsten Butz (BRICS), Stephen Cook (Toronto), Ulrich Kohlenbach (BRICS), Jan Krajíček (Prague and Oxford), Grigori Mints (Stanford), Søren Riis (BRICS), Helmut Schwichtenberg (München), Anne Troelstra (Amsterdam).

Organising Committee

Carsten Butz, Ulrich Kohlenbach, Karen K. Møller, Søren Riis, Glynn Winskel. iv

Contents

Preface iii

Abstracts of Invited Lectures 1

N. Arai Cut-free LK Quasi-Polynomially Simulates Resolution . . . . . 1

J. Avigad Interpreting classical theories in constructive ones . . . . . . . 1

A. Beckmann Dynamic ordinal analysis - a tool for separating fragments of bounded arithmetic . . . . . . . . . . . . . . . . . . . . . . . . 1

S. Bellantoni Ramification Today . . . . . . . . . . . . . . . . . . . . . . . . 1

M. L. Bonet Automatization and non-Automatization of Propositional Proof Systems . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

W. Burr Functional Interpretation of Aczel’s Constructive Set Theory CZF . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

H. de Nivelle Deciding the E+ class with an a posteriori order . . . . . . . . 2

R. Dyckhoff Contraction-free and permutation-free calculi for some nonclassical logics . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

S. Feferman Unfolding Schematic Formal Systems . . . . . . . . . . . . . . 4

A. Hendriks Doing logic by computer . . . . . . . . . . . . . . . . . . . . . 4

M. Hofmann Extending “safe recursion” to higher types, lists, trees, and polymorphism . . . . . . . . . . . . . . . . . . . . . . . . . . 4

J. Hudelmaier Finding counter models in classical and intuitionistic logic . . 5 J. Johannsen

Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems . . . . . . . . . . . . . . . . . . 5

G. Mints

Reductions of finite and infinite proofs . . . . . . . . . . . . . 6 I. Moerdijk

Martin-Löf type theory and realisability . . . . . . . . . . . . 6 V. Orevkov

The Complexity of Terms in Proofs . . . . . . . . . . . . . . . 6 J. van Oosten

SDT in Modified Realizability . . . . . . . . . . . . . . . . . . 6 C. Pollett

Multifunction Algebras and Provability of the Collapse of PH 7 A. A. Razborov

Lower Bounds for Algebraic Proof Systems . . . . . . . . . . . 7 H. Schwichtenberg

Ramification, Modality, and Linearity in Higher Type Recursion 8 D. Scott

Types and Computability . . . . . . . . . . . . . . . . . . . . 8 T. Strahm

Abstract computations in type-free applicative systems …. 9 G. Takeuti

Forcing and P ≠ NP . . . . . . . . . . . . . . . . . . . . . . 9 L. Trevisan

Interactive and Probabilistic Proof-Checking . . . . . . . . . . 9

Abstracts of Special Lectures in Connection with the Workshop 11

A. Feferman

The Saga of Alfred Tarski: Part Two . . . . . . . . . . . . . . 11 A. Wigderson

Simple proofs of bounds on Resolution proof size . . . . . . . . 11

Participants 13

Abstracts of Invited Lectures

N. Arai (Hiroshima): Cut-free LK Quasi-Polynomially Simulates Resolution

Abstract: In this talk, the relative efficiency of two propositional systems is studied: resolution and cut-free LK in DAG. We give an upper bound for translation of resolution refutation to cut-free LK proofs. The best upper bound known was 2^{n} and we improve it to n^{2+3 log n}.

J. Avigad (Pittsburgh): Interpreting classical theories in constructive ones

Abstract: In this talk I will discuss a surprisingly uniform method of interpreting a number of classical theories in constructive theories having the same proof-theoretic strength. The classical theories considered range in strength from bounded fragments of arithmetic to Kripke-Platek admissible set theory.

A. Beckmann (Münster): Dynamic ordinal analysis - a tool for separating fragments of bounded arithmetic

Abstract: We define the dynamic ordinal of a theory which is a suitable analogue of the usual prooftheoretic ordinal for weak theories of arithmetic. We compute the dymanic ordinal of certain fragments of bounded arithmetic by adapting methods from the Schütte-style ordinal analysis of the fragments IΣ_{n}^{0} of Peano-arithmetic. Then different dynamic ordinals immediately imply the separation of the associated fragments of bounded arithmetic. This way we also obtain the separation of very weak fragments of bounded arithmetic based on induction for sΣ_{n}^{bb}-formulas in the non-relativized case, i.e. without set variables or predicate variables. The sΣ_{n}^{bb}-formulas are build up from double sharply bounded formulas by counting alternations of bounded quantifiers.

S. Bellantoni (Toronto): Ramification Today

Abstract: This presentation will survey recent results in ramification and complexity theory, in both the functional and logical settings. Recent work has shown that ramification is an important tool in controlling the computational complexity of subrecursive and arithmetic systems. Another important tool in restricting computational complexity is linearity, which is particularly useful at higher type levels. The two can be integrated using mechanisms from modal logic. The use of modality allows one to generalize the concept of “ramification level” from ground type to all higher types. Thus, for a type (σ → τ) one defines a corresponding “complete” type !(σ → τ) at one higher ramification level. Analogous to the modal axiom of distribution, in the functional setting one has a term of type !(σ → τ) →!σ →!τ.

M. L. Bonet (Barcelona): Automatization and non-Automatization of Propositional Proof Systems

Abstract: A propositional proof system S is automatizable if there is a deterministic procedure that takes as input a formula and returns an Srefutation of it (if one exists) in polynomial time in the size of the shortest S-refutation of the formula. In the talk we will give an overview of what is known about different proof systems, which are automatizable and which are not, and which it is open if they are automatizable. The talk will contain some recent results, but it will also be an overview of the topic.

W. Burr (Münster): Functional Interpretation of Aczel’s Constructive Set Theory CZF

Abstract: We give a functional interpretation of Aczel’s constructive set theories CZF- and CZF in systems of constructive set functionals of finite types. This interpretation is obtained by a new translation, a refinement of the translation introduced by Diller and Nahm which again is an extension of Gödel’s Dialectica translation. The interpretation theorem gives characterizations of the definable set functions of CZF- and CZF in terms of constructive set functionals. In a second part we introduce constructive set theories in all finite types. We expand the interpretation to these theories and give a characterization of the new translation. Finally we show that the simplest non-trivial axiom of extensionality (for type 2) is not interpretable with constructive set-functionals. We obtain this result by adapting Howard’s notion of hereditarily majorizable functionals to set functionals.

H. de Nivelle (Amsterdam): Deciding the E+ class with an a posteriori order

Abstract: The talk is about resolution decision procedures. A resolution decision procedure is a restriction of the general resolution rule which is complete and which enforces termination of the search process for some class of first order formulae (or a class of clause sets). The E+ class is the basic class that has been shown decidable by resolution. The restriction used for the E+ class forms the basis for the decision techniques for most other classes. The technique used is an order <v which prefers those literals containing the deepest occurrence of a variable. This order is applied before the computation of the most general unifier. (a priori) This <v order is not preserved by substitution, which makes it incompatible with subsumption. I will show that the E+ class can be decided by a different order, <vd, when this order is applied after the most general unifier, i.e. a posteriori. The order <vd is preserved under substitution. This makes the restriction compatible with full subsumption. This type of work fits well into a workshop on proof theory because the techniques used allow proof theoretic proofs of decidability results, which before had only model theoretic proofs.

R. Dyckhoff (St. Andrews): Contraction-free and permutation-free calculi for some non-classical logics

Abstract: I shall discuss two kinds of sequent calculus: “contraction-free” calculi and “permutation-free” calculi, emphasising the former’s suitability for solving decision problems and the latter’s suitability for proof search (as in logic programming). The former have been investigated by Hudelmaier, myself and several others; we report mainly on recent work (joint with Sara Negri) showing how their completeness may (in some cases) be proven by rather routine methods allowing extension with quantifiers or non-logical notions like apartness. An example is given, however, of a terminating contraction-free calculus for (propositional) Dummett logic, with all rules invertible, where less routine methods still seem preferable. The latter are based on work of Herbelin, and have the property that the proofs are in 1-1 correspondence with normal natural deductions. We discuss some recent work (joint with Luis Pinto) extending the ideas to dependent type theory.

S. Feferman (Stanford): Unfolding Schematic Formal Systems

Abstract: The unfolding of schematic formal systems is a novel concept which weds: (i) functional (least fixed point) schemata for recursion over arbitrary structures, to (ii) schematic formal systems S considered in a wider, more open-ended sense than is customary in current metamathematics. The concept of unfolding is used to answer the following general question:

What operations, predicates and principles concerning them are implicit in the acceptance of a given schematic system S?

I will report on joint work with Thomas Strahm characterizing the notion(s) of unfolding for non-finitist arithmetic, and then will explain work in progress on this concept ranging from feasible and finitist arithmetic to higher set theory.

A. Hendriks (Amsterdam): Doing logic by computer

Abstract: This talk will be about computer experiments in (modal and intuitionistic) propositional logic. Some applications will be discussed of an approach to investigate questions in logic using both theorem provers and computations in Kripke models. One of the applications yields a counterexample to the interpolation property for intuitionistic propositional logic with equivalence as the only connective.

M. Hofmann (Edinburgh): Extending “safe recursion” to higher types, lists, trees, and polymorphism

Abstract: Bellantoni-Cook’s function system of “safe recursion” is a firstorder system which defines exactly the PTIME functions in a “resource free” way by imposing a certain syntactic restriction on primitive recursion on notation. We extend this idea to a typed lambda calculus with lists, trees, and polymorphism. The syntactic restriction contained in the Bellantoni-Cook approach is captured by way of an S4 modality on types. The presence of trees and higher-typed functions further introduces the need for linearity (in the sense of linear logic) in certain places. The proof that the resulting calculus defines PTIME functions only proceeds by a semantic interpretation using realisability and functor categories. The ultimate goal of this work is a realistic programming language for polynomial time. Time permitting, I will also talk about some of the obstacles which are yet to be overcome on the way.

J. Hudelmaier (Tübingen): Finding counter models in classical and intuitionistic logic

Abstract: Using the well known so called tableaux calculus for classical propositional logic, one can in a straightforward way derive Boolean counter models from failing deductions. Applying a non constructive argument the same holds for classical predicate logic. Thus one obtains a perspicuous semantical completeness proof for classical logic. While usual completeness proofs for intuitionistic logic are quite complicated it is in fact possible to extend these ideas to intuitionistic logic. For this purpose one considers a new kind of tableaux calculus which allows straightforward extraction of counter models even in intuitionistic logic.

J. Johannsen (San Diego): Exponential Separations between Restricted Resolution and Cutting Planes Proof Systems

Abstract: This talk reports joint work with M.L. Bonet, J.L. Esteban and N. Galesi. We prove an exponential lower bound for tree-like Cutting Planes refutations of a set of clauses which has polynomial size resolution refutations. This implies an exponential separation between tree-like and dag-like proofs for both Cutting Planes and resolution; in both cases only superpolynomial separations were known before. In order to prove the lower bound, the lower bounds on the depth of monotone circuits of Raz and McKenzie (FOCS 97) are extended to monotone real circuits. In the case of resolution, this result is further improved by giving an exponential separation of tree-like resolution from (dag-like) regular resolution proofs. In fact, the refutation provided to give the upper bound respects the stronger restriction of being a Davis-Putnam resolution proof. Finally, we prove an exponential separation between Davis-Putnam resolution and unrestricted resolution proofs; only a superpolynomial separation was previously known.

G. Mints (Stanford): Reductions of finite and infinite proofs

Abstract: Standard expansion of a finite proof d in arithmetic into an infinite proof h(d) provides normalization theorems for finite proofs of simple formulas, usually of complexity at most Σ_{1}. A slight modification of this expansion allows to normalize finite proofs of arbitrary formulas, even if the normal form contains eigenvariables. This approach extends to subsystems of analysis. It can be used to extract a set of reductions for finite proofs from cut-elimination for infinite proofs.

I. Moerdijk (Utrecht): Martin-Löf type theory and realisability

Abstract: We discuss “internal” models of Martin-Löf type theory. In particular, we show how to give an effective interpretation of general inductive (W-)types within a predicative metatheory. (Part of joint work with E. Palmgren, Uppsala).

V. Orevkov (St. Petersburg): The Complexity of Terms in Proofs

Abstract: The aim of this talk is to obtain upper bounds on the complexity of terms occurring in proofs in predicate calculus. We will consider Gentzen sequential calculus both with cut and without cut. The bounds make possible to compare lengths of direct and indirect proofs of existence theorems in predicate calculus. Then we will extend our results to axiomatic theories of algebraically closed and real-closed fields and to arithmetic without multiplication.

J. van Oosten (Utrecht): SDT in Modified Realizability

Abstract: Synthetic Domain Theory (SDT) is the mathematical theory that aims to find the most abstract form of axioms on a category of “domains”, so as to be able to perform the standard constructions domain theory is usually used for: semantics for programming languages, models for the lambda calculus, etc. It turns out that the axiomatization is most fruitfully studied in an intuitionistic context, where nontrivial models are available. The talk will present joint work with Alex Simpson from Edinburgh, on models of SDT in the Modified Realizability Topos. Interesting counterexamples will be exhibited.

C. Pollett (Boston): Multifunction Algebras and Provability of the Collapse of PH

Abstract: In this talk I will introduce some multifunctions algebras which for i > 1 correspond to functions computable in polynomial time with a limited number of witnessing queries to an oracle at the i − 1 level of the hierarchy. We then consider two subtheories of the well-studied bounded arithmetic theory S_{2} of Buss. Actually, one of our theories is contained in the other. Using our algebras (mainly the i = 1 variants on our algebras) we establish the following properties for these theories:

(1) Neither theory can prove the polynomial hierarchy collapses.

(2) If either theory is contained in S_{2}^{i} for some i then the polynomial hierarchy collapses.

(3) If either theory proves the polynomial hierarchy is infinite then for all i, S_{2}^{i} can separate the ith level of the hierarchy.

(4) There is an interesting initial segment of any model of the weaker theory that satisfies all of IΔ_{0} + exp.

A. A. Razborov (Moscow): Lower Bounds for Algebraic Proof Systems

Abstract: Algebraic proof systems are proof systems that operate with (commutative) multi-variable polynomials over some ring and prove facts of the form “every solution to some system of polynomial equations is also a solution to another equation”. In this talk we are specifically interested in the combinatorial framework in which we by default include into the set of axioms all equations x^{2} − x = 0 (x a variable; this ensures that we are in the Boolean world), and pay a special attention to those facts that reflect natural combinatorial principles. Algebraic proof systems originally emerged as a tool for proving lower bounds in the propositional proof complexity; more specifically, for attacking the system of constant-depth Frege proofs allowing also modular gates modulo some prime p. It soon became clear, however, that the importance of algebraic proof systems goes far beyond this particular task: they provide natural and elegant models for studying (our way of thinking about) the most basic algebraic facts and constructions. In this talk we firstly survey various connections between algebraic proof systems on the one hand, and such areas as propositional proof systems or automatic theorem proving on the other. In particular, we try to explain from the complexity perspective what makes algebraic proof systems very unique for the automatic proof generation. Then we survey lower bounds known for algebraic proof systems.

H. Schwichtenberg (München): Ramification, Modality, and Linearity in Higher Type Recursion

Abstract: It is shown how to restrict Gödel’s system T of recursion in all higher types, so that the type level 1 section consists of exactly the polynomial-time computable functions. The characterization is obtained by a novel combination of ramification and linearity, which are made to coincide through modal operations (joint work with S. Bellantoni and K.-H. Niggl).

D. Scott (Pittsburgh): Types and Computability

Abstract: Over the last year, we have been developing a circle of ideas that came up in Scott’s 1996 graduate course on domain theory. The aim is to use type theory (and topos theory) via realizability to model a constructive logic which accomodates standard types (e.g. countably based topological spaces) and domain theory (as certain countably based T_{0}-spaces), has extensive closure conditions (e.g. as a cartesian closed and locally cartesian closed category), and supports polymorphism (in the style of Girard and Reynolds or the calculus of constructions). Similar approaches having some of these advantages have been suggested many times before, but we now think better results can be achieved using realizability over the graph model for the (untyped) lambda calculus. Moreover, in this proposed interpretation, there is a clear-cut definition of a type operator #A, meaning the formation of the computable elements of the type A (which includes computable functions as a type #(A → B)). This operator can also be applied to propositions providing a constructive version of an kind of S4 modal logic. In this way it is possible for example to work both with the whole set of real numbers along with the computable numbers and functions.

The major task of the project is to show that this logic is capable of naturally formulating the constructions and proofs required for the questions of semantics of programming languages – especially in justifying the existence and properties of recursively defined types. If this is successful, there should be significant conclusions for constructuve logic as well.

T. Strahm (Bern): Abstract computations in type-free applicative systems

Abstract: Type-free applicative theories build the operational basis of Feferman’s explicit mathematics. In this talk we survey proof-theoretic aspects of various forms of abstract computation in a type-free applicative setting. In particular, we are interested in several type 2 functionals including the Suslin operator E_{1}, Kleene’s E and an operator related to the polynomial time hierarchy. Thus we discuss applicative systems ranging in proof-theoretic strength from Delta-1-2 comprehension, predicative subsystems of analysis to systems of feasible and bounded arithmetic.

G. Takeuti (Philadelphia): Forcing and P ≠ NP

Abstract: We discuss the forcing approach to P ≠ NP problem.

L. Trevisan (Boston): Interactive and Probabilistic Proof-Checking

Abstract: The informal statement that “proofs are easier to check than to find” is the intuition on which the P ≠ NP conjecture and much of Computational Complexity Theory are based. In slightly more than a decade, the notion of “checking the validity of a proof” has been stretched to unexpected limits, with surprising and useful consequences that extend beyond the limits of complexity theory. The use of randomization and interaction in proof checking (and, consequently, the notion of “probabilistically sound” proofsystems) showed how to efficiently check proofs of tautology-hood of propositional formulae, and even of quantified propositional formulae. Statements of such generality are conjectured not to have short proofs in any reasonable proof system without interaction and randomness, and it has been shown that they provably do not have short proofs in certain standard proof systems such as resolution. Parallel to this developments, the counter-intuitive notion of zero-knowledge proofs (proofs whose validity can be checked with high confidence by a proof-checker that verifies the validity of the proof without being able to replicate it afterwards) was exploited, with general and powerful applications to cryptographic protocols. Probabilistically checkable proofs are the latest development of this sort, with several applications to proving hardness of approximation for fundamental optimization problems. In our talk we will cover the sequence of ideas and techniques that led to these results, and we will mention some interesting open questions.

Abstracts of Special Lectures in Connection with the Workshop

A. Feferman (Stanford): The Saga of Alfred Tarski: Part Two

Abstract: Alfred Tarski (1901–1983), the great twentieth-century logician, came to the United States from Poland to deliver a lecture at a Unity of Science meeting; it was 1939, just two weeks before the Germans invaded Poland and World War II began. Tarski was Jewish; almost everyone knew his original name was Teitelbaum. To return to Warsaw would have been suicidal, so he remained in America and cast about for a job and a way to bring his family to the United States. It took him three years to find his first “real position”, at the University of California at Berkeley, an untenured appointment as lecturer. He was fortyone years old, almost exactly in the middle of his life (although he didn’t know that then); he was separated from his wife, his children, and all his family, who were living in the horrible war-time conditions of Warsaw, and he was isolated from his colleagues on the East Coast. On the other hand, he was fortunate to be alive and to be able to carry on his work. In my talk I will focus on some of the personal and professional details of the second half of Tarski’s life when, from a shaky, inauspicious beginning, in a place that seemed to him like a frontier town way out west, he went on to build a world famous center for logic, a mecca which attracted scholars from all over the world.

A. Wigderson (Jerusalem): Simple proofs of bounds on Resolution proof size

Abstract: We consider the width (= maximal clause size) of resolution proofs. We relate it to the classical proof size in the tree-like and general cases. This yields much simpler exponential size lower bound proofs of for simple tautologies. It also motivates a simple automatic (resolution) theorem prover, that can be tremendously more efficient than Davis-Putnam. Joint work with Eli Ben-Sasson.

12

Participants

We list here in alphabetical order all participants of the workshop and visitors in connection with it:

Norika H. Arai (Hiroshima City University)

email: arai@cs.hiroshima-cu.ac.jp

Jeremy Avigad (Carnegie Mellon University)

email: avigad@cmu.edu

Arnold Beckmann (University of Münster)

email: beckmaa@math.uni-muenster.de

Stephen J. Bellantoni (The Fields Institute, Toronto)

email: sjb@cs.utoronto.ca

Ulrich Berger (University of Munich)

email: berger@rz.mathematik.uni-muenchen.de

Maria Luisa Bonet (Universidad Politecnica de Catalunya, Barcelona)

email: bonet@lsi.upc.es

Wolfgang Burr (Westfälische Wilhelms-Universität Münster)

email: Wolfgang.Burr@math.uni-muenster.de

Carsten Butz (BRICS, University of Aarhus)

email: butz@brics.dk

Ivan Damgård (BRICS, University of Aarhus)

email: ivan@daimi.aau.dk

Olivier Danvy (BRICS, University of Aarhus)

email: danvy@brics.dk

Roy Dyckhoff (University of St. Andrews)

email: rd@dcs.st-and.ac.uk

Stefan Dziembowski (BRICS, University of Aarhus)

email: stefand@brics.dk

Anita Feferman (Stanford)

email: –

Solomon Feferman (Stanford University)

email: sf@csli.stanford.edu

Andrzej Filinski (BRICS, University of Aarhus)

email: andrzej@brics.dk

Nicola Galesi (Universidad Politecnica de Catalunya, Barcelona) email: galesi@lsi.upc.es Silvia Ghilezan (University of Novi Sad)

email: gsilvia@uns.ns.ac.yu

Mikkel Nygaard Hansen (BRICS, University of Aarhus)

email: nygaard@daimi.aau.dk

Alex Hendriks (ILLC, University of Amsterdam)

email: lhendrik@wins.uva.nl

Martin Hofmann (University of Edinburgh)

email: mxh@dcs.ed.ac.uk

Jacob Howe (University of St Andrews)

email: jacob@dcs.st-and.ac.uk

Jörg Hudelmaier (WSI, Universität Tübingen)

email: joerg@Informatik.Uni-Tuebingen.De

Thomas Hune (BRICS, University of Aarhus)

email: baris@brics.dk

Klaus Frovin Jørgensen (University of Roskilde)

email: frovin@ruc.dk

Jan Johannsen (University of California, San Diego)

email: johannsn@math.ucsd.edu

Ulrich Kohlenbach (BRICS, University of Aarhus)

email: kohlenb@brics.dk

Horst Luckhardt (University of Frankfurt/Main)

email: luckhard@mi.informatik.uni-frankfurt.de

Rune Lyngsø (BRICS, University of Aarhus)

email: rlyngsoe@brics.dk

Markus Michelbrink (Hannover University)

email: michelbrink@math.uni-hannover.de

Grigori Mints (Stanford University)

email: mints@csli.stanford.edu

Ieke Moerdijk (Utrecht University)

email: moerdijk@math.uu.nl

Georg Moser (University of Technology, Vienna)

email: moser@logic.at

Mogens Nielsen (BRICS, University of Aarhus)

email: mn@brics.dk

Jean de Nivelle (University of Amsterdam)

email: nivelle@cwi.nl

Jaap van Oosten (Utrecht University)

email: jvoosten@math.ruu.nl Vladimir Orevkov (Steklov Mathematical Institute, St. Petersburg)

email: orevkov@pdmi.ras.ru

Rasmus Pagh (BRICS, University of Aarhus)

email: pagh@brics.dk

Jakob Pagter (BRICS, University of Aarhus)

email: pagter@brics.dk

Erik Palmgren (Uppsala University)

email: palmgren@math.uu.se

Alessandro Panconesi (BRICS, University of Aarhus)

email: ale@brics.dk

Henrik Persson (Chalmers University of Technology, Gothenburg)

email: henrikp@cs.chalmers.se

Chris Pollett (Boston University)

email: cpollett@cs.bu.edu

A.A. Razborov (Steklov Mathematical Institute, Moscow)

email: razborov@genesis.mi.ras.ru

Søren Riis (BRICS, University of Aarhus)

email: smriis@brics.dk

Helmut Schwichtenberg (University of Munich)

email: schwicht@rz.mathematik.uni-muenchen.de

Dana Scott (Carnegie Mellon University)

email: dana.scott@cs.cmu.edu

Monika Seisenberger (University of Munich)

email: seisenb@rz.mathematik.uni-muenchen.de

Anton Setzer (Uppsala University)

email: setzer@math.uu.se

Jacek Skorupski (Warsaw University of Technology)

email: jsk@it.pw.edu.pl

Jan Smith (Chalmers University of Technology, Gothenburg)

email: smith@cs.chalmers.se

Thomas Strahm (University of Bern)

email: strahm@iam.unibe.ch

Gaisi Takeuti (University of Pennsylvania)

email: takeuti@saul.cis.upenn.edu

Luca Trevisan (MIT Lab. for Computer Science, Cambridge, MA)

email: luca@theory.lcs.mit.edu

René Vestergaard (University of Glasgow)

email: jrvest@dcs.gla.ac.uk Vinodchandran Variyam (BRICS, University of Aarhus)

email: vinod@brics.dk

Klaus Weich (LMU Munich)

email: weich@rz.mathematik.uni-muenchen.de

Avi Wigderson (Hebrew University, Jerusalem)

email: avi@cs.huji.ac.il

Glynn Winskel (BRICS, University of Aarhus)

email: gwinskel@brics.dk

Recent BRICS Notes Series Publications

NS-98-6 Carsten Butz, Ulrich Kohlenbach, Søren Riis, and Glynn Winskel, editors. Abstracts of the Workshop on Proof Theory and Complexity, PTAC ’98, (Aarhus, Denmark, August 3–7, 1998), July 1998. vi+16 pp.

NS-98-5 Hans Hüttel and Uwe Nestmann, editors. Proceedings of the Workshop on Semantics of Objects as Processes, SOAP ’98, (Aalborg, Denmark, July 18, 1998), June 1998. 50 pp.

NS-98-4 Tiziana Margaria and Bernhard Steffen, editors. Proceedings of the International Workshop on Software Tools for Technology Transfer, STTT ’98, (Aalborg, Denmark, July 12–13, 1998), June 1998. 86 pp.

NS-98-3 Nils Klarlund and Anders Møller. MONA Version 1.2 — User Manual. June 1998. 60 pp.

NS-98-2 Peter D. Mosses and Uffe H. Engberg, editors. Proceedings of the Workshop on Applicability of Formal Methods, AFM ’98, (Aarhus, Denmark, June 2, 1998), June 1998. 94 pp.

NS-98-1 Olivier Danvy and Peter Dybjer, editors. Preliminary Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation, NBE ’98, (Gothenburg, Sweden, May 8–9, 1998), May 1998.

NS-97-1 Mogens Nielsen and Wolfgang Thomas, editors. Preliminary Proceedings of the Annual Conference of the European Association for Computer Science Logic, CSL ’97 (Aarhus, Denmark, August 23–29, 1997), August 1997. vi+432 pp.

NS-96-15 CoFI. CASL – The CoFI Algebraic Specification Language; Tentative Design: Language Summary. December 1996. 34 pp.

NS-96-14 Peter D. Mosses. A Tutorial on Action Semantics. December 1996. 46 pp. Tutorial notes for FME ’94 (Formal Methods Europe, Barcelona, 1994) and FME ’96 (Formal Methods Europe, Oxford, 1996).

NS-96-13 Olivier Danvy, editor. Proceedings of the Second ACM SIGPLAN Workshop on Continuations, CW ’97 (ENS, Paris, France, 14 January, 1997), December 1996. 166 pp.