Abstract Distributed runtime verification (DRV) addresses the problem of checking the correctness of distributed systems during execution, coping with partial knowledge, dynamic topologies, and the absence of global time. These challenges are particularly prominent in proximity-based networks, such as those arising in IoT and Far Edge computing scenarios, where large numbers of devices interact through local communication. This tutorial presents an approach to DRV based on Aggregate Programming (AP), a paradigm for designing distributed collective systems via high-level abstractions over computational fields. We show how temporal and spatial properties (expressed in past-CTL and SLCS, respectively) can be systematically compiled into aggregate monitors grounded in the eXchange Calculus and executed using the FCPP C++ framework and simulator for AP. The tutorial combines conceptual foundations with practical guidance: participants learn how to specify spatio-temporal properties, generate corresponding monitors, and execute them in a 3D simulation environment. Examples are drawn from ongoing industrial collaborations and research projects, which we use to illustrate realistic monitoring scenarios and motivate open challenges for AP-based DRV.

Abstract Developing large-scale collective adaptive systems for safety-critical applications requires an extensive effort, involving the interplay of distributed programming techniques and mathematical proofs of real-time guarantees. This effort could be significantly reduced by allowing the system developer to rely on libraries of predefined algorithms. By exploiting such algorithms, distributed behaviour and (hard) real-time guarantees for the final application could be automatically inferred, effectively shifting the verification burden from the system designer to the algorithm developer. Following earlier work on real-time guarantees for aggregate computing algorithms, we argue that aggregate computing could provide a convenient framework towards this aim. As a first step, we give a detailed description of different kinds of models that can interpret corresponding classes of aggregate programs as mathematical functions. Then, building on such models, we investigate the problem of how real-time behaviour constraints can be specified in a compositional way, proposing a few composable specification patterns, and singling out a number of potential building block library algorithms that could constitute such a real-time aggregate computing library. We evaluate our proposal by means of examples, describing a series of example algorithms for each proposed model, and by investigating two possible compositions of some of them in an archetypal scenario of distributed estimation of the network diameter. In these two examples, we experimentally prove the effectiveness of the models by comparing the results of the interpretation with the simulations results, achieving a close match. Overall, the proposed framework provides a roadmap towards a real-time aggregate computing library with the potential of providing a valuable asset for supporting the rigorous engineering of safety-critical large-scale collective adaptive systems.

Improved autonomy in robotic systems is needed for innovation in, e.g., the marine sector. Autonomous robots that are let loose in hazardous environments, such as underwater, need to handle uncertainties that stem from both their environment and internal state. While self-adaptation is crucial to cope with these uncertainties, bad decisions may cause the robot to get lost or even to cause severe environmental damage. Autonomous, self-adaptive robots that operate in uncontrolled environments full of uncertainties need to be reliable! Since these uncertainties are hard to replicate in test deployments, we need methods to formally analyse self-adaptive robots operating in uncontrolled environments. In this article, we show how feature-oriented techniques can be used to formally model and analyse self-adaptive robotic systems in the presence of such uncertainties. Self-adaptive systems can be organised as two-layered systems with a managed subsystem handling the domain concerns and a managing subsystem implementing the adaptation logic. We consider a case study of an Autonomous Underwater Vehicle (AUV) for pipeline inspection, in which the managed subsystem of the AUV is modelled as a family of systems, where each family member corresponds to a valid configuration of the AUV which can be seen as an operating mode of the AUV’s behaviour. The managing subsystem of the AUV is modelled as a control layer that is capable of dynamically switching between such valid configurations, depending on both environmental and internal uncertainties. These uncertainties are captured in a probabilistic and highly configurable model. Our modelling approach allows us to exploit powerful formal methods for feature-oriented systems, which we illustrate by analysing safety properties, energy consumption, and multi-objective properties, as well as performing parameter synthesis to analyse to what extent environmental conditions affect the AUV. The case study is realised in the probabilistic feature-oriented modelling language and verification tool ProFeat, and in particular exploits family-based probabilistic and parametric model checking.

Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems (SASs) can be realised as two-layered systems, introducing a separation of concerns between the domain-specific functionalities of the system (the managed subsystem) and the adaptation logic (the managing subsystem), i.e., introducing an external feedback loop for managing adaptation in the system. We present an approach to model SASs as dynamic software product lines (SPLs) and leverage existing approaches to SPL-based analysis for the analysis of SASs. To do so, the functionalities of the SAS are modelled in a feature model, capturing the SAS’s variability. This allows us to model the managed subsystem of the SAS as a family of systems, where each family member corresponds to a valid feature configuration of the SAS. Thus, the managed subsystem of an SAS is modelled as an SPL model; more precisely, a probabilistic featured transition system. The managing subsystem of an SAS is modelled as a control layer capable of dynamically switching between these valid configurations, depending on both environmental and internal conditions. We demonstrate the approach on a small-scale evaluation of a self-adaptive autonomous underwater vehicle used for pipeline inspection, which we model and analyse with the feature-aware probabilistic model checker ProFeat. The approach allows us to analyse probabilistic reward and safety properties for the SAS, as well as the correctness of its adaptation logic. • Dynamic software product lines used to model self-adaptive systems. • Family-based analysis used for formal verification of self-adaptive systems. • A case study from the underwater robotics domain to exemplify the approach. • Maintaining separation of concerns between the two layers of a self-adaptive system.

