Theoretical and implementation aspects in the mechanization of the metatheory of programming languages

Interactive theorem provers are tools designed for the certification of formal proofs developed by means of man-machine collaboration. Formal proofs obtained in this way cover a large variety of logical theories, ranging from the branches of mainstream mathematics, to the field of software verification. The border between these two worlds is marked by results in theoretical computer science and proofs related to the metatheory of programming languages. This last field, which is an obvious application of interactive theorem proving, poses nonetheless a serious challenge to the users of such tools, due both to the particularly structured way in which these proofs are constructed, and to difficulties related to the management of notions typical of programming languages like variable binding. This thesis is composed of two parts, discussing our experience in the development of the Matita interactive theorem prover and its use in the mechanization of the metatheory of programming languages. More specifically, part I covers: - the results of our effort in providing a better framework for the development of tactics for Matita, in order to make their implementation and debugging easier, also resulting in a much clearer code; - a discussion of the implementation of two tactics, providing infrastructure for the unification of constructor forms and the inversion of inductive predicates; we point out interactions between induction and inversion and provide an advancement over the state of the art. In the second part of the thesis, we focus on aspects related to the formalization of programming languages. We describe two works of ours: - a discussion of basic issues we encountered in our formalizations of part 1A of the Poplmark challenge, where we apply the extended inversion principles we implemented for Matita; - a formalization of an algebraic logical framework, posing more complex challenges, including multiple binding and a form of hereditary substitution; this work adopts, for the encoding of binding, an extension of Masahiko Sato's canonical locally named representation we designed during our visit to the Laboratory for Foundations of Computer Science at the University of Edinburgh, under the supervision of Randy Pollack.

Transposable elements dynamics in taxa with different reproductive strategies or speciation rate

In recent years the advances in genomics allowed to understand the importance of Transposable Elements (TE) in the evolution of eukaryotic genomes. In this thesis I face two aspects of the TE impact on the in the animal kingdom. The first part is a comparison of the dynamics of the TE dynamics in three species of stick-insects of the Genus Bacillus. I produced three random genomic libraries of 200 Kbps for the three parental species of the taxon: a gonochoric population of Bacillus rossius (facultative parthenogenetic), Bacillus grandii (gonochoric) and Bacillus atticus (obligate parthenogenetic). The unisexual taxon Bacillus atticus does not shows dramatic differences in TE total content and activity with respect to Bacillus grandii and Bacillus rossius. This datum does not confirm the trend observed in other animal models in which unisexual taxa tend to repress the activity of TE to escape the extinction by accumulation of harmful mutations. In the second part I tried to add a contribute to the debate initiated in recent years about the possibility that a high TE content is linked to a high rate of speciation. I designed an evolutionary framework to establish the different rate of speciation among two or more taxa, then I compared TE dynamics considering the different rates of speciation. The species dataset comprises: 29 mammals, four birds, two fish and two insects. On the whole the majority of comparisons confirms the expected trend. In particular the amount of species analyzed in Mammalia allowed me to get a statistical support (p<0,05) of the fact that the TE activity of recently mobilized elements is positively related with the rate of speciation.

Lateral spreading and associated slope processes in fractured rock slabs

Landslides of the lateral spreading type, involving brittle geological units overlying ductile terrains, are a common occurrence in the sandstone and limestone plateaux of the northern Apennines of Italy. These instability phenomena can become particularly risky, when historical towns and cultural heritage sites built on the top of them are endangered. Neverthless, the mechanisms controlling the developing of related instabilities, i.e. toppling and rock falls, at the edges of rock plateaux are not fully understood yet. In addition, the groundwater flow path developing at the contact between the more permeable units, i.e. the jointed rock slab, and the relatively impermeable clay-rich units have not been already studied in details, even if they may play a role in this kind of instability processes, acting as eventual predisposing and/or triggering factors. Field survey, Terrestrial Laser Scanner and Close Range Photogrammetry techniques, laboratory tests on the involved materials, hydrogeological monitoring and modelling, displacements evaluation and stability analysis through continuum and discontinuum numerical codes have been performed on the San Leo case study, with the aim to bring further insights for the understanding and the assessment of the slope processes taking place in this geological context. The current research permitted to relate the aquifer behaviour of the rocky slab to slope instability processes. The aquifer hosted in the fractured slab leads to the development of perennial and ephemeral springs at the contact between the two units. The related piping erosion phenomena, together with slope processes in the clay-shales led to the progressive undermining of the slab. The cliff becomes progressively unstable due to undermining and undergoes large-scale landslides due to fall or topple.

