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.

Liquid crystal polymers: macromolecular design for enhanced performances

During this work, done mainly in the laboratories of the department of Industrial Chemistry and Materials of the University of Bologna but also in the laboratories of the Carnegie Mellon University in collaboration with prof. K. Matyjaszewski and at the university of Zaragoza in collaboration with prof. J. Barberá, was focused mainly on the synthesis and characterization of new functional polymeric materials. In the past years our group gained a deep knowledge about the photomodulation of azobenzene containing polymers. The aim of this thesis is to push forward the performances of these materials by the synthesis of well defined materials, in which, by a precise control over the macromolecular structures, better or even new functionality can be delivered to the synthesized material. For this purpose, besides the rich photochemistry of azoaromatic polymers that brings to the application, the control offered from the recent techniques of controlled radical polymerization, ATRP over all, gives an enormous range of opportunity for the developing of a new generation of functional materials whose properties are determinate not only by the chemical nature of the functional center (e.g. azoaromatic chromophore) but are tuned and even amplified by a synergy with the whole macromolecular structure. Old materials in new structures. In this contest the work of this thesis was focused mainly on the synthesis and characterization of well defined azoaromatic polymers in order to establish, for the first time, precise structure-properties correlation. In fact a series of well defined different azopolymers, chiral and achiral, with different molecular weight and highly monodisperse were synthesized and their properties were studied, in terms of photoexpansion and photomodulation of chirality. We were then able to study the influence of the macromolecular structure in terms of molecular weight and ramification on the studied properties. The huge amount of possibility offered by the tailoring of the macromolecular structure were exploited for the synthesis of new cholesteric photochromic polymers that can be used as a smart label for the certification of the thermal history of any thermosensitive product. Finally the ATRP synthesis allowed us to synthesize a total new class of material, named molecular brushes: a flat surface covered with an ultra thin layer of polymeric chain covalently bond onto the surface from one end. This new class of materials is of extreme interest as they offer the possibility to tune and manage the interaction of the surface with the environment. In this contest we synthesized both azoaromatic surfaces, growing directly the polymer from the surface, and mixed brushes: surfaces covered with incompatible macromolecules. Both type of surfaces acts as “smart” surfaces: the first it is able to move the orientation of a LC cell by simply photomodulation and, thanks to the robustness of the covalent bond, can be used as a command surface overcoming all the limitation due to the dewetting of the active layer. The second type of surface, functionalized by a grafting-to method, can self assemble the topmost layer responding to changed environmental conditions, exposing different functionality according to different environment.

The Enhanced Single-dish Control System and wide surveys of compact sources

The Italian radio telescopes currently undergo a major upgrade period in response to the growing demand for deep radio observations, such as surveys on large sky areas or observations of vast samples of compact radio sources. The optimised employment of the Italian antennas, at first constructed mainly for VLBI activities and provided with a control system (FS – Field System) not tailored to single-dish observations, required important modifications in particular of the guiding software and data acquisition system. The production of a completely new control system called ESCS (Enhanced Single-dish Control System) for the Medicina dish started in 2007, in synergy with the software development for the forthcoming Sardinia Radio Telescope (SRT). The aim is to produce a system optimised for single-dish observations in continuum, spectrometry and polarimetry. ESCS is also planned to be installed at the Noto site. A substantial part of this thesis work consisted in designing and developing subsystems within ESCS, in order to provide this software with tools to carry out large maps, spanning from the implementation of On-The-Fly fast scans (following both conventional and innovative observing strategies) to the production of single-dish standard output files and the realisation of tools for the quick-look of the acquired data. The test period coincided with the commissioning phase for two devices temporarily installed – while waiting for the SRT to be completed – on the Medicina antenna: a 18-26 GHz 7-feed receiver and the 14-channel analogue backend developed for its use. It is worth stressing that it is the only K-band multi-feed receiver at present available worldwide. The commissioning of the overall hardware/software system constituted a considerable section of the thesis work. Tests were led in order to verify the system stability and its capabilities, down to sensitivity levels which had never been reached in Medicina using the previous observing techniques and hardware devices. The aim was also to assess the scientific potential of the multi-feed receiver for the production of wide maps, exploiting its temporary availability on a mid-sized antenna. Dishes like the 32-m antennas at Medicina and Noto, in fact, offer the best conditions for large-area surveys, especially at high frequencies, as they provide a suited compromise between sufficiently large beam sizes to cover quickly large areas of the sky (typical of small-sized telescopes) and sensitivity (typical of large-sized telescopes). The KNoWS (K-band Northern Wide Survey) project is aimed at the realisation of a full-northern-sky survey at 21 GHz; its pilot observations, performed using the new ESCS tools and a peculiar observing strategy, constituted an ideal test-bed for ESCS itself and for the multi-feed/backend system. The KNoWS group, which I am part of, supported the commissioning activities also providing map-making and source-extraction tools, in order to complete the necessary data reduction pipeline and assess the general system scientific capabilities. The K-band observations, which were carried out in several sessions along the December 2008-March 2010 period, were accompanied by the realisation of a 5 GHz test survey during the summertime, which is not suitable for high-frequency observations. This activity was conceived in order to check the new analogue backend separately from the multi-feed receiver, and to simultaneously produce original scientific data (the 6-cm Medicina Survey, 6MS, a polar cap survey to complete PMN-GB6 and provide an all-sky coverage at 5 GHz).