Recent trends like the Internet of Things (IoT) suggest a vision of dense and multi-scale deployments of computing devices in nearly all kinds of environments. A prominent engineering challenge revolves around programming the collective adaptive behaviour of such computational ecosystems. This requires abstractions able to capture concepts like ensembles (dynamic groups of cooperating devices) and collective tasks (joint activities carried out by ensembles). In this work, we consider collections of devices interacting with neighbours and that execute in nearly-synchronised sense-compute-interact rounds, where the computation is given by a single program mapping sensing values and incoming messages to output and outcoming messages. To support programming whole computational collectives, we propose the abstraction of a distributed collective process, which can be used to define at once the ensemble formation logic and its collective task. We formalise the abstraction in the eXchange Calculus (XC), a core functional language based on neighbouring values (maps from neighbours to values) where state and interaction is handled through a single primitive, exchange, and provide a corresponding implementation in the FCPP language. Then, we exercise distributed collective processes using two case studies: multi-hop message propagation and distributed monitoring of spatial properties. Finally, we discuss the features of the abstraction and its suitability for different kinds of distributed computing applications.

Self-adaptation, meant to increase reliability, is a crucial feature of cyber-physical systems operating in uncertain physical environments. Ensuring safety properties of self-adaptive systems is of utter importance, especially when operating in remote environments where communication with a human operator is limited, like under water or in space. This paper presents a software model that allows the analysis of one such self-adaptive system, a configurable underwater robot used for pipeline inspection, by means of the probabilistic model checker ProFeat. Furthermore, it shows that the configurable software model is easily extensible to further, possibly more complex use cases and analyses.

Today’s distributed and pervasive computing addresses large-scale cyber-physical ecosystems, characterised by dense and large networks of devices capable of computation, communication and interaction with the environment and people. While most research focuses on treating these systems as ‘composites’ (i.e., heterogeneous functional complexes), recent developments in fields such as self-organising systems and swarm robotics have opened up a complementary perspective: treating systems as ‘collectives’ (i.e., uniform, collaborative and self-organising groups of entities). This article explores the motivations, state of the art and implications of this ‘collective computing paradigm’ in software engineering. In particular, it discusses its peculiar challenges, implied by characteristics like distribution, situatedness, large scale and cooperative nature. These challenges outline significant directions for future research in software engineering, touching on aspects such as macro-programming, collective intelligence, self-adaptive middleware, learning/synthesis of collective behaviour, human involvement, safety and security in collective cyber-physical ecosystems.

