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.

Smile detection for user interfaces

[EN]Perceptual User Interfaces (PUIs) aim at facilitating human-computer interaction with the aid of human-like capacities (computer vision, speech recognition, etc.). In PUIs, the human face is a central element, since it conveys not only identity but also other important information, particularly with respect to the user’s mood or emotional state. This paper describes both a face detector and a smile detector for PUIs. Both are suitable for real-time interaction.

Mass spectrometry-based protein profiling strategies for biomarker discovery in liver and inflammatory bowel diseases

The study of protein expression profiles for biomarker discovery in serum and in mammalian cell populations needs the continuous improvement and combination of proteins/peptides separation techniques, mass spectrometry, statistical and bioinformatic approaches. In this thesis work two different mass spectrometry-based protein profiling strategies have been developed and applied to liver and inflammatory bowel diseases (IBDs) for the discovery of new biomarkers. The first of them, based on bulk solid-phase extraction combined with matrix-assisted laser desorption/ionization - Time of Flight mass spectrometry (MALDI-TOF MS) and chemometric analysis of serum samples, was applied to the study of serum protein expression profiles both in IBDs (Crohn’s disease and ulcerative colitis) and in liver diseases (cirrhosis, hepatocellular carcinoma, viral hepatitis). The approach allowed the enrichment of serum proteins/peptides due to the high interaction surface between analytes and solid phase and the high recovery due to the elution step performed directly on the MALDI-target plate. Furthermore the use of chemometric algorithm for the selection of the variables with higher discriminant power permitted to evaluate patterns of 20-30 proteins involved in the differentiation and classification of serum samples from healthy donors and diseased patients. These proteins profiles permit to discriminate among the pathologies with an optimum classification and prediction abilities. In particular in the study of inflammatory bowel diseases, after the analysis using C18 of 129 serum samples from healthy donors and Crohn’s disease, ulcerative colitis and inflammatory controls patients, a 90.7% of classification ability and a 72.9% prediction ability were obtained. In the study of liver diseases (hepatocellular carcinoma, viral hepatitis and cirrhosis) a 80.6% of prediction ability was achieved using IDA-Cu(II) as extraction procedure. The identification of the selected proteins by MALDITOF/ TOF MS analysis or by their selective enrichment followed by enzymatic digestion and MS/MS analysis may give useful information in order to identify new biomarkers involved in the diseases. The second mass spectrometry-based protein profiling strategy developed was based on a label-free liquid chromatography electrospray ionization quadrupole - time of flight differential analysis approach (LC ESI-QTOF MS), combined with targeted MS/MS analysis of only identified differences. The strategy was used for biomarker discovery in IBDs, and in particular of Crohn’s disease. The enriched serum peptidome and the subcellular fractions of intestinal epithelial cells (IECs) from healthy donors and Crohn’s disease patients were analysed. The combining of the low molecular weight serum proteins enrichment step and the LCMS approach allowed to evaluate a pattern of peptides derived from specific exoprotease activity in the coagulation and complement activation pathways. Among these peptides, particularly interesting was the discovery of clusters of peptides from fibrinopeptide A, Apolipoprotein E and A4, and complement C3 and C4. Further studies need to be performed to evaluate the specificity of these clusters and validate the results, in order to develop a rapid serum diagnostic test. The analysis by label-free LC ESI-QTOF MS differential analysis of the subcellular fractions of IECs from Crohn’s disease patients and healthy donors permitted to find many proteins that could be involved in the inflammation process. Among them heat shock protein 70, tryptase alpha-1 precursor and proteins whose upregulation can be explained by the increased activity of IECs in Crohn’s disease were identified. Follow-up studies for the validation of the results and the in-depth investigation of the inflammation pathways involved in the disease will be performed. Both the developed mass spectrometry-based protein profiling strategies have been proved to be useful tools for the discovery of disease biomarkers that need to be validated in further studies.

Development and optimization of graphic user interfaces (GUIs) for infrared spectrometers at the Telescopio Nazionale Galileo

