We introduce a new presentation of the intersection type discipline in which typing judgments derive vectors of types rather than single types. The system uses binary relations to control the flow of information between coordinates of these vectors. We refer to this presentation as system R. The maximal length of type vectors assigned to variables serves as a reasonable notion of dimension for system R, which allows for a natural stratification into fragments of bounded dimension. The present system lies strictly between two known bounded-dimensional systems: the multiset-dimensional system, for which inhabitation is EXPSPACE-complete, and the set-dimensional system, for which inhabitation is undecidable. Our main result is that inhabitation in bounded system R is decidable in 2-EXPTIME, while for each fixed dimension, inhabitation is decidable in EXPTIME. This result is based on a subformula property restricting the inhabitant search space. Unlike in traditional intersection type systems, the proof of the subformula property requires careful treatment of the additional information flow management capabilities. Finally, we argue that system R and its stratification is a valid presentation of the intersection type discipline. First, by proving the subject reduction property for system R in each bounded dimension, and second, by establishing a correspondence with the classical intersection type system of Barendregt, Coppo, and Dezani-Ciancaglini.

Abstract Predicate intuitionistic logic is a well-established fragment of dependent types. Proof construction in this logic, as the Curry–Howard isomorphism states, is the process of program synthesis. We present automata that can handle proof construction and program synthesis in full intuitionistic first-order logic. Given a formula, we can construct an automaton such that the formula is provable if and only if the automaton has an accepting run. As further research, this construction makes it possible to discuss formal languages of proofs or programs, the closure properties of the automata and their connections with the traditional logical connectives.

Abstract We propose an interpretation of the first-order answer set programming (FOASP) in terms of intuitionistic proof theory. It is obtained by two polynomial translations between FOASP and the bounded-arity fragment of the Σ1 level of the Mints hierarchy in first-order intuitionistic logic. It follows that Σ1 formulas using predicates of fixed arity (in particular unary) is of the same strength as FOASP. Our construction reveals a close similarity between constructive provability and stable entailment, or equivalently, between the construction of an answer set and an intuitionistic refutation. This paper is under consideration for publication in Theory and Practice of Logic Programming

Declarative programming features are gradually included in the design of object-oriented languages such as Java and C++. These languages recently adopted anonymous function definitions and offer basic primitives that restrict changes on data, namely final and const keywords, respectively.

We show that the constructive predicate logic with positive (covariant) quantification is hard for doubly exponential universal time, that is, for the class co- 2-N exptime . Our approach is to represent proof-search as computation of an alternating automaton. The memory of the automaton is structured in a way that strictly corresponds to scopes of the binders used in the constructed proof. This provides an application of automata-theoretic techniques in proof theory.

Automata theoretical techniques are developed that handle inhabitant search in the simply typed lambda calculus. The automata-theoretic model for inhabitant search, which can be viewed as proof search by the Curry-Howard isomorphism, is proven to be adequate by reduction of the inhabitant existence problem to the emptiness problem for the automata. To strengthen the claim, it is demonstrated that the latter has the same complexity as the former. We also discuss the basic closure properties of the automata.

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.

A common assumption for the state-of-the-art methods of protocol testing is that the protocol description is precise, unambiguous and fully determined. Unfortunately, in many practical situations this assumption turns out to be unrealistic. We propose an architecture of a testing framework where different aspects and facets of protocols are separated in a clear manner so that the adaptation of the framework to amendments in protocol description is relatively straightforward. This architecture is realised in a testing framework for RCS mobile phone protocol suite we developed in cooperation with Samsung Electronics. The framework successfully went through a number of adjustments to accommodate new interpretations of RCS protocols as assimilated by the developers.

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.

A simple type σ is retractable to a simple type τ if there are two termsCσ→τandDτ→σsuch thatD○C λx.x. The retractability of types is affine if the termsCandDare affine, that is, when every bound variable occurs in them at most once in the scope of its declaration. This paper presents a system that derives affine retractability for simple types. It also studies the complexity of constructing these affine retractions. The problem of affine retractability is NP-complete even for the class of types over a single type atom and having limited functional order. In addition, a polynomial algorithm for types of orders less than three is presented.

We present a proof of the undecidability of type inference for the Church-style system F --- an abstraction of polymorphism. A natural reduction from the second-order unification problem to type inference leads to strong restriction on instances --- arguments of variables cannot contain variables. This requires another proof of the undecidability of the second-order unification since known results use variables in arguments of other variables. Moreover, our proof uses elementary techniques, which is important from the methodological point of view, because Goldfarb's proof [Gol81] highly relies on the undecidability of the tenth Hilbert's problem. 1 1 Introduction The Church-style system F was independently introduced by Girard [Gir72] and Reynolds [Rey74] as an extension of the simply-typed -calculus a type system introduced of H. B. Curry [Cur69]. As usual for type systems, the decidability of so called sequent decision problems was considered. A sequent decision problem in some ty...