Distributed collective systems are systems formed by homogeneous dynamic collections of devices acting in a shared environment to pursue a joint task or goal. Typical applications emerge in the context of wireless sensor networks, robot swarms, groups of wearable-augmented people, and computing infrastructures. Programming such systems is notoriously hard, due to requirements of scalability, concurrency, faults, and difficulty in making desired collective behaviour ultimately emerge: ad-hoc languages and mechanisms have been proposed threads like spatial computing, macro-programming, and field-based coordination. In this paper we present the eXchange Calculus (XC), formalising a tiny set of key mechanisms, usable across many different languages and platforms, allowing to express the overall interactive behaviour of distributed collective systems in a declarative way. In this approach, computation (executed in asynchronous rounds), communication (which is neighbour-based), and state over time, are all expressed by a single declarative construct, called exchange. We provide a formalisation of XC in terms of syntax, device-level and network-level semantics, prove a number of properties of the calculus, and discuss applicability considering a smart city scenario. XC is implemented as a DSL in Scala and in C＋＋, with different trade-offs in terms of productivity and platform targetting.

Data-centric parallel programming models such as dataflows are well established to implement complex concurrent software. However, in a context of a configurable software, the dataflow used in its computation might vary with respect to the selected options: this happens in particular in fields such as Computational Fluid Dynamics (CFD), where the shape of the domain in which the fluid flows and the equations used to simulate the flow are all options configuring the dataflow to execute. In this paper, we present an approach to implement product lines of dataflows, based on Delta-Oriented Programming (DOP) and term rewriting. This approach includes several analyses to check that all dataflows of a product line can be generated. Moreover, we discuss a prototype implementation of the approach and demonstrate its feasibility in practice.

A Software Product Line (SPL) is a family of similar programs, called variants, generated from a common artifact base. A Multi SPL (MPL) is a set of interdependent SPLs: each variant can depend on variants from other SPLs. MPLs are challenging to model and to implement efficiently, especially when different variants of the same SPL must coexist and interoperate. We address this challenge by introducing the concept of a variability module (VM), a new language construct. A VM constitutes at the same time a module and an SPL of standard (variability-free), possibly interdependent, modules. Generating a variant of a VM triggers the generation of all variants required to satisfy its dependencies. Consequentially, a set of interdependent VMs represents an MPL that can be compiled into a set of standard modules. We illustrate the VM concept with an example from an industrial modeling scenario and formalize it in a core calculus. We define family-based analyses to check that a VM satisfies certain well-formedness conditions and whether all variants can be generated. Finally, we provide an implementation of VM for the Java-like modeling language ABS, and evaluate it with case studies.

Cloud computing has radically changed the way organizations operate their Software by allowing them to achieve high availability of services at affordable cost. Containerized microservices is an enabling technology for this change, and advanced container orchestration platforms such as Kubernetes are used for service management. Despite the flourishing ecosystem of monitoring tools for such orchestration platforms, service management is still mainly a manual effort. The modeling of cloud computing systems is an essential step towards automatic management, but the modeling of cloud systems of such complexity remains challenging and, as yet, unaddressed. In fact modeling resource consumption will be a key to comparing the outcome of possible deployment scenarios. This paper considers how to derive resource models for cloud systems empirically. We do so based on models of deployed services in a formal modeling language with explicit CPU and memory resources; once the adherence to the real system is good enough, formal properties can be verified in the model. Targeting a likely microservices application, we present a model of Kubernetes developed in Real-Time ABS. We report on leveraging data collected empirically from small deployments to simulate the execution of higher intensity scenarios on larger deployments. We discuss the challenges and limitations that arise from this approach, and identify constraints under which we obtain satisfactory accuracy.

