User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

Each one teaches one: characterizing active forms of proteins by single molecule force spectroscopy

This Ph.D. candidate thesis collects the research work I conducted under the supervision of Prof.Bruno Samor´ı in 2005,2006 and 2007. Some parts of this work included in the Part III have been begun by myself during my undergraduate thesis in the same laboratory and then completed during the initial part of my Ph.D. thesis: the whole results have been included for the sake of understanding and completeness. During my graduate studies I worked on two very different protein systems. The theorical trait d’union between these studies, at the biological level, is the acknowledgement that protein biophysical and structural studies must, in many cases, take into account the dynamical states of protein conformational equilibria and of local physico-chemical conditions where the system studied actually performs its function. This is introducted in the introductory part in Chapter 2. Two different examples of this are presented: the structural significance deriving from the action of mechanical forces in vivo (Chapter 3) and the complexity of conformational equilibria in intrinsically unstructured proteins and amyloid formation (Chapter 4). My experimental work investigated both these examples by using in both cases the single molecule force spectroscopy technique (described in Chapter 5 and Chapter 6). The work conducted on angiostatin focused on the characterization of the relationships between the mechanochemical properties and the mechanism of action of the angiostatin protein, and most importantly their intertwining with the further layer of complexity due to disulfide redox equilibria (Part III). These studies were accompanied concurrently by the elaboration of a theorical model for a novel signalling pathway that may be relevant in the extracellular space, detailed in Chapter 7.2. The work conducted on -synuclein (Part IV) instead brought a whole new twist to the single molecule force spectroscopy methodology, applying it as a structural technique to elucidate the conformational equilibria present in intrinsically unstructured proteins. These equilibria are of utmost interest from a biophysical point of view, but most importantly because of their direct relationship with amyloid aggregation and, consequently, the aetiology of relevant pathologies like Parkinson’s disease. The work characterized, for the first time, conformational equilibria in an intrinsically unstructured protein at the single molecule level and, again for the first time, identified a monomeric folded conformation that is correlated with conditions leading to -synuclein and, ultimately, Parkinson’s disease. Also, during the research work, I found myself in the need of a generalpurpose data analysis application for single molecule force spectroscopy data analysis that could solve some common logistic and data analysis problems that are common in this technique. I developed an application that addresses some of these problems, herein presented (Part V), and that aims to be publicly released soon.

What Happened to Participation? Urban Development and Authoritarian Upgrading in Cairo's Informal Neighbourhoods

Participation appeared in development discourses for the first time in the 1970s, as a generic call for the involvement of the poor in development initiatives. Over the last three decades, the initial perspectives on participation intended as a project method for poverty reduction have evolved into a coherent and articulated theoretical elaboration, in which participation figures among the paraphernalia of good governance promotion: participation has acquired the status of “new orthodoxy”. Nevertheless, the experience of the implementation of participatory approaches in development projects seemed to be in the majority of cases rather disappointing, since the transformative potential of ‘participation in development’ depends on a series of factors in which every project can actually differ from others: the ultimate aim of the approach promoted, its forms and contents and, last but not least, the socio-political context in which the participatory initiative is embedded. In Egypt, the signature of a project agreement between the Arab Republic of Egypt and the Federal Republic of Germany, in 1998, inaugurated a Participatory Urban Management Programme (PUMP) to be implemented in Greater Cairo by the German Technical Cooperation (Deutsche Gesellschaft für Technische Zusammenarbeit, GTZ) and the Ministry of Planning (now Ministry of Local Development) and the Governorates of Giza and Cairo as the main counterparts. Now, ten years after the beginning of the PUMP/PDP and close to its end (December 2010), it is possible to draw some conclusions about the scope, the significance and the effects of the participatory approach adopted by GTZ and appropriated by the Egyptian counterparts in dealing with the issue of informal areas and, more generally, of urban development. Our analysis follows three sets of questions: the first set regards the way ‘participation’ has been interpreted and concretised by PUMP and PDP. The second is about the emancipating potential of the ‘participatory approach’ and its ability to ‘empower’ the ‘marginalised’. The third focuses on one hand on the efficacy of GTZ strategy to lead to an improvement of the delivery service in informal areas (especially in terms of planning and policies), and on the other hand on the potential of GTZ development intervention to trigger an incremental process of ‘democratisation’ from below.

Preparation of new crystal forms via photochemical, mechanochemical and sol-gel methods

This work of thesis involves various aspects of crystal engineering. Chapter 1 focuses on crystals containing crown ether complexes. Aspects such as the possibility of preparing these materials by non-solution methods, i.e. by direct reaction of the solid components, thermal behavior and also isomorphism and interconversion between hydrates are taken into account. In chapter 2 a study is presented aimed to understanding the relationship between hydrogen bonding capability and shape of the building blocks chosen to construct crystals. The focus is on the control exerted by shape on the organization of sandwich cations such as cobalticinium, decamethylcobalticinium and bisbenzenchromium(I) and on the aggregation of monoanions all containing carboxylic and carboxylate groups, into 0-D, 1-D, 2-D and 3-D networks. Reactions conducted in multi-component molecular assemblies or co-crystals have been recognized as a way to control reactivity in the solid state. The [2+2] photodimerization of olefins is a successful demonstration of how templated solid state synthesis can efficiently synthesize unique materials with remarkable stereoselectivity and under environment-friendly conditions. A demonstration of this synthetic strategy is given in chapter 3. The combination of various types of intermolecular linkages, leading to formation of high order aggregation and crystalline materials or to a random aggregation resulting in an amorphous precipitate, may not go to completeness. In such rare cases an aggregation process intermediate between crystalline and amorphous materials is observed, resulting in the formation of a gel, i.e. a viscoelastic solid-like or liquid-like material. In chapter 4 design of new Low Molecular Weight Gelators is presented. Aspects such as the relationships between molecular structure, crystal packing and gelation properties and the application of this kind of gels as a medium for crystal growth of organic molecules, such as APIs, are also discussed.

