A core calculus for the analysis and implementation of biologically inspired languages

The application of Concurrency Theory to Systems Biology is in its earliest stage of progress. The metaphor of cells as computing systems by Regev and Shapiro opened the employment of concurrent languages for the modelling of biological systems. Their peculiar characteristics led to the design of many bio-inspired formalisms which achieve higher faithfulness and specificity. In this thesis we present pi@, an extremely simple and conservative extension of the pi-calculus representing a keystone in this respect, thanks to its expressiveness capabilities. The pi@ calculus is obtained by the addition of polyadic synchronisation and priority to the pi-calculus, in order to achieve compartment semantics and atomicity of complex operations respectively. In its direct application to biological modelling, the stochastic variant of the calculus, Spi@, is shown able to model consistently several phenomena such as formation of molecular complexes, hierarchical subdivision of the system into compartments, inter-compartment reactions, dynamic reorganisation of compartment structure consistent with volume variation. The pivotal role of pi@ is evidenced by its capability of encoding in a compositional way several bio-inspired formalisms, so that it represents the optimal core of a framework for the analysis and implementation of bio-inspired languages. In this respect, the encodings of BioAmbients, Brane Calculi and a variant of P Systems in pi@ are formalised. The conciseness of their translation in pi@ allows their indirect comparison by means of their encodings. Furthermore it provides a ready-to-run implementation of minimal effort whose correctness is granted by the correctness of the respective encoding functions. Further important results of general validity are stated on the expressive power of priority. Several impossibility results are described, which clearly state the superior expressiveness of prioritised languages and the problems arising in the attempt of providing their parallel implementation. To this aim, a new setting in distributed computing (the last man standing problem) is singled out and exploited to prove the impossibility of providing a purely parallel implementation of priority by means of point-to-point or broadcast communication.

On Reasonable Space and Time Cost Models for the λ-Calculus

Slot and van Emde Boas Invariance Thesis states that a time (respectively, space) cost model is reasonable for a computational model C if there are mutual simulations between Turing machines and C such that the overhead is polynomial in time (respectively, linear in space). The rationale is that under the Invariance Thesis, complexity classes such as LOGSPACE, P, PSPACE, become robust, i.e. machine independent. In this dissertation, we want to find out if it possible to define a reasonable space cost model for the lambda-calculus, the paradigmatic model for functional programming languages. We start by considering an unusual evaluation mechanism for the lambda-calculus, based on Girard's Geometry of Interaction, that was conjectured to be the key ingredient to obtain a space reasonable cost model. By a fine complexity analysis of this schema, based on new variants of non-idempotent intersection types, we disprove this conjecture. Then, we change the target of our analysis. We consider a variant over Krivine's abstract machine, a standard evaluation mechanism for the call-by-name lambda-calculus, optimized for space complexity, and implemented without any pointer. A fine analysis of the execution of (a refined version of) the encoding of Turing machines into the lambda-calculus allows us to conclude that the space consumed by this machine is indeed a reasonable space cost model. In particular, for the first time we are able to measure also sub-linear space complexities. Moreover, we transfer this result to the call-by-value case. Finally, we provide also an intersection type system that characterizes compositionally this new reasonable space measure. This is done through a minimal, yet non trivial, modification of the original de Carvalho type system.

Typed behavioural equivalences in the Pi-Calculus

In this thesis, I study the notion of program equivalences, i.e. proving that two programs can be used interchangeably without altering the overall observable behaviour. This definition is highly dependent on the contexts in which these programs can be used; does the context have exceptions, parallelism, etc... So proofs also need to be adapted according to the expressiveness of those contexts. This thesis presents on the pi-calculus – a concurrent programming language – under various typing constraints. Types allows us to impose different disciplines like forcing a sequential execution, or ensuring linearity, meaning an object can be used once. In each case, the bisimulation, a standard proof technique for the pi-calculus, needs to be adapted accordingly to obtain a suitable equivalence. We then test how using the modified bisimulations can be used to reason about a language with higher-order functions and references, which once translated into the pi-calculus satisfies the typing constraints.

Study of the urinary biomarkers of synthetic cannabinoid receptor agonists (SCRAs) for the forensic unequivocal proof of consumption: medico-legal implications for drug abuse prevention

Introduction. Synthetic cannabinoid receptor agonists (SCRAs) represent the widest group of New Psychoactive Substances (NPS) and, around 2021-2022, new compounds emerged on the market. The aims of the present research were to identify suitable urinary markers of Cumyl-CB-MEGACLONE, Cumyl-NB-MEGACLONE, Cumyl-NB-MINACA, 5F-EDMB-PICA, EDMB-PINACA and ADB-HEXINACA, to present data on their prevalence and to adapt the methodology from the University of Freiburg to the University of Bologna. Materials and methods. Human phase-I metabolites detected in 46 authentic urine samples were confirmed in vitro with pooled human liver microsomes (pHLM) assays, analyzed by liquid chromatography-quadrupole time-of-flight mass spectrometry (LC-qToF-MS). Prevalence data were obtained from urines collected for abstinence control programs. The method to study SCRAs metabolism in use at the University of Freiburg was adapted to the local facilities, tested in vitro with 5F-EDMB-PICA and applied to the study of ADB-HEXINACA metabolism. Results. Metabolites built by mono, di- and tri-hydroxylation were recommended as specific urinary biomarkers to monitor the consumption of SCRAs bearing a cumyl moiety. Monohydroxylated and defluorinated metabolites were suitable proof of 5F-EDMB-PICA consumption. Products of monohydroxylation and amide or ester hydrolysis, coupled to monohydroxylation or ketone formation, were recognized as specific markers for EDMB-PINACA and ADB-HEXINACA. The LC-qToF-MS method was successfully adapted to the University of Bologna, as tested with 5F-EDMB-PICA in vitro metabolites. Prevalence data showed that 5F-EDMB-PINACA and EDMB-PINACA were more prevalent than ADB-HEXINACA, but for a limited period. Conclusion. Due to undetectability of parent compounds in urines and to shared metabolites among structurally related compounds, the identification of specific urinary biomarkers as unequivocal proofs of SCRAs consumption remains challenging for forensic laboratories. Urinary biomarkers are necessary to monitor SCRAs abuse and prevalence data could help in establishing tailored strategies to prevent their spreading, highlighting the role for legal medicine as a service to public health.