Recent works in contexts like the Internet of Things (IoT) and large-scale Cyber-Physical Systems (CPS) propose the idea of programming distributed systems by focussing on their global behaviour across space and time. In this view, a potentially vast and heterogeneous set of devices is considered as an "aggregate" to be programmed as a whole, while abstracting away the details of individual behaviour and exchange of messages, which are expressed declaratively. One such a paradigm, known as aggregate programming, builds on computational models inspired by field-based coordination. Existing models such as the field calculus capture interaction with neighbours by a so-called "neighbouring field" (a map from neighbours to values). This requires ad-hoc mechanisms to smoothly compose with standard values, thus complicating programming and introducing clutter in aggregate programs, libraries and domain-specific languages (DSLs). To address this key issue we introduce the novel notion of "computation against a neighbour", whereby the evaluation of certain subexpressions of the aggregate program are affected by recent corresponding evaluations in neighbours. We capture this notion in the neighbours calculus (NC), a new field calculus variant which is shown to smoothly support declarative specification of interaction with neighbours, and correspondingly facilitate the embedding of field computations as internal DSLs in common general-purpose programming languages -- as exemplified by a Scala implementation, called ScaFi. This paper formalises NC, thoroughly compares it with respect to the classic field calculus, and shows its expressiveness by means of a case study in edge computing, developed in ScaFi.

Abstract A Featured Transition System (FTS) models the behaviour of all products of a Software Product Line (SPL) in a single compact structure, by associating action-labelled transitions with features that condition their presence in product behaviour. It may however be the case that the resulting featured transitions of an FTS cannot be executed in any product (so called dead transitions) or, on the contrary, can be executed in all products (so called false optional transitions). Moreover, an FTS may contain states from which a transition can be executed only in some products (so called hidden deadlock states). It is useful to detect such ambiguities and signal them to the modeller, because dead transitions indicate an anomaly in the FTS that must be corrected, false optional transitions indicate a redundancy that may be removed, and hidden deadlocks should be made explicit in the FTS to improve the understanding of the model and to enable efficient verification—if the deadlocks in the products should not be remedied in the first place. We provide an algorithm to analyse an FTS for ambiguities and a means to transform an ambiguous FTS into an unambiguous one. The scope is twofold: an ambiguous model is typically undesired as it gives an unclear idea of the SPL and, moreover, an unambiguous FTS can efficiently be model checked. We empirically show the suitability of the algorithm by applying it to a number of benchmark SPL examples from the literature, and we show how this facilitates a kind of family-based model checking of a wide range of properties on FTSs.

Highly-configurable software systems can have thousands of interdependent configuration options across different subsystems. In the resulting configuration space, discovering a valid product configuration for some selected options can be complex and error prone. The configuration space can be organized using a feature model, fragmented into smaller interdependent feature models reflecting the configuration options of each subsystem.

The complexity of large-scale distributed systems, particularly when deployed in physical space, calls for new mechanisms to address composability and reusability of collective adaptive behaviour. Computational fields have been proposed as an effective abstraction to fill the gap between the macro-level of such systems (specifying a system’s collective behaviour) and the micro-level (individual devices’ actions of computation and interaction to implement that collective specification), thereby providing a basis to better facilitate the engineering of collective APIs and complex systems at higher levels of abstraction. This article proposes a full formal foundation for field computations, in terms of a core (higher-order) calculus of computational fields containing a few key syntactic constructs, and equipped with typing, denotational and operational semantics. Critically, this allows formal establishment of a link between the micro- and macro-levels of collective adaptive systems by a result of computational adequacy and abstraction for the (aggregate) denotational semantics with respect to the (per-device) operational semantics.