This Phd thesis was entirely developed at the Telescopio Nazionale Galileo (TNG, Roque de los Muchachos, La Palma Canary Islands) with the aim of designing, developing and implementing a new Graphical User Interface (GUI) for the Near Infrared Camera Spectrometer (NICS) installed on the Nasmyth A of the telescope. The idea of a new GUI for NICS has risen for optimizing the astronomers work through a set of powerful tools not present in the existing GUI, such as the possibility to move automatically, an object on the slit or do a very preliminary images analysis and spectra extraction. The new GUI also provides a wide and versatile image display, an automatic procedure to find out the astronomical objects and a facility for the automatic image crosstalk correction. In order to test the overall correct functioning of the new GUI for NICS, and providing some information on the atmospheric extinction at the TNG site, two telluric standard stars have been spectroscopically observed within some engineering time, namely Hip031303 and Hip031567. The used NICS set-up is as follows: Large Field (0.25'' /pixel) mode, 0.5'' slit and spectral dispersion through the AMICI prism (R~100), and the higher resolution (R~1000) JH and HK grisms.

Security control brought back to the user

The activity of the Ph.D. student Juri Luca De Coi involved the research field of policy languages and can be divided in three parts. The first part of the Ph.D. work investigated the state of the art in policy languages, ending up with: (i) identifying the requirements up-to-date policy languages have to fulfill; (ii) defining a policy language able to fulfill such requirements (namely, the Protune policy language); and (iii) implementing an infrastructure able to enforce policies expressed in the Protune policy language. The second part of the Ph.D. work focused on simplifying the activity of defining policies and ended up with: (i) identifying a subset of the controlled natural language ACE to express Protune policies; (ii) implementing a mapping between ACE policies and Protune policies; and (iii) adapting the ACE Editor to guide users step by step when defining ACE policies. The third part of the Ph.D. work tested the feasibility of the chosen approach by applying it to meaningful real-world problems, among which: (i) development of a security layer on top of RDF stores; and (ii) efficient policy-aware access to metadata stores. The research activity has been performed in tight collaboration with the Leibniz Universität Hannover and further European partners within the projects REWERSE, TENCompetence and OKKAM.

Query rewriting in information retrieval: automatic context extraction from local user documents to improve query results

The central objective of research in Information Retrieval (IR) is to discover new techniques to retrieve relevant information in order to satisfy an Information Need. The Information Need is satisfied when relevant information can be provided to the user. In IR, relevance is a fundamental concept which has changed over time, from popular to personal, i.e., what was considered relevant before was information for the whole population, but what is considered relevant now is specific information for each user. Hence, there is a need to connect the behavior of the system to the condition of a particular person and his social context; thereby an interdisciplinary sector called Human-Centered Computing was born. For the modern search engine, the information extracted for the individual user is crucial. According to the Personalized Search (PS), two different techniques are necessary to personalize a search: contextualization (interconnected conditions that occur in an activity), and individualization (characteristics that distinguish an individual). This movement of focus to the individual's need undermines the rigid linearity of the classical model overtaken the ``berry picking'' model which explains that the terms change thanks to the informational feedback received from the search activity introducing the concept of evolution of search terms. The development of Information Foraging theory, which observed the correlations between animal foraging and human information foraging, also contributed to this transformation through attempts to optimize the cost-benefit ratio. This thesis arose from the need to satisfy human individuality when searching for information, and it develops a synergistic collaboration between the frontiers of technological innovation and the recent advances in IR. The search method developed exploits what is relevant for the user by changing radically the way in which an Information Need is expressed, because now it is expressed through the generation of the query and its own context. As a matter of fact the method was born under the pretense to improve the quality of search by rewriting the query based on the contexts automatically generated from a local knowledge base. Furthermore, the idea of optimizing each IR system has led to develop it as a middleware of interaction between the user and the IR system. Thereby the system has just two possible actions: rewriting the query, and reordering the result. Equivalent actions to the approach was described from the PS that generally exploits information derived from analysis of user behavior, while the proposed approach exploits knowledge provided by the user. The thesis went further to generate a novel method for an assessment procedure, according to the "Cranfield paradigm", in order to evaluate this type of IR systems. The results achieved are interesting considering both the effectiveness achieved and the innovative approach undertaken together with the several applications inspired using a local knowledge base.

