Formalizing languages for service oriented computing

Service Oriented Computing is a new programming paradigm for addressing distributed system design issues. Services are autonomous computational entities which can be dynamically discovered and composed in order to form more complex systems able to achieve different kinds of task. E-government, e-business and e-science are some examples of the IT areas where Service Oriented Computing will be exploited in the next years. At present, the most credited Service Oriented Computing technology is that of Web Services, whose specifications are enriched day by day by industrial consortia without following a precise and rigorous approach. This PhD thesis aims, on the one hand, at modelling Service Oriented Computing in a formal way in order to precisely define the main concepts it is based upon and, on the other hand, at defining a new approach, called bipolar approach, for addressing system design issues by synergically exploiting choreography and orchestration languages related by means of a mathematical relation called conformance. Choreography allows us to describe systems of services from a global view point whereas orchestration supplies a means for addressing such an issue from a local perspective. In this work we present SOCK, a process algebra based language inspired by the Web Service orchestration language WS-BPEL which catches the essentials of Service Oriented Computing. From the definition of SOCK we will able to define a general model for dealing with Service Oriented Computing where services and systems of services are related to the design of finite state automata and process algebra concurrent systems, respectively. Furthermore, we introduce a formal language for dealing with choreography. Such a language is equipped with a formal semantics and it forms, together with a subset of the SOCK calculus, the bipolar framework. Finally, we present JOLIE which is a Java implentation of a subset of the SOCK calculus and it is part of the bipolar framework we intend to promote.

Indagine sulla nozione di fatto urbano ne L'architettura della città di Aldo Rossi

