Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

L'eredità di Aldo Rossi nella Penisola Iberica. La costruzione della città e il progetto contemporaneo

Descrizione, tema e obiettivi della ricerca La ricerca si propone lo studio delle possibili influenze che la teoria di Aldo Rossi ha avuto sulla pratica progettuale nella Penisola Iberica, intende quindi affrontare i caratteri fondamentali della teoria che sta alla base di un metodo progettuale ed in particolar modo porre l'attenzione alle nuove costruzioni quando queste si confrontano con le città storiche. Ha come oggetto principale lo studio dei documenti, saggi e scritti riguardanti il tema della costruzione all'interno delle città storiche. Dallo studio di testi selezionati di Aldo Rossi sulla città si vuole concentrare l'attenzione sull'influenza che tale teoria ha avuto nei progetti della Penisola Iberica, studiare come è stata recepita e trasmessa successivamente, attraverso gli scritti di autori spagnoli e come ha visto un suo concretizzarsi poi nei progetti di nuove costruzioni all'interno delle città storiche. Si intende restringere il campo su un periodo ed un luogo precisi, Spagna e Portogallo a partire dagli anni Settanta, tramite la lettura di un importante evento che ha ufficializzato il contatto dell'architetto italiano con la Penisola Iberica, quale il Seminario di Santiago de Compostela tenutosi nel 1976. Al Seminario parteciparono numerosi architetti che si confrontarono su di un progetto per la città di Santiago e furono invitati personaggi di fama internazionale a tenere lezioni introduttive sul tema di dibattito in merito al progetto e alla città storica. Il Seminario di Santiago si colloca in un periodo storico cruciale per la Penisola Iberica, nel 1974 cade il regime salazarista in Portogallo e nel 1975 cade il regime franchista in Spagna ed è quindi di rilevante importanza capire il legame tra l'architettura e la nuova situazione politica. Dallo studio degli interventi, dei progetti che furono prodotti durante il Seminario, della relazione tra questo evento ed il periodo storico in cui esso va contestualizzato, si intende giungere alla individuazione delle tracce della reale presenza di tale eredità. Presupposti metodologici. Percorso e strumenti di ricerca La ricerca può quindi essere articolata in distinte fasi corrispondenti per lo più ai capitoli in cui si articola la tesi: una prima fase con carattere prevalentemente storica, di ricerca del materiale per poter definire il contesto in cui si sviluppano poi le vicende oggetto della tesi; una seconda fase di impronta teorica, ossia di ricerca bibliografica del materiale e delle testimonianze che provvedono alla definizione della reale presenza di effetti scaturiti dai contatti tra Rossi e la Penisola Iberica, per andare a costruire una eredità ; una terza fase che entra nel merito della composizione attraverso lo studio e la verifica delle prime due parti, tramite l'analisi grafica applicata ad uno specifico esempio architettonico selezionato; una quarta fase dove il punto di vista viene ribaltato e si indaga l'influenza dei luoghi visitati e dei contatti intrattenuti con alcuni personaggi della Penisola Iberica sull'architettura di Rossi, ricercandone i riferimenti. La ricerca è stata condotta attraverso lo studio di alcuni eventi selezionati nel corso degli anni che si sono mostrati significativi per l'indagine, per la risonanza che hanno avuto sulla storia dell'architettura della Penisola. A questo scopo si sono utilizzati principalmente tre strumenti: lo studio dei documenti, le pubblicazioni e le riviste prodotte in Spagna, gli scritti di Aldo Rossi in merito, e la testimonianza diretta attraverso interviste di personaggi chiave. La ricerca ha prodotto un testo suddiviso per capitoli che rispetta l'organizzazione in fasi di lavoro. A seguito di determinate condizioni storiche e politiche, studiate nella ricerca a supporto della tesi espressa, nella Penisola Iberica si è verificato il diffondersi della necessità e del desiderio di guardare e prendere a riferimento l'architettura europea e in particolar modo quella italiana. Il periodo sul quale viene focalizzata l'attenzione ha inizio negli anni Sessanta, gli ultimi prima della caduta delle dittature, scenario dei primi viaggi di Aldo Rossi nella Penisola Iberica. Questi primi contatti pongono le basi per intense e significative relazioni future. Attraverso l'approfondimento e la studio dei materiali relativi all'oggetto della tesi, si è cercato di mettere in luce il contesto culturale, l'attenzione e l'interesse per l'apertura di un dibattito intorno all'architettura, non solo a livello nazionale, ma europeo. Ciò ha evidenziato il desiderio di innescare un meccanismo di discussione e scambio di idee, facendo leva sull'importanza dello sviluppo e ricerca di una base teorica comune che rende coerente i lavori prodotti nel panorama architettonico iberico, seppur ottenendo risultati che si differenziano gli uni dagli altri. E' emerso un forte interesse per il discorso teorico sull'architettura, trasmissibile e comunicabile, che diventa punto di partenza per un metodo progettuale. Ciò ha reso palese una condivisione di intenti e l'assunzione della teoria di Aldo Rossi, acquisita, diffusa e discussa, attraverso la pubblicazione dei suoi saggi, la conoscenza diretta con l'architetto e la sua architettura, conferenze, seminari, come base teorica su cui fondare il proprio sapere architettonico ed il processo metodologico progettuale da applicare di volta in volta negli interventi concreti. Si è giunti così alla definizione di determinati eventi che hanno permesso di entrare nel profondo della questione e di sondare la relazione tra Rossi e la Penisola Iberica, il materiale fornito dallo studio di tali episodi, quali il I SIAC, la diffusione della rivista "2C. Construccion de la Ciudad", la Coleccion Arquitectura y Critica di Gustavo Gili, hanno poi dato impulso per il reperimento di una rete di ulteriori riferimenti. E' stato possibile quindi individuare un gruppo di architetti spagnoli, che si identificano come allievi del maestro Rossi, impegnato per altro in quegli anni nella formazione di una Scuola e di un insegnamento, che non viene recepito tanto nelle forme, piuttosto nei contenuti. I punti su cui si fondano le connessioni tra l'analisi urbana e il progetto architettonico si centrano attorno due temi di base che riprendono la teoria esposta da Rossi nel saggio L'architettura della città : - relazione tra l'area-studio e la città nella sua globalità, - relazione tra la tipologia edificatoria e gli aspetti morfologici. La ricerca presentata ha visto nelle sue successive fasi di approfondimento, come si è detto, lo sviluppo parallelo di più tematiche. Nell'affrontare ciascuna fase è stato necessario, di volta in volta, operare una verifica delle tappe percorse precedentemente, per mantenere costante il filo del discorso col lavoro svolto e ritrovare, durante lo svolgimento stesso della ricerca, gli elementi di connessione tra i diversi episodi analizzati. Tale operazione ha messo in luce talvolta nodi della ricerca rimasti in sospeso che richiedevano un ulteriore approfondimento o talvolta solo una rivisitazione per renderne possibile un più proficuo collegamento con la rete di informazioni accumulate. La ricerca ha percorso strade diverse che corrono parallele, per quanto riguarda il periodo preso in analisi: - i testi sulla storia dell'architettura spagnola e la situazione contestuale agli anni Settanta - il materiale riguardante il I SIAC - le interviste ai partecipanti al I SIAC - le traduzioni di Gustavo Gili nella Coleccion Arquitectura y Critica - la rivista "2C. Construccion de la Ciudad" Esse hanno portato alla luce una notevole quantità di tematiche, attraverso le quali, queste strade vengono ad intrecciarsi e a coincidere, verificando l'una la veridicità dell'altra e rafforzandone il valore delle affermazioni. Esposizione sintetica dei principali contenuti esposti dalla ricerca Andiamo ora a vedere brevemente i contenuti dei singoli capitoli. Nel primo capitolo Anni Settanta. Periodo di transizione per la Penisola Iberica si è cercato di dare un contesto storico agli eventi studiati successivamente, andando ad evidenziare gli elementi chiave che permettono di rintracciare la presenza della predisposizione ad un cambiamento culturale. La fase di passaggio da una condizione di chiusura rispetto alle contaminazioni provenienti dall'esterno, che caratterizza Spagna e Portogallo negli anni Sessanta, lascia il posto ad un graduale abbandono della situazione di isolamento venutasi a creare intorno al Paese a causa del regime dittatoriale, fino a giungere all'apertura e all'interesse nei confronti degli apporti culturali esterni. E' in questo contesto che si gettano le basi per la realizzazione del I Seminario Internazionale di Architettura Contemporanea a Santiago de Compostela, del 1976, diretto da Aldo Rossi e organizzato da César Portela e Salvador Tarragó, di cui tratta il capitolo secondo. Questo è uno degli eventi rintracciati nella storia delle relazioni tra Rossi e la Penisola Iberica, attraverso il quale è stato possibile constatare la presenza di uno scambio culturale e l'importazione in Spagna delle teorie di Aldo Rossi. Organizzato all'indomani della caduta del franchismo, ne conserva una reminescenza formale. Il capitolo è organizzato in tre parti, la prima si occupa della ricostruzione dei momenti salienti del Seminario Proyecto y ciudad historica, dagli interventi di architetti di fama internazionale, quali lo stesso Aldo Rossi, Carlo Aymonino, James Stirling, Oswald Mathias Ungers e molti altri, che si confrontano sul tema delle città storiche, alle giornate seminariali dedicate all’elaborazione di un progetto per cinque aree individuate all’interno di Santiago de Compostela e quindi dell’applicazione alla pratica progettuale dell’inscindibile base teorica esposta. Segue la seconda parte dello stesso capitolo riguardante La selezione di interviste ai partecipanti al Seminario. Esso contiene la raccolta dei colloqui avuti con alcuni dei personaggi che presero parte al Seminario e attraverso le loro parole si è cercato di approfondire la materia, in particolar modo andando ad evidenziare l’ambiente culturale in cui nacque l’idea del Seminario, il ruolo avuto nella diffusione della teoria di Aldo Rossi in Spagna e la ripercussione che ebbe nella pratica costruttiva. Le diverse interviste, seppur rivolte a persone che oggi vivono in contesti distanti e che in seguito a questa esperienza collettiva hanno intrapreso strade diverse, hanno fatto emergere aspetti comuni, tale unanimità ha dato ancor più importanza al valore di testimonianza offerta. L’elemento che risulta più evidente è il lascito teorico, di molto prevalente rispetto a quello progettuale che si è andato mescolando di volta in volta con la tradizione e l’esperienza dei cosiddetti allievi di Aldo Rossi. Negli stessi anni comincia a farsi strada l’importanza del confronto e del dibattito circa i temi architettonici e nel capitolo La fortuna critica della teoria di Aldo Rossi nella Penisola Iberica è stato affrontato proprio questo rinnovato interesse per la teoria che in quegli anni si stava diffondendo. Si è portato avanti lo studio delle pubblicazioni di Gustavo Gili nella Coleccion Arquitectura y Critica che, a partire dalla fine degli anni Sessanta, pubblica e traduce in lingua spagnola i più importanti saggi di architettura, tra i quali La arquitectura de la ciudad di Aldo Rossi, nel 1971, e Comlejidad y contradiccion en arquitectura di Robert Venturi nel 1972. Entrambi fondamentali per il modo di affrontare determinate tematiche di cui sempre più in quegli anni si stava interessando la cultura architettonica iberica, diventando così ¬ testi di riferimento anche nelle scuole. Le tracce dell’influenza di Rossi sulla Penisola Iberica si sono poi ricercate nella rivista “2C. Construccion de la Ciudad” individuata come strumento di espressione di una teoria condivisa. Con la nascita nel 1972 a Barcellona di questa rivista viene portato avanti l’impegno di promuovere la Tendenza, facendo riferimento all’opera e alle idee di Rossi ed altri architetti europei, mirando inoltre al recupero di un ruolo privilegiato dell’architettura catalana. A questo proposito sono emersi due fondamentali aspetti che hanno legittimato l’indagine e lo studio di questa fonte: - la diffusione della cultura architettonica, il controllo ideologico e di informazione operato dal lavoro compiuto dalla rivista; - la documentazione circa i criteri di scelta della redazione a proposito del materiale pubblicato. E’ infatti attraverso le pubblicazioni di “2C. Construccion de la Ciudad” che è stato possibile il ritrovamento delle notizie sulla mostra Arquitectura y razionalismo. Aldo Rossi + 21 arquitectos españoles, che accomuna in un’unica esposizione le opere del maestro e di ventuno giovani allievi che hanno recepito e condiviso la teoria espressa ne “L’architettura della città”. Tale mostra viene poi riproposta nella Sezione Internazionale di Architettura della XV Triennale di Milano, la quale dedica un Padiglione col titolo Barcelona, tres epocas tres propuestas. Dalla disamina dei progetti presentati è emerso un interessante caso di confronto tra le Viviendas para gitanos di César Portela e la Casa Bay di Borgo Ticino di Aldo Rossi, di cui si è occupato l’ultimo paragrafo di questo capitolo. Nel corso degli studi è poi emerso un interessante risvolto della ricerca che, capovolgendone l’oggetto stesso, ne ha approfondito gli aspetti cercando di scavare più in profondità nell’analisi della reciproca influenza tra la cultura iberica e Aldo Rossi, questa parte, sviscerata nell’ultimo capitolo, La Penisola Iberica nel “magazzino della memoria” di Aldo Rossi, ha preso il posto di quello che inizialmente doveva presentarsi come il risvolto progettuale della tesi. Era previsto infatti, al termine dello studio dell’influenza di Aldo Rossi sulla Penisola Iberica, un capitolo che concentrava l’attenzione sulla produzione progettuale. A seguito dell’emergere di un’influenza di carattere prettamente teorica, che ha sicuramente modificato la pratica dal punto di vista delle scelte architettoniche, senza però rendersi esplicita dal punto di vista formale, si è preferito, anche per la difficoltà di individuare un solo esempio rappresentativo di quanto espresso, sostituire quest’ultima parte con lo studio dell’altra faccia della medaglia, ossia l’importanza che a sua volta ha avuto la cultura iberica nella formazione della collezione dei riferimenti di Aldo Rossi. L’articolarsi della tesi in fasi distinte, strettamente connesse tra loro da un filo conduttore, ha reso necessari successivi aggiustamenti nel percorso intrapreso, dettati dall’emergere durante la ricerca di nuovi elementi di indagine. Si è pertanto resa esplicita la ricercata eredità di Aldo Rossi, configurandosi però prevalentemente come un’influenza teorica che ha preso le sfumature del contesto e dell’esperienza personale di chi se ne è fatto ricevente, diventandone così un continuatore attraverso il proprio percorso autonomo o collettivo intrapreso in seguito. Come suggerisce José Charters Monteiro, l’eredità di Rossi può essere letta attraverso tre aspetti su cui si basa la sua lezione: la biografia, la teoria dell’architettura, l’opera. In particolar modo per quanto riguarda la Penisola Iberica si può parlare dell’individuazione di un insegnamento riferito alla seconda categoria, i suoi libri di testo, le sue partecipazioni, le traduzioni. Questo è un lascito che rende possibile la continuazione di un dibattito in merito ai temi della teoria dell’architettura, della sue finalità e delle concrete applicazioni nelle opere, che ha permesso il verificarsi di una apertura mentale che mette in relazione l’architettura con altre discipline umanistiche e scientifiche, dalla politica, alla sociologia, comprendendo l’arte, le città la morfologia, la topografia, mediate e messe in relazione proprio attraverso l’architettura.