Expression profiling in developing peach seed and mesocarp as affected by growth regulators

Jasmonates (JAs) and spermidine (Sd) influence fruit (and seed) development and ripening. In order to unravel their effects in peach fruit, at molecular level, field applications of methyl jasmonate (MJ) and propyl dihydrojasmonate (PDJ), and Sd were performed at an early developmental stage (late S1). At commercial harvest, JA-treated fruit were less ripe than controls. Realtime RT-PCR analyses confirmed a down-regulation of ethylene biosynthetic, perception and signaling genes, and flesh softening-related genes. The expression of cell wall-related genes, of a sugar-transporter and hormone-related transcript levels was also affected by JAs. Seeds from JA-treated fruit showed a shift in the expression of developmental marker genes suggesting that the developmental program was probably slowed down, in agreement with the contention that JAs divert resources from growth to defense. JAs also affected phenolic content and biosynthetic gene expression in the mesocarp. Levels of hydroxycinnamic acids, as well as those of flavan-3-ols, were enhanced, mainly by MJ, in S2. Transcript levels of phenylpropanoid pathway genes were up-regulated by MJ, in agreement with phenolic content. Sd-treated fruits at harvest showed reduced ethylene production and flesh softening. Sd induced a short-term and long-term response patterns in endogenous polyamines. At ripening the up-regulation of the ethylene biosynthetic genes was dramatically counteracted by Sd, leading to a down-regulation of softening-related genes. Hormone-related gene expression was also altered both in the short- and long-term. Gene expression analyses suggest that Sd interfered with fruit development/ripening by interacting with multiple hormonal pathways and that fruit developmental marker gene expression was shifted ahead in accord with a developmental slowing down. 24-Epibrassinolide was applied to Flaminia peaches under field conditions early (S1) or later (S3) during development. Preliminary results showed that, at harvest, treated fruit tended to be larger and less mature though quality parameters did not change relative to controls.

Enabling a direct path from end-user specifications to executable protocols in a biology laboratory environment

Biomedical analyses are becoming increasingly complex, with respect to both the type of the data to be produced and the procedures to be executed. This trend is expected to continue in the future. The development of information and protocol management systems that can sustain this challenge is therefore becoming an essential enabling factor for all actors in the field. The use of custom-built solutions that require the biology domain expert to acquire or procure software engineering expertise in the development of the laboratory infrastructure is not fully satisfactory because it incurs undesirable mutual knowledge dependencies between the two camps. We propose instead an infrastructure concept that enables the domain experts to express laboratory protocols using proper domain knowledge, free from the incidence and mediation of the software implementation artefacts. In the system that we propose this is made possible by basing the modelling language on an authoritative domain specific ontology and then using modern model-driven architecture technology to transform the user models in software artefacts ready for execution in a multi-agent based execution platform specialized for biomedical laboratories.

Expression profiling und rationale Expressionsoptimierung am Beispiel eines prokaryontischen Wirt-,Vektor-Systems

