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.

Tools and methods for the quality assurance of force platforms in human movement analysis

The human movement analysis (HMA) aims to measure the abilities of a subject to stand or to walk. In the field of HMA, tests are daily performed in research laboratories, hospitals and clinics, aiming to diagnose a disease, distinguish between disease entities, monitor the progress of a treatment and predict the outcome of an intervention [Brand and Crowninshield, 1981; Brand, 1987; Baker, 2006]. To achieve these purposes, clinicians and researchers use measurement devices, like force platforms, stereophotogrammetric systems, accelerometers, baropodometric insoles, etc. This thesis focus on the force platform (FP) and in particular on the quality assessment of the FP data. The principal objective of our work was the design and the experimental validation of a portable system for the in situ calibration of FPs. The thesis is structured as follows: Chapter 1. Description of the physical principles used for the functioning of a FP: how these principles are used to create force transducers, such as strain gauges and piezoelectrics transducers. Then, description of the two category of FPs, three- and six-component, the signals acquisition (hardware structure), and the signals calibration. Finally, a brief description of the use of FPs in HMA, for balance or gait analysis. Chapter 2. Description of the inverse dynamics, the most common method used in the field of HMA. This method uses the signals measured by a FP to estimate kinetic quantities, such as joint forces and moments. The measures of these variables can not be taken directly, unless very invasive techniques; consequently these variables can only be estimated using indirect techniques, as the inverse dynamics. Finally, a brief description of the sources of error, present in the gait analysis. Chapter 3. State of the art in the FP calibration. The selected literature is divided in sections, each section describes: systems for the periodic control of the FP accuracy; systems for the error reduction in the FP signals; systems and procedures for the construction of a FP. In particular is detailed described a calibration system designed by our group, based on the theoretical method proposed by ?. This system was the “starting point” for the new system presented in this thesis. Chapter 4. Description of the new system, divided in its parts: 1) the algorithm; 2) the device; and 3) the calibration procedure, for the correct performing of the calibration process. The algorithm characteristics were optimized by a simulation approach, the results are here presented. In addiction, the different versions of the device are described. Chapter 5. Experimental validation of the new system, achieved by testing it on 4 commercial FPs. The effectiveness of the calibration was verified by measuring, before and after calibration, the accuracy of the FPs in measuring the center of pressure of an applied force. The new system can estimate local and global calibration matrices; by local and global calibration matrices, the non–linearity of the FPs was quantified and locally compensated. Further, a non–linear calibration is proposed. This calibration compensates the non– linear effect in the FP functioning, due to the bending of its upper plate. The experimental results are presented. Chapter 6. Influence of the FP calibration on the estimation of kinetic quantities, with the inverse dynamics approach. Chapter 7. The conclusions of this thesis are presented: need of a calibration of FPs and consequential enhancement in the kinetic data quality. Appendix: Calibration of the LC used in the presented system. Different calibration set–up of a 3D force transducer are presented, and is proposed the optimal set–up, with particular attention to the compensation of non–linearities. The optimal set–up is verified by experimental results.

Studies of OPA1 pathogenic mechanisms in Dominant Optic Atrophy and novel protein function in mitochondrial DNA stability