Effetti degli accordi Euro-Mediterrani sul comparto dell'ortofrutta fresca

In 1995, the European Union (EU) Member States and 12 Mediterranean countries launched in Barcelona a liberalization process that aims at establishing a free trade area (to be realized by 2010) and at promoting a sustainable and balanced economic development by the adoption of a new generation of Agreements: the Euro-Mediterranean Agreements (EMA). For the Mediterranean partner countries, the main concern is a better access for their fruit and vegetable exports to the European market. These products represent the main exports of these countries, and the EU is their first trading partner. On the other side, for the EU the main issue is not only the promotion of its products, but also the protection of its fruit and vegetables producers. Moreover, the trade with third countries is the key element of the Common Market Organization of the sector. Fruit and vegetables represent a very sensitive sector since their high seasonality, high perishability, and especially since the production of the Mediterranean countries is often similar to the European Mediterranean’s countries one. In fact, the agreements define preferences at the entrance of the EU market providing limited concessions for each partner, for specific products, limited quantities and calendars. This research tries to analyze the bilateral trade volume for fresh fruit and vegetables in the European and Italian markets in order to assess the effects of Mediterranean liberalization on this sector. Free trade of agricultural products represents a very actual topic in international trade and the Mediterranean countries, recognised as big producers of fruit and vegetables, as big exporters of their crops and actually significantly present on the European market, could be high competitors with the inward production because the outlet could be the same. The goal of this study is to provide some considerations about the competitiveness of mediterranean fruit and vegetables productions after Barcelona Process, in a first step for the European market and then also for the Italian one. The aim is to discuss the influence of the euro-mediterranean agreements on the fruit and vegetables trade between 10 foreign Mediterranean countries (Algeria, Egypt, Israel, Jordan, Libya, Lebanon, Morocco, Tunisia, Syria, and Turkey) and 15 EU countries in the period 1995-2007, by means of a gravity model, which is a widespread methodology in international trade analysis. The basic idea of gravity models is that bilateral trade from one country to another (as the dependent variable) can be explained by a set of factors: - factors that capture the potential of a country to export goods and services; - factors that capture the propensity of a country to imports goods and services; - any other forces that either attract or inhibit bilateral trade. This analysis compares only imports’ flows by Europe and by Italy (in volumes) from Mediterranean countries, since the exports’ flows toward those foreign countries are not significant, especially for Italy. The market of fruit and vegetables appears as a high heterogeneous group so it is very difficult to show a synthesis of the analysis performed and the related results. In fact, this sector includes the so called “poor products” (such as potatoes and legumes), and the “rich product”, such as nuts or exotic fruit, and there are a lot of different goods that arouse a dissimilar consumer demand which directly influence the import requirements. Fruit and vegetables sector includes products with extremely different biological cycles, leading to a very unlike seasonality. Moreover, the Mediterranean area appears as a highly heterogeneous bloc, including countries which differ from the others for economic size, production potential, capability to export and for the relationships with the EU. The econometric estimation includes 68 analyses, 34 of which considering the European import and 34 the Italian import and the products are examined in their aggregated form and in their disaggregated level. The analysis obtains a very high R2 coefficient, which means that the methodology is able to assess the import effects on fruit and vegetables associated to the Association Agreements, preferential tariffs, regional integration, and others information involved in the equation. The empirical analysis suggests that fruits and vegetables trade flows are well explained by some parameters: size of the involved countries (especially GDP and population of the Mediterranean countries); distances; prices of imported products; local production for the aggregated products; preferential expressed tariffs like duty free; sub-regional agreements that enforce the export capability. The euro-mediterranean agreements are significant in some of the performed analysis, confirming the slow and gradual evolution of euro- Mediterranean liberalization. The euro-mediterranean liberalization provides opportunities from one side, and imposes a new important challenge from the other side. For the EU the chance is that fruit and vegetables imported from the mediterranean area represent a support for local supply and a possibility to increase the range of products existing on the market. The challenge regards the competition of foreign products with the local ones since the types of productions are similar and markets coincide, especially in the Italian issue. We need to apply a strategy based not on a trade antagonism, but on the realization of a common plane market with the Mediterranean countries. This goal could be achieved enhancing the industrial cooperation in addition to commercial relationships, and increasing investments’ flows in the Mediterranean countries aiming at transforming those countries from potential competitors to trade partners and creating new commercial policies to export towards extra European countries.

