ABSTRACT This paper gives a new proof of confluence for Carraro and Guerrieri’s call-by-value lambda calculus λvσ with permutation rules. We adapt the compositional Z theorem to λvσ.

We study a version of the Stone duality between the Alexandrov spaces and the completely distributive algebraic lattices.This enables us to present lattice-theoretical models of second-order intuitionistic propositional logic which correlates with the Kripke models introduced by Sobolev.This can be regarded as a second-order extension of the well-known correspondence between Heyting algebras and Kripke models in the semantics of intuitionistic propositional logic.

We show that an upper bound function for the Church–Rosser theorem of type-free λ-calculus with β-reduction must be in the fourth level of the Grzegorczyk hierarchy, i.e., the smallest Grzegorczyk class properly extending the class of elementary functions. At this level we also find common reducts for the confluence property. The proof method here can be applied not only to type-free λ-calculus with βη-reduction but also to typed λ-calculi such as Pure Type Systems.

It is well-known that the type-checking and type-inference problems are undecidable for second order lambda-calculus in Curry-style, although those for Church-style are decidable. What causes the differences in decidability and undecidability on the problems? We examine crucial conditions on terms for the (un)decidability property from the viewpoint of partially typed terms, and what kinds of type annotations are essential for (un)decidability of type-related problems. It is revealed that there exists an intermediate structure of second order lambda-terms, called a style of hole-application, between Church-style and Curry-style, such that the type-related problems are decidable under the structure. We also extend this idea to the omega-order polymorphic calculus F-omega, and show that the type-checking and type-inference problems then become undecidable.

We consider here a number of variations on the System F, that are predicative second-order systems whose terms are intermediate between the Curry style and Church style. The terms here contain the information on where the universal quantifier elimination and introduction in the type inference process must take place, which is similar to Church forms. However, they omit the information on which types are involved in the rules, which is similar to Curry forms. In this paper we prove the undecidability of the type-checking, type inference and typability problems for the system. Moreover, the proof works for the predicative version of the system with finitely stratified polymorphic types. The result includes the bounds on the Leivant’s level numbers for types used in the instances leading to the undecidability.