The mitochondrion is an essential cytoplasmic organelle that provides most of the energy necessary for eukaryotic cell physiology. Mitochondrial structure and functions are maintained by proteins of both mitochondrial and nuclear origin. These organelles are organized in an extended network that dynamically fuses and divides. Mitochondrial morphology results from the equilibrium between fusion and fission processes, controlled by a family of “mitochondria-shaping” proteins. It is becoming clear that defects in mitochondrial dynamics can impair mitochondrial respiration, morphology and motility, leading to apoptotic cell death in vitro and more or less severe neurodegenerative disorders in vivo in humans. Mutations in OPA1, a nuclear encoded mitochondrial protein, cause autosomal Dominant Optic Atrophy (DOA), a heterogeneous blinding disease characterized by retinal ganglion cell degeneration leading to optic neuropathy (Delettre et al., 2000; Alexander et al., 2000). OPA1 is a mitochondrial dynamin-related guanosine triphosphatase (GTPase) protein involved in mitochondrial network dynamics, cytochrome c storage and apoptosis. This protein is anchored or associated on the inner mitochondrial membrane facing the intermembrane space. Eight OPA1 isoforms resulting from alternative splicing combinations of exon 4, 4b and 5b have been described (Delettre et al., 2001). These variants greatly vary among diverse organs and the presence of specific isoforms has been associated with various mitochondrial functions. The different spliced exons encode domains included in the amino-terminal region and contribute to determine OPA1 functions (Olichon et al., 2006). It has been shown that exon 4, that is conserved throughout evolution, confers functions to OPA1 involved in maintenance of the mitochondrial membrane potential and in the fusion of the network. Conversely, exon 4b and exon 5b, which are vertebrate specific, are involved in regulation of cytochrome c release from mitochondria, and activation of apoptosis, a process restricted to vertebrates (Olichon et al., 2007). While Mgm1p has been identified thanks to its role in mtDNA maintenance, it is only recently that OPA1 has been linked to mtDNA stability. Missense mutations in OPA1 cause accumulation of multiple deletions in skeletal muscle. The syndrome associated to these mutations (DOA-1 plus) is complex, consisting of a combination of dominant optic atrophy, progressive external ophtalmoplegia, peripheral neuropathy, ataxia and deafness (Amati- Bonneau et al., 2008; Hudson et al., 2008). OPA1 is the fifth gene associated with mtDNA “breakage syndrome” together with ANT1, PolG1-2 and TYMP (Spinazzola et al., 2009). In this thesis we show for the first time that specific OPA1 isoforms associated to exon 4b are important for mtDNA stability, by anchoring the nucleoids to the inner mitochondrial membrane. Our results clearly demonstrate that OPA1 isoforms including exon 4b are intimately associated to the maintenance of the mitochondrial genome, as their silencing leads to mtDNA depletion. The mechanism leading to mtDNA loss is associated with replication inhibition in cells where exon 4b containing isoforms were down-regulated. Furthermore silencing of exon 4b associated isoforms is responsible for alteration in mtDNA-nucleoids distribution in the mitochondrial network. In this study it was evidenced that OPA1 exon 4b isoform is cleaved to provide a 10kd peptide embedded in the inner membrane by a second transmembrane domain, that seems to be crucial for mitochondrial genome maintenance and does correspond to the second transmembrane domain of the yeasts orthologue encoded by MGM1 or Msp1, which is also mandatory for this process (Diot et al., 2009; Herlan et al., 2003). Furthermore in this thesis we show that the NT-OPA1-exon 4b peptide co-immuno-precipitates with mtDNA and specifically interacts with two major components of the mitochondrial nucleoids: the polymerase gamma and Tfam. Thus, from these experiments the conclusion is that NT-OPA1- exon 4b peptide contributes to the nucleoid anchoring in the inner mitochondrial membrane, a process that is required for the initiation of mtDNA replication and for the distribution of nucleoids along the network. These data provide new crucial insights in understanding the mechanism involved in maintenance of mtDNA integrity, because they clearly demonstrate that, besides genes implicated in mtDNA replications (i.e. polymerase gamma, Tfam, twinkle and genes involved in the nucleotide pool metabolism), OPA1 and mitochondrial membrane dynamics play also an important role. Noticeably, the effect on mtDNA is different depending on the specific OPA1 isoforms down-regulated, suggesting the involvement of two different combined mechanisms. Over two hundred OPA1 mutations, spread throughout the coding region of the gene, have been described to date, including substitutions, deletions or insertions. Some mutations are predicted to generate a truncated protein inducing haploinsufficiency, whereas the missense nucleotide substitutions result in aminoacidic changes which affect conserved positions of the OPA1 protein. So far, the functional consequences of OPA1 mutations in cells from DOA patients are poorly understood. Phosphorus MR spectroscopy in patients with the c.2708delTTAG deletion revealed a defect in oxidative phosphorylation in muscles (Lodi et al., 2004). An energetic impairment has been also show in fibroblasts with the severe OPA1 R445H mutation (Amati-Bonneau et al., 2005). It has been previously reported by our group that OPA1 mutations leading to haploinsufficiency are associated in fibroblasts to an oxidative phosphorylation dysfunction, mainly involving the respiratory complex I (Zanna et al., 2008). In this study we have evaluated the energetic efficiency of a panel of skin fibroblasts derived from DOA patients, five fibroblast cell lines with OPA1 mutations causing haploinsufficiency (DOA-H) and two cell lines bearing mis-sense aminoacidic substitutions (DOA-AA), and compared with control fibroblasts. Although both types of DOA fibroblasts maintained a similar ATP content when incubated in a glucose-free medium, i.e. when forced to utilize the oxidative phosphorylation only to produce ATP, the mitochondrial ATP synthesis through complex I, measured in digitonin-permeabilized cells, was significantly reduced in cells with OPA1 haploinsufficiency only, whereas it was similar to controls in cells with the missense substitutions. Furthermore, evaluation of the mitochondrial membrane potential (DYm) in the two fibroblast lines DOA-AA and in two DOA-H fibroblasts, namely those bearing the c.2819-2A>C mutation and the c.2708delTTAG microdeletion, revealed an anomalous depolarizing response to oligomycin in DOA-H cell lines only. This finding clearly supports the hypothesis that these mutations cause a significant alteration in the respiratory chain function, which can be unmasked only when the operation of the ATP synthase is prevented. Noticeably, oligomycin-induced depolarization in these cells was almost completely prevented by preincubation with cyclosporin A, a well known inhibitor of the permeability transition pore (PTP). This results is very important because it suggests for the first time that the voltage threshold for PTP opening is altered in DOA-H fibroblasts. Although this issue has not yet been addressed in the present study, several are the mechanisms that have been proposed to lead to PTP deregulation, including in particular increased reactive oxygen species production and alteration of Ca2+ homeostasis, whose role in DOA fibroblasts PTP opening is currently under investigation. Identification of the mechanisms leading to altered threshold for PTP regulation will help our understanding of the pathophysiology of DOA, but also provide a strategy for therapeutic intervention.