Insulin and TOR pathways regulate cellular and organismal growth through the myc oncogene in Drosophila

A large body of literature documents in both mice and Drosophila the involvement of Insulin pathway in growth regulation, probably due to its role in glucose and lipid import, nutrient storage, and translation of RNAs implicated in ribosome biogenesis (Vanhaesebroeck et al. 2001). Moreover several lines of evidence implicate this pathway as a causal factor in cancer (Sale, 2008; Zeng and Yee 2007; Hursting et al., 2007; Chan et al., 2008). With regards to Myc, studies in cell culture have implied this family of transcription factors as regulators of the cell cycle that are rapidly induced in response to growth factors. Myc is a potent oncogene, rearranged and overexpressed in a wide range of human tumors and necessary during development. Its conditional knock-out in mice results in reduction of body weight due to defect in cell proliferation (Trumpp et al. 2001). Evidence from in vivo studies in Drosophila and mammals suggests a critical function for myc in cell growth regulation (Iritani and Eisenman 1999; Johnston et al. 1999; Kim et al. 2000; de Alboran et al. 2001; Douglas et al. 2001). This role is supported by our analysis of Myc target genes in Drosophila, which include genes involved in RNA binding, processing, ribosome biogenesis and nucleolar function (Orain et al 2003, Bellosta et al., 2005, Hulf et al, 2005). The fact that Insulin signaling and Myc have both been associated with growth control suggests that they may interact with each other. However, genetic evidence suggesting that Insulin signaling regulates Myc in vivo is lacking. In this work we were able to show, for the first time, a direct modulation of dMyc in response to Insulin stimulation/silencing both in vitro and in vivo. Our results suggest that dMyc up-regulation in response to DILPs signaling occurs both at the mRNA and potein level. We believe dMyc protein accumulation after Insulin signaling activation is conditioned to AKT-dependent GSK3β/sgg inactivation. In fact, we were able to demonstate that dMyc protein stabilization through phosphorylation is a conserved feature between Drosophila and vertebrates and requires multiple events. The final phosphorylation step, that results in a non-stable form of dMyc protein, ready to be degraded by the proteasome, is performed by GSK3β/sgg kinase (Sears, 2004). At the same time we demonstrated that CKI family of protein kinase are required to prime dMyc phosphorylation. DILPs and TOR/Nutrient signalings are known to communicate at several levels (Neufeld, 2003). For this reason we further investigated TOR contribution to dMyc-dependent growth regulation. dMyc protein accumulates in S2 cells after aminoacid stimulation, while its mRNA does not seem to be affected upon TORC1 inhibition, suggesting that the Nutrient pathway regulates dMyc mostly post-transcriptionally. In support to this hypothesis, we observed a TORC1-dependent GSK3β/sgg inactivation, further confirming a synergic effect of DILPs and Nutrients on dMyc protein stability. On the other hand, our data show that Rheb but not S6K, both downstream of the TOR kinase, contributes to the dMyc-induced growth of the eye tissue, suggesting that Rheb controls growth independently of S6K.. Moreover, Rheb seems to be able to regulate organ size during development inducing cell death, a mechanism no longer occurring in absence of dmyc. These observations suggest that Rheb might control growth through a new pathway independent of TOR/S6K but still dependent on dMyc. In order to dissect the mechanism of dMyc regulation in response to these events, we analyzed the relative contribution of Rheb, TOR and S6K to dMyc expression, biochemically in S2 cells and in vivo in morphogenetic clones and we further confirmed an interplay between Rheb and Myc that seems to be indipendent from TOR. In this work we clarified the mechanisms that stabilize dMyc protein in vitro and in vivo and we observed for the first time dMyc responsiveness to DILPs and TOR. At the same time, we discovered a new branch of the Nutrient pathway that appears to drive growth through dMyc but indipendently from TOR. We believe our work shed light on the mechanisms cells use to grow or restrain growth in presence/absence of growth promoting cues and for this reason it contributes to understand the physiology of growth control.