As the density of sensing/computation/actuation nodes is increasing, it becomes more and more feasible and useful to think at an entire network of physical devices as a single, continuous space-time computing machine. The emergent behaviour of the whole software system is then induced by local computations deployed within each node and by the dynamics of the information diffusion. A relevant example of this distribution model is given by aggregate computing and its companion language field calculus, a minimal set of purely functional constructs used to manipulate distributed data structures evolving over space and time, and resulting in robustness to changes. In this paper, we study the convergence time of an archetypal and widely used component of distributed computations expressed in field calculus, called gradient: a fully-distributed estimation of distances over a metric space by a spanning tree. We provide an analytic result linking the quality of the output of a gradient to the amount of computing resources dedicated. The resulting error bounds are then exploited for network design, suggesting an optimal density value taking broadcast interferences into account. Finally, an empirical evaluation is performed validating the theoretical results.

Software Product Lines are an established mechanism to describe multiple variants of one software product. Current approaches however, do not offer a mechanism to support the use of multiple variants from one product line in the same application. We experienced the need for such a mechanism in an industry project with German Railways where we do not merely model a highly variable system, but a system with highly variable subsystems. We present the design challenges that arise when software product lines have to support the use of multiple variants in the same application, in particular: How to reference multiple variants, how to manage multiple variants to avoid name clashes, and how to keep multiple variants interoperable.

A key problem when coordinating the behaviour of spatially situated networks, like those typically found in the Internet of Things (IoT), is adaptation to changes impacting network topology, density, and heterogeneity. Computational goals for such systems, however, are often dependent on geometric properties of the continuous environment in which the devices are situated rather than the particulars of how devices happen to be distributed through it. In this article, we identify a new property of distributed algorithms, eventual consistency , which guarantees that computation converges to a final state that approximates a predictable limit, based on the continuous environment, as the density and speed of devices increases. We then identify a large class of programs that are eventually consistent, building on prior results on the field calculus computational model (Beal et al. 2015; Viroli et al. 2015a) that identify a class of self-stabilizing programs. Finally, we confirm through simulation of IoT application scenarios that eventually consistent programs from this class can provide resilient behavior where programs that are only converging fail badly.

A number of recent works have investigated the notion of “computational fields” as a means of coordinating systems in distributed, dense and dynamic environments such as pervasive computing, sensor networks, and robot swarms. We introduce a minimal core calculus meant to capture the key ingredients of languages that make use of computational fields: functional composition of fields, functions over fields, evolution of fields over time, construction of fields of values from neighbours, and restriction of a field computation to a sub-region of the network. We formalise a notion of type soundness for the calculus that encompasses the concept of domain alignment, and present a sound static type inference system. This calculus and its type inference system can act as a core for actual implementation of coordination languages and models, as well as to pave the way towards formal analysis of properties concerning expressiveness, self-stabilisation, topology independence, and relationships with the continuous space–time semantics of spatial computations.

Modern software systems outgrow the scope of traditional software product lines (SPLs) resulting in multi software product lines (MSPLs) with many interconnected subsystem versions and variants. Delta-oriented programming (DOP) is a flexible, modular approach for implementing SPLs, but DOP so far does not allow the realization of MSPLs. In this paper, we extend DOP to support MSPL development and provide the first holistic modeling approach for MSPLs that spans problem, solution and configuration space. The main concept is the extension of DOP with the possibility to import other SPLs or MSPLs into a new MSPL. By expressing constraints amongst the imported SPLs, a common configuration and product generation is enabled.

Abstract Traits have been proposed as a more flexible mechanism than class inheritance for structuring code in object-oriented programming, to achieve fine-grained code reuse. A trait originally developed for one purpose can be adapted and reused in a completely different context. Formalizations of traits have been extensively studied, and implementations of traits have started to appear in programming languages. So far, work on formally establishing properties of trait-based programs has mostly concentrated on type systems. This paper presents the first deductive proof system for a trait-based object-oriented language. If a specification of a trait can be given a priori, covering all actual usage of that trait, our proof system is modular as each trait is analyzed only once. However, imposing such a restriction may in many cases unnecessarily limit traits as a mechanism for flexible code reuse. In order to reflect the flexible reuse potential of traits, our proof system additionally allows new specifications to be added to a trait in anincrementalway which does not violate established proofs. We formalize and show the soundness of the proof system.