L'Occidente di Elisée Reclus: l'invenzione dell'Europa nella Nouvelle Géographie Universelle (1876-1894)

La Nouvelle Géographie Universelle di Élisée Reclus relativizza e problematizza il ruolo dell’Europa e il suo peso nello scacchiere mondiale, restando tuttavia in equilibrio fra, da una parte, la critica delle pratiche coloniali e dall’altra la fiducia nei confronti della tradizione culturale proveniente dall’antica Grecia e dal secolo de Lumi destinata, nella visione evoluzionista dell’autore, a spargere negli altri continenti i germi del pensiero socialista e anarchico. In questo lavoro si cerca di chiarire questa rappresentazione dei concetti di Europa e Occidente in tre passaggi successivi. Dapprima, la ricostruzione della genealogia, della teoria e del contesto storico del concetto di geografia universale all’epoca. Poi, la ricostruzione dalle fonti di archivio delle reti scientifiche di respiro europeo che sono state alla base di quest’opera, indispensabile per poterne comprendere il significato politico nel contesto dell’epoca. Infine, l’indagine sul testo per ricostruire ruolo, caratteri e suddivisione dell’Europa, che si rivela, nonostante la serrata critica del suo ruolo colonizzatore, come il privilegiato laboratorio individuato dai “geografi anarchici” per lo sviluppo delle lotte sociali e per la costruzione, su basi anche geografiche, di una proposta politica federalista e libertaria.

Development of advanced tools and methods for the assessment and management of risk due to atypical major accident scenarios

Proper hazard identification has become progressively more difficult to achieve, as witnessed by several major accidents that took place in Europe, such as the Ammonium Nitrate explosion at Toulouse (2001) and the vapour cloud explosion at Buncefield (2005), whose accident scenarios were not considered by their site safety case. Furthermore, the rapid renewal in the industrial technology has brought about the need to upgrade hazard identification methodologies. Accident scenarios of emerging technologies, which are not still properly identified, may remain unidentified until they take place for the first time. The consideration of atypical scenarios deviating from normal expectations of unwanted events or worst case reference scenarios is thus extremely challenging. A specific method named Dynamic Procedure for Atypical Scenarios Identification (DyPASI) was developed as a complementary tool to bow-tie identification techniques. The main aim of the methodology is to provide an easier but comprehensive hazard identification of the industrial process analysed, by systematizing information from early signals of risk related to past events, near misses and inherent studies. DyPASI was validated on the two examples of new and emerging technologies: Liquefied Natural Gas regasification and Carbon Capture and Storage. The study broadened the knowledge on the related emerging risks and, at the same time, demonstrated that DyPASI is a valuable tool to obtain a complete and updated overview of potential hazards. Moreover, in order to tackle underlying accident causes of atypical events, three methods for the development of early warning indicators were assessed: the Resilience-based Early Warning Indicator (REWI) method, the Dual Assurance method and the Emerging Risk Key Performance Indicator method. REWI was found to be the most complementary and effective of the three, demonstrating that its synergy with DyPASI would be an adequate strategy to improve hazard identification methodologies towards the capture of atypical accident scenarios.

Il filo di Arianna - Una ricerca multi ed interdisciplinare per il superamento degli handicap che la x fragile propone