Respiratory chain complex I dysfunction in tumorigenesis

Diseases due to mutations in mitochondrial DNA probably represent the most common form of metabolic disorders, including cancer, as highlighted in the last years. Approximately 300 mtDNA alterations have been identified as the genetic cause of mitochondrial diseases and one-third of these alterations are located in the coding genes for OXPHOS proteins. Despite progress in identification of their molecular mechanisms, little has been done with regard to the therapy. Recently, a particular gene therapy approach, namely allotopic expression, has been proposed and optimized, although the results obtained are rather controversial. In fact, this approach consists in synthesis of a wild-type version of mutated OXPHOS protein in the cytosolic compartment and in its import into mitochondria, but the available evidence is based only on the partial phenotype rescue and not on the demonstration of effective incorporation of the functional protein into respiratory complexes. In the present study, we took advantage of a previously analyzed cell model bearing the m.3571insC mutation in MTND1 gene for the ND1 subunit of respiratory chain complex I. This frame-shift mutation induces in fact translation of a truncated ND1 protein then degraded, causing complex I disassembly, and for this reason not in competition with that allotopically expressed. We show here that allotopic ND1 protein is correctly imported into mitochondria and incorporated in complex I, promoting its proper assembly and rescue of its function. This result allowed us to further confirm what we have previously demonstrated about the role of complex I in tumorigenesis process. Injection of the allotopic clone in nude mice showed indeed that the rescue of complex I assembly and function increases tumor growth, inducing stabilization of HIF1α, the master regulator of tumoral progression, and consequently its downstream gene expression activation.