Delta-oriented programming (DOP) is a flexible approach for implementing software product lines (SPLs). DOP SPLs are implemented by a code base (a set of delta modules encapsulating changes to object-oriented programs) and a product line declaration (providing the connection of the delta modules with the product features). In this paper, we extend DOP by the capability to switch the implemented product configuration at runtime and present a formal foundation for dynamic DOP. A dynamic DOP SPL is a DOP SPL with a dynamic reconfiguration graph that specifies how to switch between different feature configurations. Dynamic DOP supports (unanticipated) software evolution such that at runtime, the product line declaration, the code base and the dynamic reconfiguration graph can be changed in any (unanticipated) way that preserves the currently running product. The type system of our dynamic DOP core calculus ensures that the dynamic reconfigurations lead to type safe products and do not cause runtime type errors.

Delta-oriented programming is a modular, yet flexible technique to implement software product lines. To efficiently verify the specifications of all possible product variants of a product line, it is usually infeasible to generate all product variants and to verify them individually. To counter this problem, we propose a transformational proof system in which the specifications in a delta module describe changes to previous specifications. Our approach allows each delta module to be verified in isolation, based on symbolic assumptions for calls to methods which may be in other delta modules. When product variants are generated from delta modules, these assumptions are instantiated by the actual guarantees of the methods in the considered product variant and used to derive the specifications of this product variant.

Traits have been proposed as a more flexible mechanism for code structuring in object-oriented programming than class inheritance, for achieving fine-grained code reuse. A trait originally developed for one purpose can be modified and reused in a completely different context. Formalizations of traits have been extensively studied, and implementations of traits have started to appear in programming languages. However, work on formally establishing properties of trait-based programs has so far mostly concentrated on type systems. This paper proposes the first deductive proof system for a trait-based object-oriented language. If a specification for a trait can be given a priori, covering all actual usage of that trait, our proof system is modular as each trait is analyzed only once. In order to reflect the flexible reuse potential of traits, our proof system additionally allows new specifications to be added to a trait in an incremental way which does not violate established proofs. We formalize and show the soundness of the proof system.

The stochastic simulation of biological systems is an increasingly popular technique in bioinformatics. It often is an enlightening technique, which may however result in being computational expensive. We discuss the main opportunities to speed it up on multi-core platforms, which pose new challenges for parallelisation techniques. These opportunities are developed in two general families of solutions involving both the single simulation and a bulk of independent simulations (either replicas of derived from parameter sweep). Proposed solutions are tested on the parallelisation of the CWC simulator (Calculus of Wrapped Compartments) that is carried out according to proposed solutions by way of the Fast Flow programming framework making possible fast development and efficient execution on multi-cores.

Dynamic trait replacement is a programming language feature for changing the objects' behavior at runtime by replacing some of the objects' methods. In previous work on dynamic trait replacement for JAVA-like languages, the object's methods that may be replaced must correspond exactly to a named trait used in the object's class definition. In this paper we propose the notion of replaceable: a programming language feature that decouples trait replacement operation code and class declaration code, thus making it possible refactoring classes and/or performing unanticipated trait replacement operations without invalidating existing code.

We present a translation from Fickle , a small object-oriented language allowing objects to change their class at runtime, into Java. The translation is provenly correct in the sense that it preserves the static and dynamic semantics. Moreover, it is compatible with separate compilation, since the translation of a Fickle class does not depend on the implementation of used classes. Based on the formal system, we have developed an implementation. The translation turned out to be a more subtle problem than we expected. In this article, we discuss four possible approaches we considered for the design of the translation and to justify our choice, we present formally the translation and proof of preservation of the static and dynamic semantics, and discuss the prototype implementation. Moreover, we outline an alternative translation based on generics that avoids most of the casts (but not all) needed in the previous translation. The language Fickle has undergone and is still undergoing several phases of development. In this article we are discussing the translation of Fickle II .

