This paper aims at incorporating the notion of self-adaptiveness in context multiparty sessions, by focusing on issue ensuring correctness for dynamic adaptations. A formal framework is presented centred around these main ingredients: global types, monitors and state. type represents overall communication choreography. Its projections are monitors, which set-up protocols participants. The association a monitor with compliant process incarnates single participant. It choreography that updated...

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

The aim of this paper is to investigate a Curry-Howard interpretation the intersection and union type inference system for Combinatory Logic. Types are interpreted as formulas Hilbert-style logic L, which turns out be an extension intuitionistic with respect provable disjunctive (because new equivalence relations on formulas), while implicational-conjunctive fragment L still logic. Moreover, typable terms translated in typed version, so that $\vee$-$\wedge$-typed combinatory proved...

We present FJ&$\lambda$, a new core calculus that extends Featherweight Java (FJ) with interfaces, supporting multiple inheritance in restricted form, $\lambda$-expressions, and intersection types. Our main goal is to formalise how lambdas types are grafted on 8, by studying their properties formal setting. show play significant role several cases, particular the typecast of $\lambda$-expression typing conditional expressions. also embody interface \emph{default methods} since they increase...

We aim at investigating the intersection-type assignment system for lambda calculus, with Curry-Howard approach. devise a propositional logic, whose notable characteristic is presence of hyperformulae denoting parallel compositions formulae. As such, this logic formalizes novel notion deductions, while forming simple generalization standard natural deduction framework. prove that logical calculus isomorphic to intersection type system, by mapping deductions into typed terms, encoding those...

Class inheritance and dynamic binding are the key features of object-oriented programming they permit designing developing complex systems. However, standard class is essentially static cannot be directly employed for modeling object behaviors. In this paper we propose a linguistic extension Java, called Dec-Java, that partially inspired by decorator design pattern. This permits easily separating basic objects (that likely not to change during application) from their behaviors (that,...

Multi-methods (collections of overloaded methods associated to the same message, whose selection takes place dynamically instead statically as in standard overloading) are a useful mechanism since they unleash power dynamic binding object-oriented languages, so enhancing re-usability and separation responsibilities. However, many mainstream such as, e.g., Java, do not provide it, resorting only static overloading.

Goals of flexibility and re-usability in typed object-oriented languages suggest the requirement double dispatch, i.e., mechanism dynamically selecting a method not only according to run-time type receiver (single dispatch), but also argument. However, many mainstream languages, such as, e.g., C++ Java, do provide it, resorting single dispatch. In this paper we present general technique for adding dispatch as type-safe language feature, so yielding dynamic overloading covariant...