Search

Multiparty sessions with asynchronous communications and global types play an important role for the modelling of interaction protocols in distributed systems. In designing such calculi the aim is to enforce, by typing, good properties for all participants, maximising, at the same time, the accepted behaviours. Our type system improves the state-of-the-art by typing all asynchronous sessions and preserving the key properties of Subject Reduction, Session Fidelity and Progress when some well-formedness conditions are satisfied. The type system comes together with a sound and complete type inference algorithm. The well-formedness conditions are undecidable, but an algorithm checking an expressive restriction of them recovers the effectiveness of typing.

Traditionally, semantic models of imperative languages use an auxiliary structure which mimics memory. In this way, ownership and other encapsulation properties need to be reconstructed from the graph structure of such global memory. We present an alternative "syntactic" model where memory is encoded as part of the program rather than as a separate resource. This means that execution can be modelled by just rewriting source code terms, as in semantic models for functional programs. Formally, this is achieved by the block construct, introducing local variable declarations, which play the role of memory when their initializing expressions have been evaluated. In this way, we obtain a language semantics which directly represents at the syntactic level constraints on aliasing, allowing simpler reasoning about related properties. To illustrate this advantage, we consider the issue, widely studied in the literature, of characterizing an isolated portion of memory, which cannot be reached through external references. In the syntactic model, closed block values, called "capsules", provide a simple representation of isolated portions of memory, and capsules can be safely moved to another location in the memory, without introducing sharing, by means of "affine' variables. We prove that the syntactic model can be encoded in the conventional one, hence efficiently implemented.

The negative impacts of extreme heat and drought on olive plants have driven the quest for mitigation approaches based on the use of biostimulants, which have proved to be effective in contrasting environmental stresses. The aim of our study was to evaluate the effectiveness of six biostimulants in mitigating high temperature and water stress in young olive trees in terms of vegetative and eco-physiological parameters as well as bioactive compound content. Biostimulants based on glycine betaine and macro- and micro-algae effectively protected the plants from abiotic stress by improving their eco-physiological and vegetative parameters. At the end of the growing season, olive plants were experiencing water deficit which had built up through the summer months. At this time, the glycine betaine-treated plants had a three-fold higher stomatal conductance compared with the control, while plants sprayed with the seaweed mix had a relative water content 33% higher than the control. The kaolin treatment resulted in higher total phenolics and antioxidant activities (DPPH, FRAP and ABTS) in water stress conditions and caused an increase of 238.53 and 443.49% in leaves total polyphenols content in 100% and 50% water regime, respectively. This study showed the effectiveness of biostimulants in mitigating the damage from abiotic stress on young olive trees, by improving some vegetative, eco-physiological and leaf nutraceutical parameters. Further studies are needed to test the efficiency of these biostimulants in open field conditions on olive trees in full production.

Neglected and underutilized species (NUS) offer largely unexplored opportunities for providing nutritious plant food, while making agro-ecosystems more diverse and resilient to climate change. The aim of this work was to explore the potential of two typical Mediterranean underutilized species, purslane and borage, as novel vegetable product (microgreens). Micro-scale production of edible plants is spreading due to the simplicity of their management, rapid cycle, harvest index, and phytochemical value of the edible product. Microgreens, therefore, represent an opportunity to link NUS, nutrition, and agricultural and dietary diversification. By analyzing yield, antioxidants activities, mineral composition, and main phenolic acids and flavonoids, our work indicated that the two species provide interesting results when compared with those reported for crops and horticultural species. Specifically, purslane should be considered highly nutritional due to the amount of phenolic compounds and ascorbic acid, and to potential good β-carotene bioavailability. Borage microgreens have a very high fresh yield and a more composite and balanced phenolic profile. In conclusion, our work provided evidence for implementing new ways to expand the NUS market-chains and for developing added-value food products.

Reversible interactions model different scenarios, like biochemical systems and human as well as automatic negotiations. We abstract interactions via multiparty sessions enriched with named checkpoints. Computations can either go forward or roll back to some checkpoints, where possibly different choices may be taken. In this way communications can be undone and different conversations may be tried. Interactions are typed with global types, which control also rollbacks. Typeability of session participants in agreement with global types ensures session fidelity and progress of reversible communications.

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.