Il seguente lavoro di tesi verte sulla ricerca-azione formazione triennale “Il Filo di Arianna” realizzata in convenzione tra Associazione Italiana Sindrome X Fragile e Dipartimento Di Scienze dell’Educazione – Università di Bologna, finalizzata alla superamento degli handicap che la X fragile propone. La ricerca ha un fuoco in Pedagogia Speciale e un carattere multidisciplinare e inter istituzionale grazie alla sinergia con l’area neuroriabilitativa (Istituto di Ricovero e Cura a Carattere Scientifico (IRCCS) San Raffaele Pisana di Roma) e l’area della Psicologia Clinica (Ospedale Bambin Gesù di Roma). Il lavoro di tesi descrive il percorso per giungere alle linee guida di intervento scaturite dalla ricerca, per il potenziamento cognitivo ed affettivo di bambini e persone con x fragile nei contesti di casa, scuola e tempo libero.

The European External Action Service and the Implementation of the 'Union Method' in European Foreign Policy

The European External Action Service (EEAS or Service) is one of the most significant and most debated innovations introduced by the Lisbon Treaty. This analysis intends to explain the anomalous design of the EEAS in light of its function, which consists in the promotion of external action coherence. Coherence is a principle of the EU legal system, which requires synergy in the external actions of the Union and its Members. It can be enforced only through the coordination of European policy-makers' initiatives, by bridging the gap between the 'Communitarian' and intergovernmental approaches. This is the 'Union method' envisaged by A. Merkel: "coordinated action in a spirit of solidarity - each of us in the area for which we are responsible but all working towards the same goal". The EEAS embodies the 'Union method', since it is institutionally linked to both Union organs and Member States. It is also capable of enhancing synergy in policy management and promoting unity in international representation, since its field of action is delimited not by an abstract concern for institutional balance but by a pragmatic assessment of the need for coordination in each sector. The challenge is now to make sure that this pragmatic approach is applied with respect to all the activities of the Service, in order to reinforce its effectiveness. The coordination brought by the EEAS is in fact the only means through which a European foreign policy can come into being: the choice is not between the Community method and the intergovernmental method, but between a coordinated position and nothing at all.

La terapia combinata di cellule mesenchimali stromali e aceinibitori riduce la fibrosi renale in un modello animale di ostruzione ureterale unilaterale

Le cellule mesenchimali stromali (MSC) sono cellule multipotenti e numerosi studi hanno mostrato i loro effetti benefici nel danno renale acuto ma non sono ancora stati dimostrati potenziali effetti nella malattia renale cronica. L'ostruzione ureterale unilaterale (UUO) è un modello di fibrosi interstiziale nel quale l'attivazione di molecole vasoattive, citochine profibrotiche e infiammatorie gioca un ruolo patogenetico nello sviluppo dell'apoptosi e atrofia tubulare. Il sistema renina-angiotensina (RAS) gioca un ruolo chiave nello sviluppo della fibrosi renale e i farmaci che hanno come target l'angiotensina II, principale mediatore del RAS, sono attualmente la terapia più efficace nel ridurre la progressione della malattia renale cronica. E' noto che gli ACE-inibitori (ACEi) inducono un aumento compensatorio della renina plasmatica per la mancaza del feedback negativo sulla sua produzione. Tuttavia, la renina (R) promuove il danno renale non solo stimolando la produzione di ANGII, ma anche up-regolando geni profibrotici attraverso l'attivazione del recettore renina/prorenina. Lo scopo dello studio è stato indagare se l'infusione di MSC riduceva il danno renalein un modello animale di UUO e comparare gli eventuali effetti protettivi di ACEi e MSC in UUO. Abbiamo studiato 5 gruppi di ratti. A: sham operati. B: ratti sottoposti a UUO che ricevevano soluzione salina. C: ratti sottoposti a UUO che ricevavano MSC 3X106 nella vena della coda al giorno 0. D:ratti sottoposti a UUO che ricevevano lisinopril dal g 1 al g 21. E: ratti sottoposti a UUO che ricevevano MSC 3X106 nella vena della coda al giorno 0 e lisinopril dal g 1 al g 21. I ratti sono stati sacrificati al giorno 7 e 21. I risultati dello studio mostrano che MSC in UUO prevengono l'aumento della renina, riducono la generazione di ANGII e che in terapia combinata con ACEi riducono ulteriormente l'ANGII, determinando una sinergia nel miglioramento della fibrosi renale.

Cell death mechanisms triggered by monoclonal antibodies against CD99 in Ewing sarcoma: Cross-talk between MDM2, IGF-1R and Ras/MAPK

