We present FJ&$\lambda$, a new core calculus that extends Featherweight Java (FJ) with interfaces, supporting multiple inheritance in a restricted form, $\lambda$-expressions, and intersection types. Our main goal is to formalise how lambdas and intersection types are grafted on Java 8, by studying their properties in a formal setting. We show how intersection types play a significant role in several cases, in particular in the typecast of a $\lambda$-expression and in the typing of conditional expressions. We also embody interface \emph{default methods} in FJ&$\lambda$, since they increase the dynamism of $\lambda$-expressions, by allowing these methods to be called on $\lambda$-expressions. The crucial point in Java 8 and in our calculus is that $\lambda$-expressions can have various types according to the context requirements (target types): indeed, Java code does not compile when $\lambda$-expressions come without target types. In particular, in the operational semantics we must record target types by decorating $\lambda$-expressions, otherwise they would be lost in the runtime expressions. We prove the subject reduction property and progress for the resulting calculus, and we give a type inference algorithm that returns the type of a given program if it is well typed. The design of FJ&$\lambda$ has been driven by the aim of making it a subset of Java 8, while preserving the elegance and compactness of FJ. Indeed, FJ&$\lambda$ programs are typed and behave the same as Java programs.

This paper aims at incorporating the notion of self-adaptiveness in the context of multiparty sessions, by focusing on the issue of ensuring correctness for dynamic adaptations. A formal framework is presented centred around these main ingredients: global types, monitors and global state. A global type represents the overall communication choreography. Its projections are the monitors, which set-up the protocols of the participants. The association of a monitor with a compliant process incarnates a single participant. It is the choreography that is updated at runtime, in response to changing conditions in the global state. Monitors result to be self-adaptive in the sense that they react to these changes by modifying themselves, in order to prescribe new behaviours to the participants.

Guaranteeing that the parties of a network application respect a given protocol is a crucial issue.Session typesoffer a method for abstracting and validating structured communication sequences (sessions).Object-oriented programmingis an established paradigm for large scale applications.Union types, which behave as the least common supertypes of a set of classes, allow the implementation of unrelated classes with similar interfaces without additional programming. We have previously developed an integration of the features above into a class-based core language for building network applications, and this successfully amalgamated sessions and methods so that data can be exchanged flexibly according to communication protocols (session types). The first aim of the work reported in this paper is to provide a full proof of the type safety property for that core language by renewing syntax, typing and semantics. In this way, static typechecking guarantees that after a session has started, computation cannot get stuck on a communication deadlock. The second aim is to define a constraint-based type system that reconstructs the appropriate session types of session declarations instead of assuming that session types are explicitly given by the programmer. Such an algorithm can save programming work, and automatically presents an abstract view of the communications of the sessions.

Double dispatch is the ability to dynamically select a method not only according to the run-time type of the receiver (single dispatch), but also according to the run-time type of the argument. This mechanism unleashes the power of dynamic binding in object-oriented languages, so enhancing re-usability and separation of responsibilities. However, many mainstream languages, such as, e.g., C++ and Java, do not provide it, resorting only to single dispatch. In this paper we propose an extension of C++ (also applicable to other object-oriented languages) that enables double dispatch as a language feature. This yields dynamic overloading and covariant specialization of methods. We define a translation from the new constructs to standard C++ and we present the preprocessor implementing this translation, called doublecpp. The translated code enjoys static type safety and implements the semantics of double dispatch by using only standard mechanisms of static overloading and dynamic binding, with minimal impact on the performance of the program. Copyright © 2006 John Wiley & Sons, Ltd.

The aim of this paper is to investigate, in the Curry-Howard isomorphism approach, a logical characterization for the intersection-type discipline. First a novel formulation of the intersection type inference for combinatory logic is presented, such that it is equivalent to the original version of the system, while the intersection operator is no longer dealt with as a proof-theoretical connective. Then a Hilbert-style axiomatization is defined and proved to totally parallel intersection-derivability, in such a way that inhabited intersection-types are all and only the provable formulae in the logic system.

The main idea of this paper is to develop an inference system to assign partial types to terms of the untyped lambda calculus. A term can either be necessarily or possibly of a certain type; these notions of necessity and possibility are incorporated into the type inference system as modalities. A subclass of types are the total types, for which necessity and possibility are equivalent. In the semantics the meaning of a total type is a set of values in the domain, the meaning of a type being, in general, an interval (a set of sets of values). This is a generalization of Cartwright’s semantics [Conference Record of the 12th Annual ACM Symposium on Principles of Programming Languages, Association for Computing Machinery, New York, 1984, pp. 22–36]. The main results are the soundness and completeness of the type inference system with respect to interval semantics.