Questa tesi di dottorato di ricerca ha come oggetto la nozione di fatto urbano elaborata e presentata da Aldo Rossi nel libro L’architettura della città edito nel 1966. Ne L’architettura della città sono molteplici le definizioni e le forme con cui è enunciata la nozione di fatto urbano. Nel corso della tesi si è indagato come la costruzione nel tempo di questo concetto è stata preceduta da diversi studi giovanili intrapresi dal 1953, poi riorganizzati e sintetizzati a partire dal 1963 in un quaderno manoscritto dal titolo “Manuale di urbanistica”, in diversi appunti e in due quaderni manoscritti. Il lavoro di ricerca ha ricostruito la formulazione della nozione di fatto urbano attraverso gli scritti di Rossi. In questa direzione la rilevazione della partecipazione di Rossi a dibattiti, seminari, riviste, corsi universitari o ricerche accademiche è apparsa di fondamentale importanza, per comprendere la complessità di un lavoro non riconducibile a dei concetti disciplinari, ma alla formazione di una teoria trasmissibile. Il tentativo di comprendere e spiegare la nozione di fatto urbano ha condotto ad esaminare l’accezione con cui Rossi compone L’architettura della città, che egli stesso assimila ad un trattato. L’analisi ha identificato come la composizione del libro non è direttamente riferibile ad un uso classico della stesura editoriale del trattato, la quale ha tra i riferimenti più noti nel passato la promozione di una pratica corretta come nel caso vitruviano o un’impalcatura instauratrice di una nuova categoria come nel caso dell’Alberti. La mancanza di un sistema globale e prescrittivo a differenza dei due libri fondativi e il rimando non immediato alla stesura di un trattato classico è evidente ne L’architettura della città. Tuttavia la possibilità di condurre la ricerca su una serie di documenti inediti ha permesso di rilevare come negli scritti a partire dal 1953, sia maturata una trattazione delle questioni centrali alla nozione di fatto urbano ricca di intuizioni, che aspirano ad un’autonomia, sintetizzate, seppure in modo non sistematico, nella stesura del celebre libro. Si è così cercato di mettere in luce la precisazione nel tempo della nozione di fatto urbano e della sua elaborazione nei molteplici scritti antecedenti la pubblicazione de L’architettura della città, precisando come Rossi, pur costruendo su basi teoriche la nozione di fatto urbano, ne indichi una visione progressiva, ossia un uso operativo sulla città. La ricerca si è proposta come obiettivo di comprendere le radici culturali della nozione di fatto urbano sia tramite un’esplorazione degli interessi di Rossi nel suo percorso formativo sia rispetto alla definizione della struttura materiale del fatto urbano che Rossi individua nelle permanenze e che alimenta nella sua definizione con differenti apporti derivanti da altre discipline. Compito di questa ricerca è stato rileggere criticamente il percorso formativo compiuto da Rossi, a partire dal 1953, sottolinearne gli ambiti innovativi e precisarne i limiti descrittivi che non vedranno mai la determinazione di una nozione esatta, ma piuttosto la strutturazione di una sintesi complessa e ricca di riferimenti ad altri studi. In sintesi la tesi si compone di tre parti: 1. la prima parte, dal titolo “La teoria dei fatti urbani ne L’architettura della città”, analizza il concetto di fatto urbano inserendolo all’interno del più generale contesto teorico contenuto nel libro L’architettura della città. Questo avviene tramite la scomposizione del libro, la concatenazione delle sue argomentazioni e la molteplicità delle fonti esplicitamente citate da Rossi. In questo ambito si precisa la struttura del libro attraverso la rilettura dei riferimenti serviti a Rossi per comporre il suo progetto teorico. Inoltre si ripercorre la sua vita attraverso le varie edizioni, le ristampe, le introduzioni e le illustrazioni. Infine si analizza il ruolo del concetto di fatto urbano nel libro rilevando come sia posto in un rapporto paritetico con il titolo del libro, conseguendone un’accezione di «fatto da osservare» assimilabile all’uso proposto dalla geografia urbana francese dei primi del Novecento. 2. la seconda parte, dal titolo “La formazione della nozione di fatto urbano 1953-66”, è dedicata alla presentazione dell’elaborazione teorica negli scritti di Rossi prima de L’architettura della città, ossia dal 1953 al 1966. Questa parte cerca di descrivere le radici culturali di Rossi, le sue collaborazioni e i suoi interessi ripercorrendo la progressiva definizione della concezione di città nel tempo. Si è analizzato il percorso maturato da Rossi e i documenti scritti fin dagli anni in cui era studente alla Facoltà di Architettura Politecnico di Milano. Emerge un quadro complesso in cui i primi saggi, gli articoli e gli appunti testimoniano una ricerca intellettuale tesa alla costruzione di un sapere sullo sfondo del realismo degli anni Cinquanta. Rossi matura infatti un impegno culturale che lo porta dopo la laurea ad affrontare discorsi più generali sulla città. In particolare la sua importante collaborazione con la rivista Casabella-continuità, con il suo direttore Ernesto Nathan Rogers e tutto il gruppo redazionale segnano il periodo successivo in cui compare l’interesse per la letteratura urbanistica, l’arte, la sociologia, la geografia, l’economia e la filosofia. Seguono poi dal 1963 gli anni di lavoro insieme al gruppo diretto da Carlo Aymonino all’Istituto Universitario di Architettura di Venezia, e in particolare le ricerche sulla tipologia edilizia e la morfologia urbana, che portano Rossi a compiere una sintesi analitica per la fondazione di una teoria della città. Dall’indagine si rileva infatti come gli scritti antecedenti L’architettura della città sviluppano lo studio dei fatti urbani fino ad andare a costituire il nucleo teorico di diversi capitoli del libro. Si racconta così la genesi del libro, la cui scrittura si è svolta nell’arco di due anni, e le aspirazioni che hanno portato quello che era stato concepito come un “manuale d’urbanistica” a divenire quello che Rossi definirà “l’abbozzo di un trattato” per la formulazione di una scienza urbana. 3. la terza parte, dal titolo “La struttura materiale dei fatti urbani: la teoria della permanenza”, indaga monograficamente lo studio della città come un fatto materiale, un manufatto, la cui costruzione è avvenuta nel tempo e del tempo mantiene le tracce. Sul tema della teoria della permanenza è stato importante impostare un confronto con il dibattito vivo negli anni della ricostruzione dopo la guerra intorno ai temi delle preesistenze ambientali nella ricostruzione negli ambienti storici. Sono emersi fin da subito importanti la relazione con Ernesto Nathan Rogers, le discussioni sulle pagine di Casabella-Continuità, la partecipazione ad alcuni dibatti e ricerche. Si è inoltre Rilevato l’uso di diversi termini mutuati dalle tesi filosofiche di alcune personalità come Antonio Banfi e Enzo Paci, poi elaborati dal nucleo redazionale di Casabella-Continuità, di cui faceva parte anche Rossi. Sono così emersi alcuni spostamenti di senso e la formulazione di un vocabolario di termini all’interno della complessa vicenda della cultura architettonica degli anni Cinquanta e Sessanta. 1. Si è poi affrontato questo tema analizzando le forme con cui Rossi presenta la definizione della teoria della permanenza e i contributi desunti da alcuni autori per la costruzione scientifica di una teoria dell’architettura, il cui fine è quello di essere trasmissibile e di offrire strumenti di indagine concreti. Questa ricerca ha permesso di ipotizzare come il lavoro dei geografi francesi della prima metà del XX secolo, e in particolare il contributo più rilevante di Marcel Poëte e di Pierre Lavedan, costituiscono le fonti principali e il campo d’indagine maggiormente esplorato da Rossi per definire la teoria della permanenza e i monumenti. Le permanenze non sono dunque presentate ne L’architettura della città come il “tutto”, ma emergono da un metodo che sceglie di isolare i fatti urbani permanenti, consentendo così di compiere un’ipotesi su “ciò che resta” dopo le trasformazioni continue che operano nella città. Le fonti su cui ho lavorato sono state quelle annunciate da Rossi ne L’architettura della città, e più precisamente i testi nelle edizioni da lui consultate. Anche questo lavoro ha permesso un confronto dei testi che ha fatto emergere ne L’architettura della città l’uso di termini mutuati da linguaggi appartenenti ad altre discipline e quale sia l’uso di concetti estrapolati nella loro interezza. Presupposti metodologici Della formulazione della nozione di fatto urbano si sono indagate l’originalità dell’espressione, le connessioni presunte o contenute negli studi di Rossi sulla città attraverso la raccolta di fonti dirette e indirette che sono andate a formare un notevole corpus di scritti. Le fonti dirette più rilevanti sono state trovare nelle collezioni speciali del Getty Research Institute di Los Angeles in cui sono conservati gli Aldo Rossi Papers, questo archivio comprende materiali inediti dal 1954 al 1988. La natura dei materiali si presenta sotto forma di manoscritti, dattiloscritti, quaderni, documenti ciclostilati, appunti sparsi e una notevole quantità di corrispondenza. Negli Aldo Rossi Papers si trovano anche 32 dei 47 Quaderni Azzurri, le bozze de L’architettura della città e dell’ Autobiografia Scientifica. Per quanto riguarda in particolare L’architettura della città negli Aldo Rossi Papers sono conservati: un quaderno con il titolo “Manuale d’urbanistica, giugno 1963”, chiara prima bozza del libro, degli “Appunti per libro urbanistica estate/inverno 1963”, un quaderno con la copertina rossa datato 20 settembre 1964-8 agosto 1965 e un quaderno con la copertina blu datato 30 agosto 1965-15 dicembre 1965. La possibilità di accedere a questo archivio ha permesso di incrementare la bibliografia relativa agli studi giovanili consentendo di rileggere il percorso culturale in cui Rossi si è formato. E’ così apparsa fondamentale la rivalutazione di alcune questioni relative al realismo socialista che hanno portato a formare un più preciso quadro dei primi scritti di Rossi sullo sfondo di un complesso scenario intellettuale. A questi testi si è affiancata la raccolta delle ricerche universitarie, degli articoli pubblicati su riviste specializzate e degli interventi a dibattiti e seminari. A proposito de L’architettura della città si è raccolta un’ampia letteratura critica riferita sia al testo in specifico che ad una sua collocazione nella storia dell’architettura, mettendo in discussione alcune osservazioni che pongono L’architettura della città come un libro risolutivo e definitivo. Per quanto riguarda il capitolo sulla teoria della permanenza l’analisi è stata svolta a partire dai testi che Rossi stesso indicava ne L’architettura della città rivelando i diversi apporti della letteratura urbanistica francese, e permettendo alla ricerca di precisare le relazioni con alcuni scritti centrali e al contempo colti da Rossi come opportunità per intraprendere l’elaborazione dell’idea di tipo. Per quest’ultima parte si può precisare come Rossi formuli la sua idea di tipo in un contesto culturale dove l’interesse per questo tema era fondamentale. Dunque le fonti che hanno assunto maggior rilievo in quest’ultima fase emergono da un ricco panorama in cui Rossi compie diverse ricerche sia con il gruppo redazionale di Casabella-continuità, sia all’interno della scuola veneziana negli anni Sessanta, ma anche negli studi per l’ILSES e per l’Istituto Nazionale d’Urbanistica. RESEARCH ON THE NOTION OF URBAN ARTIFACT IN THE ARCHITECTURE OF THE CITY BY ALDO ROSSI. Doctoral candidate: Letizia Biondi Tutor: Valter Balducci The present doctoral dissertation deals with the notion of urban artifact that was formulated and presented by Aldo Rossi in his book The Architecture of the City, published in 1966. In The Architecture of the City, the notion of urban artifact is enunciated through a wide range of definitions and forms. In this thesis, a research was done on how the construction of this concept over time was preceded by various studies started in 1953 during the author’s youth, then re-organized and synthesized since 1963 in a manuscript titled “Manual of urban planning” and in two more manuscripts later on. The work of research re-constructed the formulation of the notion of urban artifact through Rossi’s writings. In this sense, the examination of Rossi’s participation in debates, seminars, reviews, university courses or academic researches was of fundamental importance to understand the complexity of a work which is not to be attributed to disciplinary concepts, but to the formulation of a communicable theory. The effort to understand and to explain the notion of urban artifact led to an examination of the meaning used by Rossi to compose The Architecture of the City, which he defines as similar to a treatise. Through this analysis, it emerged that the composition of the book is not directly ascribable to the classical use of editorial writing of a treatise, whose most famous references in the past are the promotion of a correct practice as in the case of Vitruvio’s treatise, or the use of a structure that introduces a new category as in the Alberti case. Contrary to the two founding books, the lack of a global and prescriptive system and the not immediate reference to the writing of a classical treatise are evident in The Architecture of the City. However, the possibility of researching on some unpublished documents allowed to discover that in the writings starting from 1953 the analysis of the questions that are at the core of the notion of urban artifact is rich of intuitions, that aim to autonomy and that would be synthesized, even though not in a systematic way, in his famous book. The attempt was that of highlighting the specification over time of the notion of urban artifact and its elaboration in the various writings preceding the publication of The Architecture of the City. It was also specified that, despite building on theoretical grounds, Rossi indicates a progressive version of the notion of urban artifact, that is a performing use in the city. The present research aims to understand the cultural roots of the notion of urban artifact in two main directions: analyzing, firstly, Rossi’s interests along his formation path and, secondly, the definition of material structure of an urban artifact identified by Rossi in the permanences and enriched by various contributions from other disciplines. The purpose of the present research is to revise the formation path made by Rossi in a critical way, starting by 1953, underlining its innovative aspects and identifying its describing limits, which will never lead to the formulation of an exact notion, but rather to the elaboration of a complex synthesis, enriched by references to other studies. In brief, the thesis is composed of three parts: 1. The first part, titled “The Theory of urban artifacts in The Architecture of the City”, analyzes the concept of urban artifact in the more general theoretical context of the book The Architecture of the City. Such analysis is done by “disassembling” the book, and by linking together the argumentations and the multiplicity of the sources which are explicitly quoted by Rossi. In this context, the book’s structure is defined more precisely through the revision of the references used by Rossi to compose his theoretical project. Moreover, the author’s life is traced back through the various editions, re-printings, introductions and illustrations. Finally, it is specified which role the concept of urban artifact has in the book, pointing out that it is placed in an equal relation with the book’s title; by so doing, the concept of urban artifact gets the new meaning of “fact to be observed”, similar to the use that was suggested by the French urban geography at the beginning of the 20th century. 2. The second part, titled “The formation of the notion of urban artifact 1953-66”, introduces the theoretical elaboration in Rossi’s writings before The Architecture of the City, that is from 1953 to 1966. This part tries to describe Rossi’s cultural roots, his collaborations and his interests, tracing back the progressive definition of his conception of city over time. The analysis focuses on the path followed by Rossi and on the documents that he wrote since the years as a student at the Department of Architecture at the Politecnico in Milan. This leads to a complex scenario of first essays, articles and notes that bear witness to the intellectual research aiming to the construction of a knowledge on the background of the Realism of the 1950s. Rossi develops, in fact, a cultural engagement that leads him after his studies to deal with more general issues about the city. In particular, his important collaboration with the architecture magazine “Casabella-continuità”, with the director Ernesto Nathan Rogers and with the whole redaction staff mark the following period when he starts getting interested in city planning literature, art, sociology, geography, economics and philosophy. Since 1963, Rossi has worked with the group directed by Carlo Aymonino at the “Istituto Universitario di Architettura” (University Institute of Architecture) in Venice, especially researching on building typologies and urban morphology. During these years, Rossi elaborates an analytical synthesis for the formulation of a theory about the city. From the present research, it is evident that the writings preceding The Architecture of the City develop the studies on urban artifacts, which will become theoretical core of different chapters of the book. In conclusion, the genesis of the book is described; written in two years, what was conceived to be an “urban planning manual” became a “treatise draft” for the formulation of an urban science, as Rossi defines it. 3. The third part is titled “The material structure of urban artifacts: the theory of permanence”. This research is made on the study of the city as a material fact, a manufacture, whose construction was made over time, bearing the traces of time. As far as the topic of permanence is concerned, it was also important to draw a comparison with the debate about the issues of environmental pre-existence of re-construction in historical areas, which was very lively during the years of the Reconstruction. Right from the beginning, of fundamental importance were the relationship with Ernesto Nathan Rogers, the discussions on the pages of Casabella-Continuità and the participation to some debates and researches. It is to note that various terms were taken by the philosophical thesis by some personalities such as Antonio Banfi and Enzo Paci, and then re-elaborated by the redaction staff at Casabella-Continuità, which Rossi took part in as well. Through this analysis, it emerged that there were some shifts in meaning and the formulation of a vocabulary of terms within the complex area of the architectonic culture in the 1950s and 1960s. Then, I examined the shapes in which Rossi introduces the definition of the theory of permanence and the references by some authors for the scientific construction of an architecture theory whose aim is being communicable and offering concrete research tools. Such analysis allowed making a hypothesis about the significance for Rossi of the French geographers of the first half of the 20th century: in particular, the work by Marcel Poëte and by Pierre Lavedan is the main source and the research area which Rossi mostly explored to define the theory of permanence and monuments. Therefore, in The Architecture of the City, permanencies are not presented as the “whole”, but they emerge from a method which isolates permanent urban artifacts, in this way allowing making a hypothesis on “what remains” after the continuous transformations made in the city. The sources examined were quoted by Rossi in The Architecture of the City; in particular I analyzed them in the same edition which Rossi referred to. Through such an analysis, it was possible to make a comparison of the texts with one another, which let emerge the use of terms taken by languages belonging to other disciplines in The Architecture of the City and which the use of wholly extrapolated concepts is. Methodological premises As far as the formulation of the notion of urban artifact is concerned, the analysis focuses on the originality of the expression, the connections that are assumed or contained in Rossi’s writings about the city, by collecting direct and indirect sources which formed a significant corpus of writings. The most relevant direct sources were found in the special collections of the Getty Research Institute in Los Angeles, where the “Aldo Rossi Papers” are conserved. This archive contains unpublished material from 1954 to 1988, such as manuscripts, typescripts, notebooks, cyclostyled documents, scraps and notes, and several letters. In the Aldo Rossi Papers there are also 32 out of the 47 Light Blue Notebooks (Quaderni Azzurri), the rough drafts of The Architecture of the City and of the “A Scientific Autobiography”. As regards The Architecture of the City in particular, the Aldo Rossi Papers preserve: a notebook by the title of “Urban planning manual, June, 1963”, which is an explicit first draft of the book; “Notes for urban planning book summer/winter 1963”; a notebook with a red cover dated September 20th, 1964 – August 8th, 1965; and a notebook with a blue cover dated August 30th, 1965 – December 15th, 1965. The possibility of accessing this archive allowed to increase the bibliography related to the youth studies, enabling a revision of the cultural path followed by Rossi’s education. To that end, it was fundamental to re-evaluate some issues linked to the socialist realism which led to a more precise picture of the first writings by Rossi against the background of the intellectual scenario where he formed. In addition to these texts, the collection of university researches, the articles published on specialized reviews and the speeches at debates and seminars were also examined. About The Architecture of the City, a wide-ranging critical literature was collected, related both to the text specifics and to its collocation in the story of architecture, questioning some observations which define The Architecture of the City as a conclusive and definite book. As far as the chapter on the permanence theory is concerned, the analysis started by the texts that Rossi indicated in The Architecture of the City, revealing the different contributions from the French literature on urban planning. This allowed to the present research a more specific definition of the connections to some central writings which, at the same time, were seen by Rossi as an opportunity to start up the elaboration of the idea of type. For this last part, it can be specified that Rossi formulates his idea of type in a cultural context where the interest in this topic was fundamental. Therefore, the sources which played a central role in this final phase emerge from an extensive panorama in which Rossi researched not only with the redaction staff at Casablanca-continuità and within the School of Venice in the 1960s, but also in his studies for the ILSES (Institute of the Region Lombardia for Economics and Social Studies) and for the National Institute of Urban Planning.