CD99 is a 32 kDa transmembrane protein whose high expression characterizes Ewing sarcoma (ES), a very aggressive pediatric bone tumor. In addition to its diagnostic value, CD99 has therapeutic potential since it leads to rapid and massive ES cell death when engaged with specific antibodies. Here a novel mechanism of cell death triggered via CD99 is shown, leading, ultimately, to the appearance of macropinocytotic vescicles. Anti-CD99 mAb 0662 induces MDM2 ubiquitination and degradation, which causes not only a p53 reactivation but also the IGF-1R induction and its subsequent internalization; CD99 results internalized together with IGF-1R inside endosomes, but then the two molecules display a different sorting: CD99 is degraded, while IGF-1R is recycled on the surface, causing, as a final step, the up-regulation of RAS-MAPK. High-expressing CD99 mesenchymal stem cells show mild Ras induction but no p53 activation and escape cell death, but in presence of EWS/FLI1 mesenchymal stem cells expressing CD99 show a stronger Ras induction and a p53 reactivation, leading to a significant cell death rate. We propose that CD99 triggering in a EWS/FLI1-driven oncogenetic context creates a synergy between RAS upregulation and p53 activation in ES cells, leading to cell death. Moreover, our data rule out possible concerns on toxicity related to the broad CD99 expression in normal tissues and provide the rationale for the therapeutic use of anti-CD99 MAbs in the clinic.

Portfolio Approaches in Constraint Programming

Recent research has shown that the performance of a single, arbitrarily efficient algorithm can be significantly outperformed by using a portfolio of —possibly on-average slower— algorithms. Within the Constraint Programming (CP) context, a portfolio solver can be seen as a particular constraint solver that exploits the synergy between the constituent solvers of its portfolio for predicting which is (or which are) the best solver(s) to run for solving a new, unseen instance. In this thesis we examine the benefits of portfolio solvers in CP. Despite portfolio approaches have been extensively studied for Boolean Satisfiability (SAT) problems, in the more general CP field these techniques have been only marginally studied and used. We conducted this work through the investigation, the analysis and the construction of several portfolio approaches for solving both satisfaction and optimization problems. We focused in particular on sequential approaches, i.e., single-threaded portfolio solvers always running on the same core. We started from a first empirical evaluation on portfolio approaches for solving Constraint Satisfaction Problems (CSPs), and then we improved on it by introducing new data, solvers, features, algorithms, and tools. Afterwards, we addressed the more general Constraint Optimization Problems (COPs) by implementing and testing a number of models for dealing with COP portfolio solvers. Finally, we have come full circle by developing sunny-cp: a sequential CP portfolio solver that turned out to be competitive also in the MiniZinc Challenge, the reference competition for CP solvers.

Processi integrati per l’intensificazione di processo: reazione di fotocatalisi accoppiata alla pervaporazione, la dialisi e all’ozonizzazione

L’accoppiamento di diverse operazioni unitarie può in certi casi portare ad una cosiddetta “intensificazione di processo”, cioè ad un aumento sostanziale delle rese, dell’efficienza e della sostenibilità. Nel presente lavoro sono state pertanto analizzate le potenzialità di accoppiamento della fotocatalisi, il più studiato tra i “processi di ossidazione avanzata”, sia con alcuni processi a membrana per la sintesi verde di aromi sia con l’ozonizzazione per la depurazione di acque. È stato dimostrato che in entrambi i casi l’ottenimento di una significativa intensificazione di processo dipende in gran parte dai parametri operativi, in particolare dal rapporto, delta, tra la velocità caratteristica di fotocatalisi e quella del processo accoppiato. Nel caso della sintesi di aromi, in cui la fotocatalisi viene accoppiata con la pervaporazione o con la dialisi ricircolando al reattore il retentato dalla cella con la membrana. Il parametro delta dipende dalla velocità di reazione, dalle proprietà di trasporto delle membrane e naturalmente dal volume del rettore e dall’area della membrana. La reazione fotocatalitica produce l’aroma, ad esempio vanillina da acido ferulico, per ossidazione parziale e grazie al recupero del prodotto se ne evita l’ulteriore ossidazione aumentandone pertanto la resa. L’operare in apparati separati offre diversi vantaggi come la possibilità di variare senza vincoli il rapporto tra area della membrana e volume del reattore, ma impone di considerare anche il grado effettivo di accoppiamento dei processi. In questo caso, come evidenziato dal modello matematico, un sufficientemente elevato rapporto di ricircolo consente comunque di integrare efficacemente i processi. Nell’ozonizzazione fotocatalitica si hanno due importanti vantaggi: l’aumento della velocità di degradazione grazie alla sinergia tra i processi e la capacità di controllare la formazione di prodotti pericolosi. La sinergia viene massimizzata ad un valore ottimale di delta, mentre la formazione dei prodotti indesiderati viene controllata operando secondo le procedure che sono state individuate.

