The context of this paper is the type-theoretic or logical approach to semantics of untyped lambda calculus introduced by Barendregt, Dezani, and Coppo in the early eighties. The idea is this: to interpret some extension of the untyped lambda calculus one introduces a Curry-style type system and defines the semantic meaning of a (closed) term \(M\) as the set \([M]\) of types it can be assigned to. Provided the type system was chosen sufficiently expressive then one obtains a completeness result of the form: \([{M}]=[{N}]\) if and only if \(M\) and \(N\) are observationally equivalent (yield the same result in arbitrary context). In general, such completeness result will require a subtyping relation on types \(\sigma\leq\tau\) and intersection types \(\sigma\wedge\tau\) together with typing and subtyping rules which ensure that the types become a meet semilattice with \(\wedge\) the meet operation and that the sets \([{M}]\) are filters. The latter effect is achieved by the subsumption rule \(M:\sigma\) implies \(M':\tau\) when \(\sigma\leq\tau\) and by the intersection rule \(M:\sigma\wedge \tau\) provided \(M:\sigma\) and \(M:\tau\). These filters (ordered by reverse inclusion) form a distributive lattice and this establishes a link to the (more standard) order-theoretic approach to semantics of \(\lambda\)-calculus pioneered by Scott. The type-theoretic approach can be advantageous in situations where one does not know a priori what form a semantic model should have. This is precisely the case in the situation of the paper under review. A type-theoretic semantics is given to an extension of the untyped lambda calculus with two nondeterministic constructs: \(M+N\) (demonic nondeterministic choice between \(M\) and \(N\)) and \(M\parallel N\) (parallel composition of \(M\) and \(N\)). Such extension is aimed at providing a metalanguage for concurrent programming languages in the same way as (following Scott-Strachey) the untyped lambda calculus provides a universal metalanguage for functional and imperative programming languages. In addition to these nondeterministic constructs the calculus has two kinds of abstraction: \(\lambda v.M\) (eager abstraction) and \(\lambda x.M\) (lazy abstraction) . A small step operational semantics is given whose distinctive features are: 1) the rules \(M+N\rightarrow M\) and \(M+N\rightarrow N\) for nondeterministic choice, 2) the rule \(M\parallel N\rightarrow M'\parallel N'\) when \(M\rightarrow M'\) and \(N\rightarrow N'\) for parallel composition, 3) the parallel eager \(\beta\)-reduction rule (in addition to standard \(\beta\)-reduction for lazy abstractions): \((\lambda v.M)V\rightarrow M[V/v]\parallel (\lambda v.M)V'\) when \(V\) is a value (variable, abstraction, or parallel composition with at least one factor a value) and \(V\rightarrow V'\). There are a number of less prominent rules for which I refer to the paper. The first technical part of the paper (Section 2) is devoted to a syntactical study of this operational semantics. The main concept is the ``bar'': a finite set of terms \(b\) is a bar of some term \(M\) if every maximal reduction sequence starting from \(M\) intersects \(b\). This allows to define ``must convergence'' by \(M{\Downarrow}\) iff \(M\) has a bar consisting of values. Two terms \(M,N\) are called observationally equivalent, symbolically \(M\simeq^{\mathcal O}N\), iff \(C[M]{\Downarrow} \Leftrightarrow C[N]{\Downarrow}\) for all contexts \(C[ ]\) (terms with a designated hole \([ ]\). An important technical tool is the definition of an auxiliary reduction relation \(M \triangleright N\) which is Church-Rosser and moreover has the property that if \(\{M_1,\dots,M_n\}\) is a bar of \(M\) then \(M\triangleright M_1+\dots+M_n\) (Lemma 2.9). This, together with the inductive definition of \(\triangleright\) provides the following characterisation of convergence: if \(M\triangleright N\) and \(M{\Downarrow}\) then also \(N{\Downarrow}\) (Theorem 2.12). The second part (Section 3) is aimed at a type-theoretic characterisation of observational equivalence. To that end a type system with one base type \(\omega\) and three binary type formers \(\tau_1\rightarrow \tau_2\) (function space), \(\tau_1\wedge\tau_2\) (intersection type), and \(\tau_1\vee\tau_2\) (union type) is introduced. The subtyping relation on the set of types is the least partial ordering \(\leq\) such that \(\omega\) is the largest element, \(\wedge,\vee\) are binary meet and join, and \(\rightarrow\) is antitone in its first argument and monotone in its second argument. The type assignment system is fairly canonical. The rules governing the typing of the new constructs are as follows. Every term has type \(\omega\). The type formers \(\wedge\) and \(\vee\) are used to type parallel composition and nondeterministic choice, respectively. An eager abstraction \(\lambda v.M\) gets type \(\sigma{\rightarrow}\tau\) if \(M:\tau\) under \(v:\sigma_i\) for each \(\sigma_i\) appearing in a join-irreducible decomposition \(\sigma=\sigma_1\vee\dots\vee \sigma_n\). The authors argue that it is this latter rule which makes the main completeness result go through: \(M{\Downarrow}\) iff \(M:\omega\rightarrow\omega\) (Theorem 3.23 (\(\Rightarrow\)) and Corollary 5.6 (\(\Leftarrow\))). The \(\Leftarrow\)-direction is first proved for values by direct induction and then lifted to all terms by way of Lemma 2.9 and a subject expansion property for \(\triangleright\) (Theorem 3.22). The \(\Leftarrow\)-direction of completeness builds upon a semantic characterisation of typeability: \(M:\tau\) iff \(M\in[\tau]\) where \([-]\) is an interpretation of types in the lattice of those sets of terms which satisfy certain closure properties formulated in Lemma 5.4. Finally, in Section 5.3 things are put together to obtain the main result: \(M\simeq^{\mathcal O} N\) iff \(M:\tau\Leftrightarrow N:\tau\) for all types \(\tau\) (Theorem 5.11). In fact, following common practice a slightly more general preorder version is proved. Section 4, which probably should go after Section 5, relates the type-theoretic semantics to a domain-theoretic interpretation of the calculus in the least solution \(D\) in the category of prime algebraic lattices of the domain equation \(D={\mathcal P}^{\#}([D{\rightarrow}D]_{\bot})\) where \({\mathcal P}^{\#}\) is the upper or Smyth powerdomain functor. Section 6 as well as parts of the Introduction form a comprehensive discussion of related work. It emerges from this that, although extensions of Curry typing with intersection and union types have been around for a while, the connection with a concurrent language boasting both nondeterminism and parallelism is new. In the reviewers opinion the resulting system is surprisingly natural and makes a strong case for the type-theoretic approach in this context. Given the ongoing interest in extending functional programming languages with concurrency primitives, the paper is a timely contribution and well worth reading.