We define compositional compilation as the ability to typecheck source code fragments in isolation, generate We define compositional compilation as the ability to typecheck source code fragments in isolation, generate corresponding binaries,and link together fragments whose mutual assumptions are satisfied, without reinspecting the code. Even though compositional compilation is a highly desirable feature, in Java-like languages it can hardly be achieved. This is due to the fact that the bytecode generated for a fragment (say, a class) is not uniquely determined by its source code, but also depends on the compilation context.We propose a way to obtain compositional compilation for Java, by introducing a polymorphic form of bytecode containing type variables (ranging over class names) and equipped with a set of constraints involving type variables. Thus, polymorphic bytecode provides a representation for all the (standard) bytecode that can be obtained by replacing type variables with classes satisfying the associated constraints.We illustrate our proposal by developing a typing and a linking algorithm. The typing algorithm compiles a class in isolation generating the corresponding polymorphic bytecode fragment and constraints on the classes it depends on. The linking algorithm takes a collection of polymorphic bytecode fragments, checks their mutual consistency, and possibly simplifies and specializes them. In particular, linking a self-contained collection of fragments either fails, or produces standard bytecode (the same as would have been produced by standard compilation of all fragments).

We propose a rank 2 intersection type system for a language of modules built on a core ML-like language. The principal typing property of the rank 2 intersection type system for the core language plays a crucial role in the design of the type system for the module language. We first consider a "plain" notion of module, where a module is just a set of mutually recursive top-level definitions, and illustrate the notions of: module intrachecking (each module is typechecked in isolation and its interface, which is the set of typings of the defined identifiers, is inferred); interface interchecking (when linking modules, typechecking is done just by looking at the interfaces); interface specialization (interface intrachecking may require to specialize the typing listed in the interfaces); principal interfaces (the principal typing property for the type system of modules); and separate typechecking (looking at the code of the modules does not provide more type information than looking at their interfaces). Then we illustrate some limitations of the "plain" framework and extend the module language and the type system in order to overcome these limitations. The decidability of the system is shown by providing algorithms for the fundamental operations involved in module intrachecking and interface interchecking.

We investigate the use of conjunctive non-standard type inference for the elimination of useless code in higher-order typed functional programs. In particular, we present a non-standard type assignment system for detecting useless code together with a mapping that simplifies a program by removing the useless code detected using the system.

We propose a rank 2 intersection type system with new typing rules for local definitions (let-expressions and letrec-expressions) and conditional expressions (if-expressions and match-expressions). This is a further step towards the use of intersection types in "real" programming languages.The technique for typing local definitions relies entirely on the principal typing property (i.e. it does not depend on particulars of rank 2 intersection), so it can be applied to any system with principal typings. The technique for typing conditional expressions, which is based on the idea of introducing metrics on types to "limit the use" of the intersection type constructor in the types assigned to the branches of the conditionals, is instead tailored to rank 2 intersection. However, the underlying idea might also be useful for other type systems.

Reclassification changes the class membership of an object at run-time while retaining its identity. We suggest language features for object reclassification, which extend an imperative, typed, class-based, object-oriented language.We present our proposal through the language Fickle ⋄⋄ . The imperative features, combined with the requirement for a static and safe type system, provided the main challenges. We develop a type and effect system for Fickle ⋄⋄ and prove its soundness with respect to the operational semantics. In particular, even though objects may be reclassified across classes with different members, there will never be an attempt to access nonexisting members.

In this paper we present two type inference systems for detecting useless-code in higher-order typed functional programs. Type inference can be performed in an efficient and complete way, by reducing it to the solution of a system of constraints. We also give a useless-code elimination algorithm which is based on a combined use of these type inference systems. The main application of the technique is the optimization of programs extracted from proofs in logical frameworks, but it could be used as well in the elimination of useless-code determined by program transformations.