Contributi della Geomatica nella salvaguardia e gestione dei Beni Culturali

Il territorio italiano presenta una grandissima ricchezza nel campo dei Beni Culturali, sia mobili che immobili; si tratta di un patrimonio di grande importanza che va gestito e tutelato nel migliore dei modi e con strumenti adeguati, anche in relazione ai problemi ad esso legati in termini di manutenzione e di salvaguardia dai fattori di rischio a cui può essere esposto. Per una buona conoscenza del Patrimonio Culturale, è fondamentale un’acquisizione preliminare di informazioni condotte in modo sistematico e unitario, che siano diffuse ed organiche, ma anche utili ad una valutazione preventiva e ad una successiva programmazione degli interventi di restauro di tipo conservativo. In questo ambito, l'impiego delle tecniche e tecnologie geomatiche nel campo dei Beni Culturali, può fornire un valido contributo, che va dalla catalogazione e documentazione del bene culturale al suo controllo e monitoraggio. Oggigiorno il crescente sviluppo di nuove tecnologie digitali, accompagnato dai notevoli passi avanti compiuti dalle discipline della geomatica (in primo luogo topografiche e fotogrammetriche), rende possibile una efficace integrazione tra varie tecniche, favorita anche dalla diffusione di soluzioni per l’interscambio dati e per la comunicazione tra differenti dispositivi. Lo studio oggetto della presente tesi si propone, di approfondire gli aspetti legati all’uso delle tecniche e tecnologie della Geomatica, per mettere in risalto le condizioni di un bene ed il suo stato di degrado. Per la gestione e la salvaguardia di un bene culturale , si presenta il SIT Carta del Rischio che evidenzia le pericolosità legate al patrimonio, e come esse sommate alla vulnerabilità di un singolo bene, contribuiscano all’individuazione del grado di rischio. di approfondire gli aspetti legati all’uso delle tecniche e tecnologie delle Geomatica, per mettere in risalto le condizioni di un bene ed il suo stato di degrado.

