Abstract

Abstract
The computational efficiency of linear ?-calculi with iterators is evaluated using closed reduction strategies. The interaction between linearity and closed reduction and the computational power of linear systems with and without closed reduction is analyzed. A linear version of Gödel's System T with closed reductions is defined to analyze the computational power of linear systems. Closed reduction strategies in the ?-calculus restrict the reduction rules since closed reduction strategies can take place when certain terms are closed and do not contain free variables. Closed reduction strategies impose strong constraints on the application of reduction rules. Closed reduction strategies can simulate call-by-name and call-by-value evaluations in the ?-calculus. Linear ?-calculus with iterators can be efficiently analyzed by relaxing the constraints on the construction of iterator terms.

Abstract
System L is a linear A-calculus with numbers and an iterator, which, although imposing linearity restrictions on terms, has all the computational power of Godel's System T. System C owes its power to two features: the use of a closed reduction strategy (which permits the construction of an iterator on an open function, but only iterates the function after it becomes closed), and the use of a liberal typing rule for iterators based on iterative types. In this paper, we study these new types, and show how they relate to intersection types. We also give a sound and complete type reconstruction algorithm for System L.

Abstract
We show that the full PCF language can be encoded in L-rec, a syntactically linear lambda-calculus extended with numbers, pairs, and an unbounded recursor that preserves the syntactic linearity of the calculus. We give call-by-name and call-by-value evaluation strategies and discuss implementation techniques for L-rec, exploiting its linearity.

Abstract
In this paper we present an implementation of the general system for type inference algorithms HM(X), using Prolog and Constraint Handling Rules. In our implementation the difference between the general aspects of the type inference algorithms and the constraint resolution module becomes clearer, when compared to other implementations of the same systems, usually made in a functional programming language. In the constraint module, solving equality constraints, here implemented by Prolog unification, is completely separated from constraint simplification, which is made by a solver implemented in CHR for each system. CHR rules become a clear and natural way of specifying the simplification mechanism. © 2002 Publishd by Elsevier Science B.V.

Abstract
We identify a restricted class of terms of the lambda calculus, here called weak linear, that includes the linear lambda-terms keeping their good properties of strong normalization, non-duplicating reductions and typability in polynomial time. The advantage of this class over the linear lambda-calculus is the possibility of transforming general terms into weak linear terms with the same normal form. We present such transformation and prove its correctness by showing that it preserves normal forms.