ABSTRACT. Higher-order model checking is the model checking of infinite trees generated by simply-typed lambda calculus with recursion. Although the original decidability proof was based on game semantics, intersection types have played a prominent role in the subsequent development of algorithms for higher-order model checking. In this talk, I will introduce the approach to higher-order model checking based on intersection types, present connections with game semantics, and discuss recent applications of intersection types and game semantics to problems in higher-order computation.

ABSTRACT. We show that the relational theory of intersection types known as BCD has the finite model property; that is, BCD is complete for its finite models. Our proof uses rewriting techniques which have as an immediate by product the polynomial time decidability of the preorder [ (although this also follows from the so called beta soundeness of BCD).

ABSTRACT. Type isomorphism is useful for retrieving library components, since a function in a library can have a type different from, but isomorphic to, the one expected by the user. Moreover type isomorphism gives for free the coercion required to include the function in the user program with the correct type. In presence of intersection and union types, type isomorphism is not a congruence and cannot be characterised in an equational way. A characterisation can still be given, which is quite complicated by the interference between functional and non functional types. The present paper faces this problem, by interpreting each atomic type as the set of functions mapping any argument into the interpretation of the type itself. This is done taking inspiration from the initial projection of Scott's inverse limit lambda-model. In particular, an isomorphism preserving reduction between types is defined. The main results of this paper are, on one hand, the fact that two types with the same normal form are isomorphic, on the other hand, an interesting condition assuring isomorphism between types.

ABSTRACT. We present intersection type systems in the style of sequent calculus, modifying the systems that Valentini introduced to prove normalisation properties without using the reducibility method. Our systems are more natural than Valentini's ones and equivalent to the usual natural deduction style systems. We prove the characterisation theorems of strong and weak normalisation through the proposed systems, and, moreover, the approximation theorem without using the reducibility method. This provides in a uniform way proofs of the normalisation and approximation theorems via type systems in sequent calculus style.

ABSTRACT. In recent work, Kobayashi observed that the acceptance by an alternating tree automaton A of an infinite tree T generated by a higher-order recursion scheme G may be formulated as the typability of the recursion scheme G in an appropriate intersection type system associated to the automaton A. The purpose of this article is to establish a clean connection between this line of work and Bucciarelli and Ehrhard's indexed linear logic. This is achieved in two steps. First, we recast Kobayashi's result in an equivalent infinitary intersection type system where intersection is not idempotent anymore. Then, we show that the resulting type system is a fragment of an infinitary version of Bucciarelli and Ehrhard's indexed linear logic. While this work is very preliminary and does not integrate key ingredients of higher-order model-checking like priorities, it reveals an interesting and promising connection between higher-order model checking and linear logic.

ABSTRACT. Scripting code may present maintenance problems in the long run. There is, then, the call for methodologies that make it possible to control the properties of programs written in dynamic languages in an automatic fashion. We introduce Lucretia, a core language with an introspection primitive. Lucretia is equipped with a (retrofitted) static type system based on local updates of types that describe the structure of objects being used. In this way, we deal with one of the most dynamic features of scripting languages, that is, the runtime modification of object interfaces. Judgements in our systems have a Hoare-like shape, as they have a precondition and a postcondition part. Preconditions describe static approximations of the interfaces of visible objects before a certain expression has been executed and postconditions describe them after its execution. The field update operation complicates the issue of aliasing in the system. We cope with it by introducing intersection types in method signatures.

ABSTRACT. We present a new type system combining refinement types and the expressiveness of intersection type discipline. The use of such features makes it possible to derive more precise types than in the original refinement system. We have been able to prove several interesting properties for our system (including subject reduction) and developed an inference algorithm, which we proved to be sound.

ABSTRACT. We consider a formalization of mixins composition and class linearization yielding a class in mixin-based inheritance. We provide an interpretation of the mixin calculus into a lambda-calculus extended with records and a record merge operator. After extending the BCD intersection type assignment to such calculus showing that types are preserved by subject expansion and reduction, we naturally interpret mixin terms as the sets of the types that can be deduced of their translations. It turns out that the class obtained from a composition of mixins and the composition itself have the same logical meaning.

ABSTRACT. In the object oriented world existing inheritance concepts have been extended by mixins to assist modular software design. Actually, most languages only have limited mixin support. We use staged computation proposed by Davies and Pfenning together with a specification following an interface based design pattern to introduce mixins to Java 8. We present a synthesis based approach for mixin composition guided by user annotated semantics translated to intersection types. Synthesis results in meaningful Java code utilizing delegation to augment existing classes with mixin features.