Expressiveness of Concurrent Languages

The aim of this thesis is to go through different approaches for proving expressiveness properties in several concurrent languages. We analyse four different calculi exploiting for each one a different technique. We begin with the analysis of a synchronous language, we explore the expressiveness of a fragment of CCS! (a variant of Milner's CCS where replication is considered instead of recursion) w.r.t. the existence of faithful encodings (i.e. encodings that respect the behaviour of the encoded model without introducing unnecessary computations) of models of computability strictly less expressive than Turing Machines. Namely, grammars of types 1,2 and 3 in the Chomsky Hierarchy. We then move to asynchronous languages and we study full abstraction for two Linda-like languages. Linda can be considered as the asynchronous version of CCS plus a shared memory (a multiset of elements) that is used for storing messages. After having defined a denotational semantics based on traces, we obtain fully abstract semantics for both languages by using suitable abstractions in order to identify different traces which do not correspond to different behaviours. Since the ability of one of the two variants considered of recognising multiple occurrences of messages in the store (which accounts for an increase of expressiveness) reflects in a less complex abstraction, we then study other languages where multiplicity plays a fundamental role. We consider the language CHR (Constraint Handling Rules) a language which uses multi-headed (guarded) rules. We prove that multiple heads augment the expressive power of the language. Indeed we show that if we restrict to rules where the head contains at most n atoms we could generate a hierarchy of languages with increasing expressiveness (i.e. the CHR language allowing at most n atoms in the heads is more expressive than the language allowing at most m atoms, with m

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.

Expressiveness in biologically inspired languages

A very recent and exciting new area of research is the application of Concurrency Theory tools to formalize and analyze biological systems and one of the most promising approach comes from the process algebras (process calculi). A process calculus is a formal language that allows to describe concurrent systems and comes with well-established techniques for quantitative and qualitative analysis. Biological systems can be regarded as concurrent systems and therefore modeled by means of process calculi. In this thesis we focus on the process calculi approach to the modeling of biological systems and investigate, mostly from a theoretical point of view, several promising bio-inspired formalisms: Brane Calculi and k-calculus family. We provide several expressiveness results mostly by means of comparisons between calculi. We provide a lower bound to the computational power of the non Turing complete MDB Brane Calculi by showing an encoding of a simple P-System into MDB. We address the issue of local implementation within the k-calculus family: whether n-way rewrites can be simulated by binary interactions only. A solution introducing divergence is provided and we prove a deterministic solution preserving the termination property is not possible. We use the symmetric leader election problem to test synchronization capabilities within the k-calculus family. Several fragments of the original k-calculus are considered and we prove an impossibility result about encoding n-way synchronization into (n-1)-way synchronization. A similar impossibility result is obtained in a pure computer science context. We introduce CCSn, an extension of CCS with multiple input prefixes and show, using the dining philosophers problem, that there is no reasonable encoding of CCS(n+1) into CCSn.

Investigations on formation and specification of neural precursor cells in the central nervous system of the Drosophila melanogaster embryo

Investigations on formation and specification of neural precursor cells in the central nervous system of the Drosophila melanogaster embryoSpecification of a unique cell fate during development of a multicellular organism often is a function of its position. The Drosophila central nervous system (CNS) provides an ideal system to dissect signalling events during development that lead to cell specific patterns. Different cell types in the CNS are formed from a relatively few precursor cells, the neuroblasts (NBs), which delaminate from the neurogenic region of the ectoderm. The delamination occurs in five waves, S1-S5, finally leading to a subepidermal layer consisting of about 30 NBs, each with a unique identity, arranged in a stereotyped spatial pattern in each hemisegment. This information depends on several factors such as the concentrations of various morphogens, cell-cell interactions and long range signals present at the position and time of its birth. The early NBs, delaminating during S1 and S2, form an orthogonal array of four rows (2/3,4,5,6/7) and three columns (medial, intermediate, and lateral) . However, the three column and four row-arrangement pattern is only transitory during early stages of neurogenesis which is obscured by late emerging (S3-S5) neuroblasts (Doe and Goodman, 1985; Goodman and Doe, 1993). Therefore the aim of my study has been to identify novel genes which play a role in the formation or specification of late delaminating NBs.In this study the gene anterior open or yan was picked up in a genetic screen to identity novel and yet unidentified genes in the process of late neuroblast formation and specification. I have shown that the gene yan is responsible for maintaining the cells of the neuroectoderm in an undifferentiated state by interfering with the Notch signalling mechanism. Secondly, I have studied the function and interactions of segment polarity genes within a certain neuroectodermal region, namely the engrailed (en) expressing domain, with regard to the fate specification of a set of late neuroblasts, namely NB 6-4 and NB 7-3. I have dissected the regulatory interaction of the segment polarity genes wingless (wg), hedgehog (hh) and engrailed (en) as they maintain each other’s expression to show that En is a prerequisite for neurogenesis and show that the interplay of the segmentation genes naked (nkd) and gooseberry (gsb), both of which are targets of wingless (wg) activity, leads to differential commitment of NB 7-3 and NB 6-4 cell fate. I have shown that in the absence of either nkd or gsb one NB fate is replaced by the other. However, the temporal sequence of delamination is maintained, suggesting that formation and specification of these two NBs are under independent control.

Theoretical and implementation aspects in the mechanization of the metatheory of programming languages

Interactive theorem provers are tools designed for the certification of formal proofs developed by means of man-machine collaboration. Formal proofs obtained in this way cover a large variety of logical theories, ranging from the branches of mainstream mathematics, to the field of software verification. The border between these two worlds is marked by results in theoretical computer science and proofs related to the metatheory of programming languages. This last field, which is an obvious application of interactive theorem proving, poses nonetheless a serious challenge to the users of such tools, due both to the particularly structured way in which these proofs are constructed, and to difficulties related to the management of notions typical of programming languages like variable binding. This thesis is composed of two parts, discussing our experience in the development of the Matita interactive theorem prover and its use in the mechanization of the metatheory of programming languages. More specifically, part I covers: - the results of our effort in providing a better framework for the development of tactics for Matita, in order to make their implementation and debugging easier, also resulting in a much clearer code; - a discussion of the implementation of two tactics, providing infrastructure for the unification of constructor forms and the inversion of inductive predicates; we point out interactions between induction and inversion and provide an advancement over the state of the art. In the second part of the thesis, we focus on aspects related to the formalization of programming languages. We describe two works of ours: - a discussion of basic issues we encountered in our formalizations of part 1A of the Poplmark challenge, where we apply the extended inversion principles we implemented for Matita; - a formalization of an algebraic logical framework, posing more complex challenges, including multiple binding and a form of hereditary substitution; this work adopts, for the encoding of binding, an extension of Masahiko Sato's canonical locally named representation we designed during our visit to the Laboratory for Foundations of Computer Science at the University of Edinburgh, under the supervision of Randy Pollack.

A study of two Languages for Active Objects with Futures

In computer systems, specifically in multithread, parallel and distributed systems, a deadlock is both a very subtle problem - because difficult to pre- vent during the system coding - and a very dangerous one: a deadlocked system is easily completely stuck, with consequences ranging from simple annoyances to life-threatening circumstances, being also in between the not negligible scenario of economical losses. Then, how to avoid this problem? A lot of possible solutions has been studied, proposed and implemented. In this thesis we focus on detection of deadlocks with a static program analysis technique, i.e. an analysis per- formed without actually executing the program. To begin, we briefly present the static Deadlock Analysis Model devel- oped for coreABS−− in chapter 1, then we proceed by detailing the Class- based coreABS−− language in chapter 2. Then, in Chapter 3 we lay the foundation for further discussions by ana- lyzing the differences between coreABS−− and ASP, an untyped Object-based calculi, so as to show how it can be possible to extend the Deadlock Analysis to Object-based languages in general. In this regard, we explicit some hypotheses in chapter 4 first by present- ing a possible, unproven type system for ASP, modeled after the Deadlock Analysis Model developed for coreABS−−. Then, we conclude our discussion by presenting a simpler hypothesis, which may allow to circumvent the difficulties that arises from the definition of the ”ad-hoc” type system discussed in the aforegoing chapter.

Engineering Agent-Oriented Technologies and Programming Languages for Computer Programming and Software Development

Mainstream hardware is becoming parallel, heterogeneous, and distributed on every desk, every home and in every pocket. As a consequence, in the last years software is having an epochal turn toward concurrency, distribution, interaction which is pushed by the evolution of hardware architectures and the growing of network availability. This calls for introducing further abstraction layers on top of those provided by classical mainstream programming paradigms, to tackle more effectively the new complexities that developers have to face in everyday programming. A convergence it is recognizable in the mainstream toward the adoption of the actor paradigm as a mean to unite object-oriented programming and concurrency. Nevertheless, we argue that the actor paradigm can only be considered a good starting point to provide a more comprehensive response to such a fundamental and radical change in software development. Accordingly, the main objective of this thesis is to propose Agent-Oriented Programming (AOP) as a high-level general purpose programming paradigm, natural evolution of actors and objects, introducing a further level of human-inspired concepts for programming software systems, meant to simplify the design and programming of concurrent, distributed, reactive/interactive programs. To this end, in the dissertation first we construct the required background by studying the state-of-the-art of both actor-oriented and agent-oriented programming, and then we focus on the engineering of integrated programming technologies for developing agent-based systems in their classical application domains: artificial intelligence and distributed artificial intelligence. Then, we shift the perspective moving from the development of intelligent software systems, toward general purpose software development. Using the expertise maturated during the phase of background construction, we introduce a general-purpose programming language named simpAL, which founds its roots on general principles and practices of software development, and at the same time provides an agent-oriented level of abstraction for the engineering of general purpose software systems.

Statistical analysis of written languages

La tesi presenta una serie di risultati dell'analisi quantitativa sulla linguistica. Inizialmente sono studiate due fra le leggi empiriche più famose di questo campo, le leggi di Zipf e Heaps, e vengono esposti vari modelli sullo sviluppo del linguaggio. Nella seconda parte si giunge alla discussione di risultati più specifici sulla presenza di fenomeni di burstiness e di correlazioni a lungo raggio nei testi. Tutti questi studi teorici sono affiancati da analisi sperimentali, svolte utilizzando varie traduzioni del libro "Guerra e pace" di Leo Tolstoj e concentrate principalmente sulle eventuali differenze riscontrabili tra le diverse lingue.

Extending Implicit Computational Complexity and Abstract Machines to Languages with Control

The Curry-Howard isomorphism is the idea that proofs in natural deduction can be put in correspondence with lambda terms in such a way that this correspondence is preserved by normalization. The concept can be extended from Intuitionistic Logic to other systems, such as Linear Logic. One of the nice conseguences of this isomorphism is that we can reason about functional programs with formal tools which are typical of proof systems: such analysis can also include quantitative qualities of programs, such as the number of steps it takes to terminate. Another is the possiblity to describe the execution of these programs in terms of abstract machines. In 1990 Griffin proved that the correspondence can be extended to Classical Logic and control operators. That is, Classical Logic adds the possiblity to manipulate continuations. In this thesis we see how the things we described above work in this larger context.

Spagnolo Tecnico Semplificato

L’obiettivo della presente dissertazione è quello di creare un nuovo linguaggio controllato, denominato Español Técnico Simplificado (ETS). Basato sulla specifica tecnica del Simplified Technical English (STE), ufficialmente conosciuta come ASD-STE100, lo spagnolo controllato ETS si presenta come un documento metalinguistico in grado di fornire ad un redattore o traduttore tecnico alcune regole specifiche per produrre un documento tecnico. La strategia di implementazione conduce allo studio preliminare di alcuni linguaggi controllati simili all’inglese STE, quali il Français Rationalisé e il Simplified Technical Spanish. Attraverso un approccio caratteristico della linguistica dei corpora, la soluzione proposta fornisce il nuovo linguaggio controllato mediante l’estrazione di informazioni specifiche da un corpus ad-hoc di lingua spagnola appositamente creato ed interrogato. I risultati evidenziano un metodo linguistico (controllato) utile a produrre documentazione tecnica priva di ogni eventuale ambiguità. Il sistema ETS, infatti, si fonda sul concetto della intelligibilità in quanto condizione necessaria da soddisfare nell’ambito della produzione di un testo controllato. E, attraverso la sua macrostruttura, il documento ETS fornisce gli strumenti necessari per rendere il testo controllato univoco. Infatti, tale struttura bipartita suddivide in maniera logica i dettami: una prima parte riguarda e contiene regole sintattiche e stilistiche; una seconda parte riguarda e contiene un dizionario di un numero limitato di lemmi opportunamente selezionati. Il tutto a favore del principio della biunivocità dei segni, in questo caso, della lingua spagnola. Il progetto, nel suo insieme, apre le porte ad un linguaggio nuovo in alternativa a quelli presenti, totalmente creato in accademia, che vale come prototipo a cui far seguire altri progetti di ricerca.

The languages of postcolonial ireland and their potential for cultural expression

Ireland is a country in which two languages are spoken: English and Irish. This thesis analyzes the historical relationship between the languages, the cultural codes and meanings attached to each of them, as well as how much of the culture of its speakers each is able to carry. Beyond that, the influence the two languages have exercised on one another and their mutual entwinement is taken into closer examination.

Acknowledging linguistic diversity in a multicultural society: the issue of indigenous languages in Colombia.

Nowadays, modern society is gradually becoming multicultural. However, only in the last few years awareness on its importance has been raised. In the case of Colombia, multiculturalism has existed since the pre-Columbian period and today there are more than 80 ethnic groups and 65 indigenous languages in the country. The aim of this work is to illustrate the status of indigenous languages in Colombia and to enlighten about the importance of recognizing, protecting and strengthening the use of these native languages. Subsequent to this, it will be point out that linguistic diversity should be considered a resource and not a barrier to achieve unity in diversity. Finally, ethno-education will be presented as an adequate educational program that may guarantee an equal linguistic representation in the country.