We show that the decomposition of intuitionistic logic into linear logic along the equation A /spl rarr/ B = !A /spl rarr/ B may be adapted into a decomposition of classical logic into LLP, the polarized version of Linear Logic. Firstly, we build a categorical model of classical logic (a control category) from a categorical model of linear logic by a construction similar to the co-Kleisli category. Secondly, we analyze two standard continuation-passing style (CPS) translations, the Plotkin and the Krivine's translations, which are shown to correspond to two embeddings of LLP into LL.

A general category of games is constructed. A subcategory of saturated strategies, closed under all possible codings in copy games, is shown to model reduction in classical linear logic.

The interaction processes at work by M. Hyland and L. Ong (1994) (HO) and S. Abramsky et al. (1994) (AJM) new game semantics are two preexisting paradigmatic implementations of linear head reduction: respectively Krivine's abstract machine and Girard's interaction abstract machine. There is a simple and natural embedding of AJM-games to HO-games, mapping strategies to strategies and reducing AJM definability (or full abstraction) property to HO's one.

Since the rebirth of /spl lambda/-calculus in the late 1960s, three major theoretical investigations of /spl beta/-reduction have been undertaken: (1) Levy's (1978) analysis of families of redexes (and the associated concept of labeled reductions); (2) Lamping's (1990) graph-reduction algorithm; and (3) Girard's (1988) geometry of interaction. All three studies happened to make crucial (if not always explicit) use of the notion of a path, namely and respectively: legal paths, consistent paths and regular paths. We prove that these are equivalent to each other.>

The authors build a confluent, local, asynchronous reduction on lambda -terms, using infinite objects (partial injections of Girard's (1988) algebra L*), which is simple (only one move), intelligible (semantic setting of the reduction), and general (based on a large-scale decomposition of beta ), and may be mechanized.>

J.-Y. Girard (Proc. ASL Meeting, 1988) proposed an interpretation of second order lambda -calculus in a C algebra and showed that the interpretation of a term is a nilpotent operator. By extending to untyped lambda -calculus the functional analysis interpretation for typed lambda -terms, V. Danos (Proc. 3rd Italian Conf. on Theor. Comput. Sci., 1989) showed that all and only strongly normalizable terms are interpreted by nilpotent operators; in particular all and only nonstrongly normalizable terms are interpreted by infinite sums of operators. It is shown that interpretation of lambda -terms always makes sense, by showing that lambda -terms are interpreted by weakly nilpotent operators in the sense of Girard. This result is obtained as a corollary of an aperiodicity property of execution of lambda -terms, which seems to be related to some basic property of environment machines.>