An architecture for scaling ontology networks

Constructing ontology networks typically occurs at design time at the hands of knowledge engineers who assemble their components statically. There are, however, use cases where ontology networks need to be assembled upon request and processed at runtime, without altering the stored ontologies and without tampering with one another. These are what we call "virtual [ontology] networks", and keeping track of how an ontology changes in each virtual network is called "multiplexing". Issues may arise from the connectivity of ontology networks. In many cases, simple flat import schemes will not work, because many ontology managers can cause property assertions to be erroneously interpreted as annotations and ignored by reasoners. Also, multiple virtual networks should optimize their cumulative memory footprint, and where they cannot, this should occur for very limited periods of time. We claim that these problems should be handled by the software that serves these ontology networks, rather than by ontology engineering methodologies. We propose a method that spreads multiple virtual networks across a 3-tier structure, and can reduce the amount of erroneously interpreted axioms, under certain raw statement distributions across the ontologies. We assumed OWL as the core language handled by semantic applications in the framework at hand, due to the greater availability of reasoners and rule engines. We also verified that, in common OWL ontology management software, OWL axiom interpretation occurs in the worst case scenario of pre-order visit. To measure the effectiveness and space-efficiency of our solution, a Java and RESTful implementation was produced within an Apache project. We verified that a 3-tier structure can accommodate reasonably complex ontology networks better, in terms of the expressivity OWL axiom interpretation, than flat-tree import schemes can. We measured both the memory overhead of the additional components we put on top of traditional ontology networks, and the framework's caching capabilities.