Il critico teatrale come operatore di scrittura scenica. La critica teatrale italiana tra pratica organizzativa e utilizzo dei nuovi media nel Nuovo Teatro e in alcune esperienze dal 2003 ad oggi

La crisi del “teatro come servizio pubblico” degli Stabili, Piccolo Teatro in testa, si manifesta allo stadio di insoddisfazione interna già alla fine degli anni Cinquanta. Se dal punto di vista della pratica scenica, la prima faglia di rottura è pressoché unanimemente ricondotta alla comparsa delle primissime messe in scena –discusse, irritanti e provocatorie- di Carmelo Bene e Quartucci (1959-60) più difficile è individuare il corrispettivo di un critico-intellettuale apportatore di una altrettanto deflagrante rottura. I nomi di Arbasino e di Flaiano sono, in questo caso, i primi che vengono alla mente, ma, seppure portatori di una critica sensibile al “teatro ufficiale”, così come viene ribattezzato dopo il Convegno di Ivrea (1967) il modello attuato dagli Stabili, essi non possono, a ben vedere, essere considerati i veri promotori di una modalità differente di fare critica che, a partire da quel Convegno, si accompagnerà stabilmente alla ricerca scenica del Nuovo Teatro. Ma in cosa consiste, allora, questa nuova “operatività” critica? Si tratta principalmente di una modalità capace di operare alle soglie della scrittura, abbracciando una progressiva, ma costante fuoriuscita dalla redazione di cronache teatrali, per ripensare radicalmente la propria attività in nuovi spazi operativi quali le riviste e l’editoria di settore, un rapporto sempre più stretto con i mass-media quali radio e televisione e la pratica organizzativa di momenti spettacolari e teorici al contempo -festival, convegni, rassegne e premi- per una forma di partecipazione poi identificata come “sporcarsi le mani”. La seconda parte della tesi è una raccolta documentaria sull’oggi. A partire dal Manifesto dei Critici Impuri redatto nel 2003 a Prato da un gruppo di critici dell'ultima generazione, la tesi utilizza quella dichiarazione come punto di partenza per creare un piccolo archivio sull’oggi raccogliendo le elaborazioni di alcune delle esperienze più significative di questi dieci anni. Ricca appendice di materiali.

Sparse Signal Representation of Ultrasonic Signals for Structural Health Monitoring Applications

Assessment of the integrity of structural components is of great importance for aerospace systems, land and marine transportation, civil infrastructures and other biological and mechanical applications. Guided waves (GWs) based inspections are an attractive mean for structural health monitoring. In this thesis, the study and development of techniques for GW ultrasound signal analysis and compression in the context of non-destructive testing of structures will be presented. In guided wave inspections, it is necessary to address the problem of the dispersion compensation. A signal processing approach based on frequency warping was adopted. Such operator maps the frequencies axis through a function derived by the group velocity of the test material and it is used to remove the dependence on the travelled distance from the acquired signals. Such processing strategy was fruitfully applied for impact location and damage localization tasks in composite and aluminum panels. It has been shown that, basing on this processing tool, low power embedded system for GW structural monitoring can be implemented. Finally, a new procedure based on Compressive Sensing has been developed and applied for data reduction. Such procedure has also a beneficial effect in enhancing the accuracy of structural defects localization. This algorithm uses the convolutive model of the propagation of ultrasonic guided waves which takes advantage of a sparse signal representation in the warped frequency domain. The recovery from the compressed samples is based on an alternating minimization procedure which achieves both an accurate reconstruction of the ultrasonic signal and a precise estimation of waves time of flight. Such information is used to feed hyperbolic or elliptic localization procedures, for accurate impact or damage localization.