We define BioScapeL, a stochastic pi-calculus in 3D-space. A novel aspect of BioScapeL is that entities have programmable locations. The programmer can specify a particular location where to place an entity, or a location relative to the current location of the entity. The motivation for the extension comes from the need to describe the evolution of populations of biochemical species in space, while keeping a sufficiently high level description, so that phenomena like diffusion, collision, and confinement can remain part of the semantics of the calculus. Combined with the random diffusion movement inherited from BioScape, programmable locations allow us to capture the assemblies of configurations of polymers, oligomers, and complexes such as microtubules or actin filaments. Further new aspects of BioScapeL include random translation and scaling. Random translation is instrumental in describing the location of new entities relative to the old ones. For example, when a cell secretes a hydronium ion, the ion should be placed at a given distance from the originating cell, but in a random direction. Additionally, scaling allows us to capture at a high level events such as division and growth; for example, daughter cells after mitosis have half the size of the mother cell.

We define an extension of the simply-typed lambda calculus where two different binding mechanisms, by position and by name, nicely coexist. In the former, as in standard lambda calculus, the matching between parameter and argument is done on a positional basis, hence alpha-equivalence holds, whereas in the latter it is done on a nominal basis. The two mechanisms also respectively correspond to static binding, where the existence and type compatibility of the argument are checked at compile-time, and dynamic binding, where they are checked at run-time.

BioScape is a concurrent language motivated by the biological landscapes found at the interface of biology and biomaterials. It has been motivated by the need to model antibacterial surfaces, biofilm formation, and the effect of DNAse in treating and preventing biofilm infections. As its predecessor, SPiM, BioScape has a sequential semantics based on Gillespie's algorithm, and its implementation does not scale beyond 1000 agents. However, in order to model larger and more realistic systems, a semantics that may take advantage of the new multi-core and GPU architectures is needed. This motivates the introduction of parallel semantics, which is the contribution of this paper: Parallel BioScape, an extension with fully parallel semantics.

In this paper we present a variant of the Calculus of Looping Sequences (CLS for short) with global and local rewrite rules. While global rules, as in CLS, are applied anywhere in a given term, local rules can only be applied in the compartment on which they are defined. Local rules are dynamic: they can be added, moved and erased. We enrich the new calculus with a parallel semantics where a reduction step is lead by any number of global and local rules that could be performed in parallel. A type system is developed to enforce the property that a compartment must contain only local rules with specific features. As a running example we model some interactions happening in a cell starting from its nucleus and moving towards its mitochondria.

We define a type system with intersection types for an extension of lambda-calculus with unbind and rebind operators. In this calculus, a term with free variables, representing open code, can be packed into an "unbound" term, and passed around as a value. In order to execute inside code, an unbound term should be explicitly rebound at the point where it is used. Unbinding and rebinding are hierarchical, that is, the term can contain arbitrarily nested unbound terms, whose inside code can only be executed after a sequence of rebinds has been applied. Correspondingly, types are decorated with levels, and a term has type decorated with k if it needs k rebinds in order to reduce to a value. With intersection types we model the fact that a term can be used differently in contexts providing different numbers of unbinds. In particular, top-level terms, that is, terms not requiring unbinds to reduce to values, should have a value type, that is, an intersection type where at least one element has level 0. With the proposed intersection type system we get soundness under the call-by-value strategy, an issue which was not resolved by previous type systems.

The calculus of looping sequences is a formalism for describing the evolution of biological systems by means of term rewriting rules. We enrich this calculus with a type discipline to guarantee the soundness of reduction rules with respect to some biological properties deriving from the requirement of certain elements, and the repellency of others. As an example, we model a toy system where the repellency of a certain element is captured by our type system and forbids another element to exit a compartment.

The Stochastic Calculus of Looping Sequences is suitable to describe the evolution of microbiological systems, taking into account the speed of the described activities. We propose a type system for this calculus that models how the presence of positive and negative catalysers can modify these speeds. We claim that types are the right abstraction in order to represent the interaction between elements without specifying exactly the element positions. Our claim is supported through an example modelling the lactose operon.