Type theory is one of the most important tools in the design of higher-level programming
languages, such as ML. This book introduces and teaches its techniques by focusing on one …

This paper is meant to be a survey about implicit characterizations of complexity classes by
fragments of higher-order programming languages, with a special focus on type systems …

Abstract Zaionc, M., λ-Definability on free algebras, Annals of Pure and Applied Logic 51
(1991) 279-300. A λ-language over a simple type structure is considered. There is a natural …

There is a natural isomorphism identifying second order types of the simple typed λ calculus
with free homogeneous term algebras. Let τ A and τ B be types representing algebras A and …

Six λ-languages over function-types between algebras B, N and Υ are considered. Type
N=(0→ 0)→(0→ 0) is called a non-negative integers type; B=(0→ 0)→((0→ 0)→(0→ 0)) is …

In this paper, we study λ→-representability of functions over (open or closed) term algebras.
First, by extending the standard notion of λ→-representation of closed (or variable-free) …

In the paper we consider a-language over the type (N! N)! N where the type N=(0! 0)!(0! 0) is
called a Church numeral type. As opposed to the rst order-representability in the type (N! N) …

Ti,..,~ T~ 0 where T= 0 L~ 0. it can be seen that closed terms of the type T reflex
constructions in the algebra A. Therefore any term of the type (TA) n~ TA defines some n-ary …