Search

This paper deals with retraction - intended as isomorphic embedding - in intersection types building left and right inverses as terms of a lambda calculus with a bottom constant. The main result is a necessary and sufficient condition two strict intersection types must satisfy in order to assure the existence of two terms showing the first type to be a retract of the second one. Moreover, the characterisation of retraction in the standard intersection types is discussed., Comment: In Proceedings ITRS 2016, arXiv:1702.01874

The paper presents a data-driven model of self-adaptivity for multiparty sessions. System choreography is prescribed by a global type. Participants are incarnated by processes associated with monitors, which control their behaviour. Each participant can access and modify a set of global data, which are able to trigger adaptations in the presence of critical changes of values. The use of the parallel composition for building global types, monitors and processes enables a significant degree of flexibility: an adaptation step can dynamically reconfigure a set of participants only, without altering the remaining participants, even if the two groups communicate., Comment: In Proceedings PLACES 2016, arXiv:1606.05403

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 right type. The present paper faces the problem of type isomorphism in a system with intersection and union types. In the presence of intersection and union, isomorphism is not a congruence and cannot be characterised in an equational way. A characterisation can still be given, quite complicated by the interference between functional and non functional types. This drawback is faced in the paper by interpreting each atomic type as the set of functions mapping any argument into the interpretation of the type itself. This choice has been suggested by the initial projection of Scott's inverse limit lambda-model. The main result of this paper is a condition assuring type isomorphism, based on an isomorphism preserving reduction., Comment: In Proceedings ITRS 2014, arXiv:1503.04377

Within the framework of a global French program oriented towards the development of renewable energies, Martinique Island (Lesser Antilles, France) has been extensively investigated (from 2012 to 2013) through an integrated multi-methods approach, with the aim to define precisely the potential geothermal ressources, previously highlighted (Sanjuan et al., 2003). Amongst the common investigation methods deployed, we carried out three magnetotelluric (MT) surveys located above three of the most promising geothermal fields of Martinique, namely the Anses d'Arlet, the Montagne Pel{\'e}e and the Pitons du Carbet prospects. A total of about 100 MT stations were acquired showing single or multi-dimensional behaviors and static shift effects. After processing data with remote reference, 3-D MT inversions of the four complex elements of MT impedance tensor without pre-static-shift correction, have been performed for each sector, providing three 3-D resistivity models down to about 12 to 30 km depth. The sea coast effect has been taken into account in the 3-D inversion through generation of a 3-D resistivity model including the bathymetry around Martinique from the coast up to a distance of 200 km. The forward response of the model is used to calculate coast effect coefficients that are applied to the calculated MT response during the 3-D inversion process for comparison with the observed data. 3-D resistivity models of each sector, which are inherited from different geological history, show 3-D resistivity distribution and specificities related to its volcanological history. In particular, the geothermal field related to the Montagne Pel{\'e}e strato-volcano, is characterized by a quasi ubiquitous conductive layer and quite monotonic typical resistivity distribution making interpretation difficult in terms of geothermal targets. At the opposite, the resistivity distribution of Anse d'Arlet area is radically different and geothermal target is thought to be connected to a not so deep resistive intrusion elongated along a main structural axis. Beside these interesting deep structures, we demonstrate, after analyzing the results of the recent heliborne TEM survey covering the whole Martinique, that surface resistivity distribution obtained from 3-D inversion reproduce faithfully the resistivity distribution observed by TEM. In spite of a very different sampling scale, this comparison illustrates the ability of 3-D MT inversion to take into account and reproduce static shift effects in the sub-surface resistivity distribution., Comment: Wordl Geothermal Congress 2015, Apr 2015, Melbourne, Australia

This paper investigates type isomorphism in a lambda-calculus with intersection and union types. It is known that in lambda-calculus, the isomorphism between two types is realised by a pair of terms inverse one each other. Notably, invertible terms are linear terms of a particular shape, called finite hereditary permutators. Typing properties of finite hereditary permutators are then studied in a relevant type inference system with intersection and union types for linear terms. In particular, an isomorphism preserving reduction between types is defined. Type reduction is confluent and terminating, and induces a notion of normal form of types. The properties of normal types are a crucial step toward the complete characterisation of type isomorphism. 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, the characterisation of the isomorphism between types in normal form, modulo isomorphism of arrow types., Comment: In Proceedings ITRS 2012, arXiv:1307.7849

