L'epatite E nei suidi: epidemiologia, diagnosi e filogenesi

Hepatitis E is an infectious viral disease with clinical and morphological features of acute hepatitis. The aetiological agent is the Hepatitis E virus (HEV). The disease represents an important Public Health problem in developing countries where is frequently epidemic and primarily transmitted by fecal-oral route. In the last few years, a certain number of sporadic cases have been also described in industrialized countries, Italy included. A swine HEV was first identified in 1997 and is now considered an ubiquitous virus. Human and swine strains from the same geographical region have shown to have a high level of nucleotidic omology and in experimental infections, the possibility of interspecific transmission of swine strains to humans and of human strains to non-human primates has been demonstrated. Furthermore, some seroepidemiological studies have demonstrated that people working in contact with swine have a higher risk to get infected than normal blood donors. Recently, cases of HEV hepatitis have been directly associated to the ingestion of uncooked tissues from pigs, wild boar or deer and today the disease is considered an emerging zoonosis. The aims of this thesis were: evaluate HEV prevalence in Italian swine herds (both in fattening and in breeding animals); investigate the possibility of finding HEV in livers used for human consumption; investigate if there is any correlation between HEV infection and the presence of macroscopical lesions; investigate HEV prevalence in a demographic managed wild boar population; phylogenetically analyse viral strains identified. During an internship period at Veterinary Laboratories Agency (Weybridge, UK), furthermore, swine samples at different stages of production and slurry lagoons have been analysed. Six swine herds located in North Italy have been sampled at different stage of production. The overall prevalence resulted 42%, and both breeding and fattening animals were positive for HEV infection. A longitudinal study has been conducted in a herd across all stages of production until the slaughtering age. Livers have been collected from the animals at the abattoir and 11.8% of them were positive for HEV infection. No correlations have been identified between HEV infection and macroscopical lesions in pigs affected by different pathological conditions. Of 86 wild boars tested 22 (25%) were positive for HEV. Of the swine tested in UK 21,5 % and 2 of the 9 slurry lagoons (22,2%) were positive for HEV infection. All the strains identified belonged to genotype 3 and showed high percentages of nucleotidic identity with humans and swine strains identified in Europe. The high prevalence detected in these studies confirms the widespread diffusion of HEV in swine populations in Italy and in UK. Phylogenetical analysis of identified strains, similar to those identified in autochthonous human hepatitis E cases of the same geographical area, confirm the hypothesis that pigs can be a font of zoonotical infection. The finding that a fraction of the livers inserted in the food chain are positive for HEV infection it’s of some concern for Public Health. The finding of a high HEV prevalence in all examined farms, together with the observation that infection may be sub-clinical and affect animals at slaughtering age, raise concern because of the possible risk of transmission of HEV to humans by either direct contact with infected pigs, indirect contact with environment and working instruments contaminated with pig feces, or ingestion of contaminated undercooked meat.

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.

Effect of Laser Shock Peening on Fatigue Crack Propagation of Aeronautical Structures

Laser Shock Peening (LSP) is a surface enhancement treatment which induces a significant layer of beneficial compressive residual stresses up to several mm underneath the surface of metal components in order to improve the detrimental effects of crack growth behavior rate in it. The aim of this thesis is to predict the crack growth behavior of thin Aluminum specimens with one or more LSP stripes defining a compressive residual stress area. The LSP treatment has been applied as crack retardation stripes perpendicular to the crack growing direction, with the objective of slowing down the crack when approaching the LSP patterns. Different finite element approaches have been implemented to predict the residual stress field left by the laser treatment, mostly by means of the commercial software Abaqus/Explicit. The Afgrow software has been used to predict the crack growth behavior of the component following the laser peening treatment and to detect the improvement in fatigue life comparing to the specimen baseline. Furthermore, an analytical model has been implemented on the Matlab software to make more accurate predictions on fatigue life of the treated components. An educational internship at the Research and Technologies Germany- Hamburg department of Airbus helped to achieve knowledge and experience to write this thesis. The main tasks of the thesis are the following: -To up to date Literature Survey related to laser shock peening in metallic structures -To validate the FE models developed against experimental measurements at coupon level -To develop design of crack growth slow down in centered and edge cracked tension specimens based on residual stress engineering approach using laser peened patterns transversal to the crack path -To predict crack growth behavior of thin aluminum panels -To validate numerical and analytical results by means of experimental tests.