Methods for Biodata Analysis in different Omic Contexts

The world of Computational Biology and Bioinformatics presently integrates many different expertise, including computer science and electronic engineering. A major aim in Data Science is the development and tuning of specific computational approaches to interpret the complexity of Biology. Molecular biologists and medical doctors heavily rely on an interdisciplinary expert capable of understanding the biological background to apply algorithms for finding optimal solutions to their problems. With this problem-solving orientation, I was involved in two basic research fields: Cancer Genomics and Enzyme Proteomics. For this reason, what I developed and implemented can be considered a general effort to help data analysis both in Cancer Genomics and in Enzyme Proteomics, focusing on enzymes which catalyse all the biochemical reactions in cells. Specifically, as to Cancer Genomics I contributed to the characterization of intratumoral immune microenvironment in gastrointestinal stromal tumours (GISTs) correlating immune cell population levels with tumour subtypes. I was involved in the setup of strategies for the evaluation and standardization of different approaches for fusion transcript detection in sarcomas that can be applied in routine diagnostic. This was part of a coordinated effort of the Sarcoma working group of "Alleanza Contro il Cancro". As to Enzyme Proteomics, I generated a derived database collecting all the human proteins and enzymes which are known to be associated to genetic disease. I curated the data search in freely available databases such as PDB, UniProt, Humsavar, Clinvar and I was responsible of searching, updating, and handling the information content, and computing statistics. I also developed a web server, BENZ, which allows researchers to annotate an enzyme sequence with the corresponding Enzyme Commission number, the important feature fully describing the catalysed reaction. More to this, I greatly contributed to the characterization of the enzyme-genetic disease association, for a better classification of the metabolic genetic diseases.

AI and legal personhood: a theoretical survey

I set out the pros and cons of conferring legal personhood on artificial intelligence systems (AIs), mainly under civil law. I provide functionalist arguments to justify this policy choice and identify the content that such a legal status might have. Although personhood entails holding one or more legal positions, I will focus on the distribution of liabilities arising from unpredictably illegal and harmful conduct. Conferring personhood on AIs might efficiently allocate risks and social costs, ensuring protection for victims, incentives for production, and technological innovation. I also consider other legal positions, e.g., the capacity to act, the ability to hold property, make contracts, and sue (and be sued). However, I contend that even assuming that conferring personhood on AIs finds widespread consensus, its implementation requires solving a coordination problem, determined by three asymmetries: technological, intra-legal systems, and inter-legal systems. I address the coordination problem through conceptual analysis and metaphysical explanation. I first frame legal personhood as a node of inferential links between factual preconditions and legal effects. Yet, this inferentialist reading does not account for the ‘background reasons’, i.e., it does not explain why we group divergent situations under legal personality and how extra-legal information is integrated into it. One way to account for this background is to adopt a neo-institutional perspective and update its ontology of legal concepts with further layers: the meta-institutional and the intermediate. Under this reading, the semantic referent of legal concepts is institutional reality. So, I use notions of analytical metaphysics, such as grounding and anchoring, to explain the origins and constituent elements of legal personality as an institutional kind. Finally, I show that the integration of conceptual and metaphysical analysis can provide the toolkit for finding an equilibrium around the legal-policy choices that are involved in including (or not including) AIs among legal persons.

Essays in macroeconomics: insurance, market power, and inequality

This thesis investigates a broad range of topics related to insurance, market power, and inequality, both from an empirical and a theoretical perspective. In the first chapter, I exploit the significant heterogeneity of the shocks hitting Ethiopian households and their heterogeneous response, using relatively recent data (World Bank's LSMS-ISA for households and satellite data for weather shocks). On the one hand, households seem able to insure against most idiosyncratic and mild adverse weather shocks. On the other hand, vulnerability to stronger weather shocks (especially droughts) remains elevated. In the second chapter, starting from firms' individual data, aggregate trends about industry concentration and other proxies of competition are built. This chapter is part of a larger project conducted at the OECD in the Productivity Innovation and Entrepreneurship Division of the STI Directorate The project innovates on the existing literature in its measurement of concentration, aimed at reflecting markets more accurately. On average, aggregate concentration is found to be increasing. In the third chapter, which only lays out some preliminary steps of a more extensive inquiry, I model the heterogeneous effects of aggregate technological progress on individual economic agents and show how this can affect aggregate inequality and other aggregate indicators studied in the macroeconomics literature, such as the entrepreneurship rate and the overall firm distribution. It should be noted, however, that this note is a simple exposition of a possible modelling device rather than a full explanation of these phenomena.