Arbuscular mycorrhiza (AM) is the most wide-spread plant-fungus symbiosis on earth. Investigating this kind of symbiosis is considered one of the most promising ways to develop methods to nurture plants in more natural manners, avoiding the complex chemical productions used nowadays to produce artificial fertilizers. In previous work we used the Calculus of Wrapped Compartments (CWC) to investigate different phases of the AM symbiosis. In this paper, we continue this line of research by modelling the colonisation of the plant root cells by the fungal hyphae spreading in the soil. This study requires the description of some spatial interaction. Although CWC has no explicit feature modelling a spatial geometry, the compartment labelling feature can be effectively exploited to define a discrete surface topology outlining the relevant sectors which determine the spatial properties of the system under consideration. Different situations and interesting spatial properties can be modelled and analysed in such a lightweight framework (which has not an explicit notion of geometry with coordinates and spatial metrics), thus exploiting the existing CWC simulation tool., Comment: In Proceedings CompMod 2011, arXiv:1109.1044

The Calculus of Wrapped Compartments (CWC) is a recently proposed modelling language for the representation and simulation of biological systems behaviour. Although CWC has no explicit structure modelling a spatial geometry, its compartment labelling feature can be exploited to model various examples of spatial interactions in a natural way. However, specifying large networks of compartments may require a long modelling phase. In this work we present a surface language for CWC that provides basic constructs for modelling spatial interactions. These constructs can be compiled away to obtain a standard CWC model, thus exploiting the existing CWC simulation tool. A case study concerning the modelling of Arbuscular Mychorrizal fungi growth is discussed., Comment: Presented at MeCBIC 2011

The modelling and analysis of biological systems has deep roots in Mathematics, specifically in the field of ordinary differential equations (ODEs). Alternative approaches based on formal calculi, often derived from process algebras or term rewriting systems, provide a quite complementary way to analyze the behaviour of biological systems. These calculi allow to cope in a natural way with notions like compartments and membranes, which are not easy (sometimes impossible) to handle with purely numerical approaches, and are often based on stochastic simulation methods. Recently, it has also become evident that stochastic effects in regulatory networks play a crucial role in the analysis of such systems. Actually, in many situations it is necessary to use stochastic models. For example when the system to be described is based on the interaction of few molecules, when we are at the presence of a chemical instability, or when we want to simulate the functioning of a pool of entities whose compartmentalised structure evolves dynamically. In contrast, stable metabolic networks, involving a large number of reagents, for which the computational cost of a stochastic simulation becomes an insurmountable obstacle, are efficiently modelled with ODEs. In this paper we define a hybrid simulation method, combining the stochastic approach with ODEs, for systems described in CWC, a calculus on which we can express the compartmentalisation of a biological system whose evolution is defined by a set of rewrite rules., Comment: In Proceedings MeCBIC 2010, arXiv:1011.0051

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 FastFlow programming framework making possible fast development and efficient execution on multi-cores., Comment: 19 pages + cover page

The Calculus of Wrapped Compartments (CWC) is a variant of the Calculus of Looping Sequences (CLS). While keeping the same expressiveness, CWC strongly simplifies the development of automatic tools for the analysis of biological systems. The main simplification consists in the removal of the sequencing operator, thus lightening the formal treatment of the patterns to be matched in a term (whose complexity in CLS is strongly affected by the variables matching in the sequences). We define a stochastic semantics for this new calculus. As an application we model the interaction between macrophages and apoptotic neutrophils and a mechanism of gene regulation in E.Coli.

The Stochastic Calculus of Looping Sequences (SCLS) is a recently proposed modelling language for the representation and simulation of biological systems behaviour. It has been designed with the aim of combining the simplicity of notation of rewrite systems with the advantage of compositionality. It also allows a rather simple and accurate description of biological membranes and their interactions with the environment. In this work we apply SCLS to model a newly discovered ammonium transporter. This transporter is believed to play a fundamental role for plant mineral acquisition, which takes place in the arbuscular mycorrhiza, the most wide-spread plant-fungus symbiosis on earth. Due to its potential application in agriculture this kind of symbiosis is one of the main focuses of the BioBITs project. In our experiments the passage of NH3 / NH4+ from the fungus to the plant has been dissected in known and hypothetical mechanisms; with the model so far we have been able to simulate the behaviour of the system under different conditions. Our simulations confirmed some of the latest experimental results about the LjAMT2;2 transporter. The initial simulation results of the modelling of the symbiosis process are promising and indicate new directions for biological investigations.