Durch globale Expressionsprofil-Analysen auf Transkriptom-, Proteom- oder Metabolom-Ebene können biotechnologische Produktionsprozesse besser verstanden und die Erkenntnisse für die zielgerichtete, rationale Optimierung von Expressionssystemen genutzt werden. In der vorliegenden Arbeit wurde die Überexpression einer Glukose-Dehydrogenase (EC 1.1.5.2), die von der Roche Diagnostics GmbH für die diagnostische Anwendung optimiert worden war, in Escherichia coli untersucht. Die Enzymvariante unterscheidet sich in sieben ihrer 455 Aminosäuren vom Wildtyp-Enzym und wird im sonst isogenen Wirt-/Vektor-System in signifikant geringeren Mengen (Faktor 5) gebildet. Das prokaryontische Expressionssystem wurde auf Proteom-Ebene charakterisiert. Die 2-dimensionale differenzielle Gelelektrophorese (DIGE) wurde zuvor unter statistischen Aspekten untersucht. Unter Berücksichtigung von technischen und biologischen Variationen, falsch-positiven (α-) und falsch-negativen (β-) Fehlern sowie einem daraus abgeleiteten Versuchsdesign konnten Expressionsunterschiede als signifikant quantifiziert werden, wenn sie um den Faktor ≥ 1,4 differierten. Durch eine Hauptkomponenten-Analyse wurde gezeigt, dass die DIGE-Technologie für die Expressionsprofil-Analyse des Modellsystems geeignet ist. Der Expressionsstamm für die Enzymvariante zeichnete sich durch eine höhere Variabilität an Enzymen für den Zuckerabbau und die Nukleinsäure-Synthese aus. Im Expressionssystem für das Wildtyp-Enzym wurde eine unerwartet erhöhte Plasmidkopienzahl nachgewiesen. Als potenzieller Engpass in der Expression der rekombinanten Glukose-Dehydrogenase wurde die Löslichkeitsvermittlung identifiziert. Im Expressionsstamm für das Wildtyp-Enzym wurden viele Proteine für die Biogenese der äußeren Membran verstärkt exprimiert. Als Folge dessen wurde ein sog. envelope stress ausgelöst und die Zellen gingen in die stationäre Wuchsphase über. Die Ergebnisse der Proteomanalyse wurden weiterführend dazu genutzt, die Produktionsleistung für die Enzymvariante zu verbessern. Durch den Austausch des Replikationsursprungs im Expressionsvektor wurde die Plasmidkopienzahl erhöht und die zelluläre Expressionsleistung für die diagnostisch interessantere Enzymvariante um Faktor 7 - 9 gesteigert. Um die Löslichkeitsvermittlung während der Expression zu verbessern, wurde die Plasmidkopienzahl gesenkt und die Coexpression von Chaperonen initiiert. Die Ausbeuten aktiver Glukose-Dehydrogenase wurden durch die Renaturierung inaktiven Produkts aus dem optimierten Expressionssystem insgesamt um einen Faktor von 4,5 erhöht. Somit führte im Rahmen dieser Arbeit eine proteombasierte Expressionsprofil-Analyse zur zielgerichteten, rationalen Expressionsoptimierung eines prokaryontischen Modellsystems.

Profiling, re-factoring e ottimizzazione del middleware di coordinazione TuCSoN

In questo lavoro di tesi vengono esaminate quelle caratteristiche architetturali del middleware di coordinazione TuCSoN che maggiormente impattano sulle prestazioni dei sistemi coordinati. Laddove è stato possibile si è intervenuto sia a livello architetturale sia a livello tecnologico per migliorare le prestazioni del middleware. Come risultato finale si è ottenuto un importante incremento delle prestazioni del sistema. Non tutte le migliorie apportabili sono state realizzate, tuttavia vengono forniti alcuni spunti per possibili sviluppi futuri.

Kinect e openNI a supporto delle NUI (Natural User Interface) applications.

Descrizione delle Natural User Interface e del framework OpenNI 2.0 compreso di caso applicativo.

MicroRNA profiling nei linfomi a cellule T periferiche

I linfomi a cellule T periferiche rappresentano circa il 12% di tutte le neoplasie linfoidi.In questo studio, abbiamo effettuato un’analisi di miRNA profiling (TaqMan Array MicroRNA Cards A) su 60 campioni FFPE suddivisi in: PTCLs/NOS (N=25), AITLs (N=10), ALCLs (N=12) e cellule T normali (N=13). Abbiamo identificato 4 miRNA differenzialmente espressi tra PTCLs e cellule T normali. Inoltre, abbiamo identificato tre set di mirna che discriminano le tre entita di PTCLs nodali

User testing and analysis di interfacce web e mobile per un merge di sistemi

Testing e Analisi di problemi di usabilità che potrebbero sorgere se due sistemi venissero integrati in un unico nuovo sistema.