Rare and complicated forms of infantile hemangiomas: new therapeutic outlooks

Infantile hemangiomas (IHs) are the most common benign neoplastic pathology of childhood; their natural history generally involves three phases: after the onset, which usually occurs in the first weeks of life, there is the proliferation phase where the IH reaches its maximum development and it is followed by the spontaneous involution which leads to the IH regression. The duration and the extent of these phases may vary widely even though in most of the cases the involution process begins around twelve months of life and the regression, complete or partial, is completed around seventh-ninth year of life. The majority of the IHs does not require any treatment. However, 10%-20% is likely to develop serious complications, functional impairments or aesthetic alterations and entail a timely treatment. Although there is no treatment protocol currently shared, therapies usually used in cases with a complication risk consist in: systemic or intralesional steroids as a first choice; interferon α, vincristine and/or bleomicin as second or third choice and/or surgical treatment. Propranolol, a non-selective beta-blocker, has been used for cardiovascular diseases even in childhood for decades. Since 2008 it has been widely used in the IHs treatment, although it is still "off-label". In literature there are hundreds of cases and some clinical studies that show the effectiveness and safety of this drug for this indication. Thanks to a multidisciplinary team (Dermatologists, Cardiologists, Paediatricians, and Radiologists) of S. Orsola-Malpighi Hospital, a clinical study, which has been previously approved by the ethics committee, is carried out in order to evaluate the efficacy and safety of systemic propranolol in the treatment of IHs in paediatric age. At the end of 2012, 78 patients underwent this treatment: the results we have obtained so far show a good efficacy and safety profile in agreement with the data provided by the literature.

Use of shared memory in the context of embedded multi-core processors: exploration of the technology and its limits

Modern embedded systems embrace many-core shared-memory designs. Due to constrained power and area budgets, most of them feature software-managed scratchpad memories instead of data caches to increase the data locality. It is therefore programmers’ responsibility to explicitly manage the memory transfers, and this make programming these platform cumbersome. Moreover, complex modern applications must be adequately parallelized before they can the parallel potential of the platform into actual performance. To support this, programming languages were proposed, which work at a high level of abstraction, and rely on a runtime whose cost hinders performance, especially in embedded systems, where resources and power budget are constrained. This dissertation explores the applicability of the shared-memory paradigm on modern many-core systems, focusing on the ease-of-programming. It focuses on OpenMP, the de-facto standard for shared memory programming. In a first part, the cost of algorithms for synchronization and data partitioning are analyzed, and they are adapted to modern embedded many-cores. Then, the original design of an OpenMP runtime library is presented, which supports complex forms of parallelism such as multi-level and irregular parallelism. In the second part of the thesis, the focus is on heterogeneous systems, where hardware accelerators are coupled to (many-)cores to implement key functional kernels with orders-of-magnitude of speedup and energy efficiency compared to the “pure software” version. However, three main issues rise, namely i) platform design complexity, ii) architectural scalability and iii) programmability. To tackle them, a template for a generic hardware processing unit (HWPU) is proposed, which share the memory banks with cores, and the template for a scalable architecture is shown, which integrates them through the shared-memory system. Then, a full software stack and toolchain are developed to support platform design and to let programmers exploiting the accelerators of the platform. The OpenMP frontend is extended to interact with it.

Optimization of molecular and crystalline forms of drugs, agrochemicals, pesticides in relation to activity, bioavailability, patentability and to the fabrication of polymorphs, solvates, co-crystals with green chemistry methods

This doctorate was funded by the Regione Emilia Romagna, within a Spinner PhD project coordinated by the University of Parma, and involving the universities of Bologna, Ferrara and Modena. The aim of the project was: - Production of polymorphs, solvates, hydrates and co-crystals of active pharmaceutical ingredients (APIs) and agrochemicals with green chemistry methods; - Optimization of molecular and crystalline forms of APIs and pesticides in relation to activity, bioavailability and patentability. In the last decades, a growing interest in the solid-state properties of drugs in addition to their solution chemistry has blossomed. The achievement of the desired and/or the more stable polymorph during the production process can be a challenge for the industry. The study of crystalline forms could be a valuable step to produce new polymorphs and/or co-crystals with better physical-chemical properties such as solubility, permeability, thermal stability, habit, bulk density, compressibility, friability, hygroscopicity and dissolution rate in order to have potential industrial applications. Selected APIs (active pharmaceutical ingredients) were studied and their relationship between crystal structure and properties investigated, both in the solid state and in solution. Polymorph screening and synthesis of solvates and molecular/ionic co-crystals were performed according to green chemistry principles. Part of this project was developed in collaboration with chemical/pharmaceutical companies such as BASF (Germany) and UCB (Belgium). We focused on on the optimization of conditions and parameters of crystallization processes (additives, concentration, temperature), and on the synthesis and characterization of ionic co-crystals. Moreover, during a four-months research period in the laboratories of Professor Nair Rodriguez-Hormedo (University of Michigan), the stability in aqueous solution at the equilibrium of ionic co-crystals (ICCs) of the API piracetam was investigated, to understand the relationship between their solid-state and solution properties, in view of future design of new crystalline drugs with predefined solid and solution properties.