This paper introduces trust analysis for higher-order languages. Trust analysis encourages the programmer to make explicit the trustworthiness of data, and in return it can guarantee that no mistakes with respect to trust will be made at run-time. We present a confluent λ-calculus with explicit trust operations, and we equip it with a trust-type system which has the subject reduction property. Trust information is presented as annotations of the underlying Curry types, and type inference is computable in O(n3) time.

A combinatory system (or equivalently the set of its basic combinators) is called combinatorially complete for a functional system, if any member of the latter can be defined by an entity of the former system. In this paper the decision problem of combinatory completeness for finite sets of proper combinators is studied for three subsystems of the pure lambda calculus. Precise characterizations of proper combinator bases for the linear and the affine λ-calculus are given, and the respective decision problems are shown to be decidable. Furthermore, it is determined which extensions with proper combinators of bases for the linear λ-calculus are combinatorially complete for the λI-calculus.

In this paper we present the algebraic-λ-cube, an extension of Barendregt's λ-cube with first- and higher-order algebraic rewriting. We show that strong normalization is a modular property of all the systems in the algebraic-λ-cube, provided that the first-order rewrite rules are non-duplicating and the higher-order rules satisfy the general schema of Jouannaud and Okada. We also prove that local confluence is a modular property of all the systems in the algebraic-λ-cube, provided that the higher-order rules do not introduce critical pairs. This property and the strong normalization result imply the modularity of confluence.

Among the many flavours of balanced binary trees, Braun trees (Braun and Rem, 1983) are perhaps the most circumscribed. For any given node of a Braun tree, the left subtree is either exactly the same size as the right subtree, or one element larger. Braun trees always have minimum height, and the shape of each Braun tree is completely determined by its size. In return for this rigor, algorithms that manipulate Braun trees are often exceptionally simple and elegant, and need not maintain any explicit balance information.

Braun trees have been used to implement both flexible arrays (Braun and Rem, 1983; Hoogerwoord, 1992; Paulson, 1996) and priority queues (Paulson, 1996; Bird, 1996). Most operations involving a single element (e.g. adding, removing, inspecting or updating an element) take O(log n) time, since the trees are balanced. We consider three algorithmically interesting operations that manipulate entire trees. First, we give an O(log2n) algorithm for calculating the size of a tree. Second, we show how to create a tree containing n copies of some element x in O(log n) time. Finally, we describe an order-preserving algorithm for converting a list to a tree in O(n) time. This last operation is not nearly as straightforward as it sounds!