This paper is about a categorical approach for modelling the pure (i.e., without constants) call-by-value λ-calculus, defined by Plotkin as a restriction of the call-by-name λ-calculus. In particular, we give the properties that a category Cbv must enjoy to describe a model of call-by-value λ-calculus. The category Cbv is general enough to catch models in Scott Domains and Coherence Spaces.

This paper unveils and motivates an ambitious programme of hidden algebraic research in software engineering. We begin with an outline of our general goals, continue with an overview of results, and conclude with a discussion of some future plans. The main contribution is powerful hidden coinduction techniques for proving behavioural correctness of concurrent systems, and several mechanical proofs are given using OBJ3. We also show how modularization, bisimulation, transition systems, concurrency and combinations of the functional, constraint, logic and object paradigms fit into hidden algebra.

We study the relationship between the encodings of the λ-calculus into π-calculus, the Continuation Passing Style (CPS) transforms, and the compilation of the Higher-Order π-calculus (HOπ) into π-calculus. We factorise the π-calculus encodings of (untyped as well as simply-typed) call-by-name and call-by-value λ-calculus into three steps: a CPS transform, the inclusion of CPS terms into HOπ and the compilation from HOπ to π-calculus. The factorisations are used both to derive the encodings and to prove their correctness.

We give a formulation of simple type theory in which types are just sets. This theory is obtained by relativizing quantifiers and replacing typing predicates by membership of some sets. It can easily be extended to include predicate subtyping.

We discuss new ways of characterizing, as maximal fixed points of monotone operators, observational congruences on λ-terms and, more generally, equivalences on applicative structures. These characterizations naturally induce new forms of coinduction principles for reasoning on program equivalences, which are not based on Abramsky's applicative bisimulation. We discuss, in particular, what we call the cartesian coinduction principle, which arises when we exploit the elementary observation that functional behaviours can be expressed as cartesian graphs. Using the paradigm of final semantics, the soundness of this principle over an applicative structure can be expressed easily by saying that the applicative structure can be construed as a strongly extensional coalgebra for the functor ([Pscr ](- × -))[oplus ]([Pscr ](- × -)). In this paper we present two general methods for showing the soundness of this principle. The first applies to approximable applicative structures – many CPO λ-models in the literature and the corresponding quotient models of indexed terms turn out to be approximable applicative structures. The second method is based on Howe's congruence candidates, which applies to many observational equivalences. Structures satisfying cartesian coinduction are precisely those applicative structures that can be modelled using the standard set-theoretic application in non-wellfounded theories of sets, where the Foundation Axiom is replaced by the Axiom X1 of Forti and Honsell.

We present the λ-calculus with resources λr, and two variants of it: a deterministic restriction λm and an extension λcr with a convergence testing operator. These calculi provide a control on the substitution process – deadlocks may arise if not enough resources are available to carry out all the substitutions needed to pursue a computation. The design of these calculi was motivated by Milner's encoding of the λ-calculus in the π-calculus. As Boudol and Laneve have shown elsewhere, the discriminating power of λm (given by the contextual observational equivalence) over λ-terms coincides with that induced by Milner's π-encoding, and coincides also with that provided by the lazy algebraic semantics (Lévy–Longo trees). The main contribution of this paper is model-theoretic. We define and solve an appropriate domain equation, and show that the model thus obtained is fully abstract with respect to λcr. The techniques used are in the line of those used by Abramsky for the lazy λ-calculus, the main departure being that the resource-consciousness of our calculi leads us to introduce a non-idempotent form of intersection types.

We give a negative answer to the question of whether every partial combinatory algebra can be completed. The explicit counterexample will be an intricately constructed term model. The construction and the proof that it works depend heavily on syntactic techniques. In particular, it provides a nice example of reasoning with elementary diagrams and descendants. We also include a domain-theoretic proof of the existence of an incompletable partial combinatory algebra.

Natural restrictions on the syntax of the second-order (i.e., polymorphic) lambda calculus are of interest for programming language theory. One of the authors showed in Leivant (1991) that when type abstraction in that calculus is stratified into levels, the definable numeric functions are precisely the super-elementary functions (level [Escr ]4 in the Grzegorczyk Hierarchy). We define here a second-order lambda calculus in which type abstraction is stratified to levels up to ωω, an ordinal that permits highly uniform (and finite) type inference rules. Referring to this system, we show that the numeric functions definable in the calculus using ranks < ω[lscr ] are precisely Grzegorczyk's class [Escr ][lscr ]+3 ([lscr ] [ges ] 1). This generalizes Leivant (1991), where this is proved for [lscr ] = 1. Thus, the numeric functions definable in our calculus are precisely the primitive recursive functions.