La promozione dell'inclusione nei sistemi scolastici attraverso l'intervento di cooperazione internazionale: l'esperienza di El Salvador

La ricerca si colloca all’interno di un complesso intervento di cooperazione internazionale realizzato in El Salvador tra il 2009 e il 2014. Il Progetto di cooperazione è stato promosso dal Dipartimento di Scienze dell’Educazione dell’Università di Bologna e finanziato dalla Cooperazione Italiana. L’esperienza studiata rappresenta un esempio di promozione dell’inclusione nei sistemi scolastici di Paesi del Sud del mondo e si propone due obiettivi: 1) analizzare il processo di cambiamento della prospettiva di intervento promossa dalla cooperazione internazionale, evidenziando la dimensione educativa che sostiene processi di empowerment e ownership delle istituzioni locali; 2) contribuire al dibattito sull’ “inclusive education”, sostenendo processi di inclusione scolastica e sociale rivolti a tutti coloro che si trovano in situazione di svantaggio psico-fisico e/o socio-culturale. Le politiche locali del Ministero dell’Educazione dal 2009 hanno promosso un modello educativo con l’obiettivo di garantire il diritto all’educazione per tutti nella scuola pubblica. Lo studio costituisce un'indagine di tipo valutativo sul processo di sviluppo della scuola inclusiva in El Salvador, supportato dall’intervento di cooperazione internazionale. La ricerca utilizza in modo integrato strumenti di natura quantitativa (questionari) e qualitativa (interviste). Dai dati raccolti emerge come il processo di cooperazione sia stato caratterizzato dal principio della pari dignità tra esperti internazionali e autorità politiche e tecniche locali. Inoltre, la ricerca ha consentito di verificare come la cultura dell'inclusione si sia radicata in modo diffuso nella percezione della missione della scuola e il suo ruolo tra i protagonisti del sistema scolastico. Alla luce dei risultati, appare fondamentale continuare a investire sulla formazione tecnica delle figure chiave del sistema educativo; facilitare il processo di inclusione dei disabili nelle scuole regolari con una parallela trasformazione delle scuole speciali in centri di supporto all’integrazione; promuovere una sinergia di azione formativa tra il ministero, mondo accademico e della formazione professionale.

Meccanizzazione dei vigneti allevati a doppia cortina e a cordone libero

La ricerca svolta ha voluto approfondire le possibilità offerte dai sistemi di allevamento dei vigneti a Doppia Cortina (GDC) e a Cordone Libero nei riguardi della meccanizzazione. La ricerca ha considerato gli interventi di potatura invernale, di gestione della chioma (spollonatura, cimatura, defogliazione e pettinatura della doppia cortina) e di vendemmia. Un’operazione particolarmente seguita è stata la potatura invernale realizzando differenti livelli di meccanizzazione. Tutti gli interventi sono stati eseguiti sia manualmente che meccanicamente, confrontando i tempi d’impiego, la qualità del lavoro svolto e gli impegni di manodopera. I risultati sono stati sintetizzati in una valutazione economica, ipotizzando differenti livelli di costo della manodopera impiegata, per ottenere giudizi di convenienza per i singoli interventi e per costruire una valutazione completa e più organica della linea di lavoro proposta. Nelle due forme d’allevamento la meccanizzazione della potatura invernale e della gestione della chioma hanno rispettato pienamente gli obbiettivi tecnici prefissati, dimostrando di essere un valido mezzo per ridurre tempi e costi di gestione. Per questi interventi l’acquisto delle macchine risulta conveniente anche per vigneti di piccola dimensione. Ancor più evidenti in queste due forme d’allevamento sono i vantaggi economici offerti dalla vendemmia meccanica, realizzata con pochi maltrattamenti e perdite di prodotto. La tendenza a meccanizzare integralmente gli interventi di gestione del ciclo colturale della vite, può essere nei prossimi anni un motivo di interesse e di scelta nella realizzazione di nuovi impianti con queste due forme di allevamento, che hanno dimostrato di essere un’espressione completa di sinergia tra macchina e pianta.