Development of musculoskeletal models for the design and the pre-clinical validation of hip resurfacing prosthesis

Background. The surgical treatment of dysfunctional hips is a severe condition for the patient and a costly therapy for the public health. Hip resurfacing techniques seem to hold the promise of various advantages over traditional THR, with particular attention to young and active patients. Although the lesson provided in the past by many branches of engineering is that success in designing competitive products can be achieved only by predicting the possible scenario of failure, to date the understanding of the implant quality is poorly pre-clinically addressed. Thus revision is the only delayed and reliable end point for assessment. The aim of the present work was to model the musculoskeletal system so as to develop a protocol for predicting failure of hip resurfacing prosthesis. Methods. Preliminary studies validated the technique for the generation of subject specific finite element (FE) models of long bones from Computed Thomography data. The proposed protocol consisted in the numerical analysis of the prosthesis biomechanics by deterministic and statistic studies so as to assess the risk of biomechanical failure on the different operative conditions the implant might face in a population of interest during various activities of daily living. Physiological conditions were defined including the variability of the anatomy, bone densitometry, surgery uncertainties and published boundary conditions at the hip. The protocol was tested by analysing a successful design on the market and a new prototype of a resurfacing prosthesis. Results. The intrinsic accuracy of models on bone stress predictions (RMSE < 10%) was aligned to the current state of the art in this field. The accuracy of prediction on the bone-prosthesis contact mechanics was also excellent (< 0.001 mm). The sensitivity of models prediction to uncertainties on modelling parameter was found below 8.4%. The analysis of the successful design resulted in a very good agreement with published retrospective studies. The geometry optimisation of the new prototype lead to a final design with a low risk of failure. The statistical analysis confirmed the minimal risk of the optimised design over the entire population of interest. The performances of the optimised design showed a significant improvement with respect to the first prototype (+35%). Limitations. On the authors opinion the major limitation of this study is on boundary conditions. The muscular forces and the hip joint reaction were derived from the few data available in the literature, which can be considered significant but hardly representative of the entire variability of boundary conditions the implant might face over the patients population. This moved the focus of the research on modelling the musculoskeletal system; the ongoing activity is to develop subject-specific musculoskeletal models of the lower limb from medical images. Conclusions. The developed protocol was able to accurately predict known clinical outcomes when applied to a well-established device and, to support the design optimisation phase providing important information on critical characteristics of the patients when applied to a new prosthesis. The presented approach does have a relevant generality that would allow the extension of the protocol to a large set of orthopaedic scenarios with minor changes. Hence, a failure mode analysis criterion can be considered a suitable tool in developing new orthopaedic devices.

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.

Models and Algorihtm for the Optimization of Real-World Routing and Logistics Problems

Logistics involves planning, managing, and organizing the flows of goods from the point of origin to the point of destination in order to meet some requirements. Logistics and transportation aspects are very important and represent a relevant costs for producing and shipping companies, but also for public administration and private citizens. The optimization of resources and the improvement in the organization of operations is crucial for all branches of logistics, from the operation management to the transportation. As we will have the chance to see in this work, optimization techniques, models, and algorithms represent important methods to solve the always new and more complex problems arising in different segments of logistics. Many operation management and transportation problems are related to the optimization class of problems called Vehicle Routing Problems (VRPs). In this work, we consider several real-world deterministic and stochastic problems that are included in the wide class of the VRPs, and we solve them by means of exact and heuristic methods. We treat three classes of real-world routing and logistics problems. We deal with one of the most important tactical problems that arises in the managing of the bike sharing systems, that is the Bike sharing Rebalancing Problem (BRP). We propose models and algorithms for real-world earthwork optimization problems. We describe the 3DP process and we highlight several optimization issues in 3DP. Among those, we define the problem related to the tool path definition in the 3DP process, the 3D Routing Problem (3DRP), which is a generalization of the arc routing problem. We present an ILP model and several heuristic algorithms to solve the 3DRP.

Judicial Specialisation in Intellectual Property: the Unified Patent Court as a Model of Specialised Court

The aim of this thesis is to discuss and develop the Unified Patent Court project to account for the role it could play in implementing judicial specialisation in the Intellectual Property field. To provide an original contribution to the existing literature on the topic, this work addresses the issue of how the Unified Patent Court could relate to the other forms of judicial specialisation already operating in the European Union context. This study presents a systematic assessment of the not-yet-operational Unified Patent Court within the EU judicial system, which has recently shown a trend towards being developed outside the institutional framework of the European Union Court of Justice. The objective is to understand to what extent the planned implementation of the Unified Patent Court could succeed in responding to the need for specialisation and in being compliant with the EU legal and constitutional framework. Using the Unified Patent Court as a case study, it is argued that specialised courts in the field of Intellectual Property have a significant role to play in the European judicial system and offer an adequate response to the growing complexity of business operations and relations. The significance of this study is to analyse whether the UPC can still be considered as an appropriate solution to unify the European patent litigation system. The research considers the significant deficiencies, which risks having a negative effect on the European Union institutional procedures. In this perspective, this work aims to make a contribution in identifying the potential negative consequences of this reform. It also focuses on considering different alternatives for a European patent system, which could effectively promote innovation in Europe.

Evaluation of the transcriptomic response of an Alzheimer's disease murine model induced at different ages: searching for predictors

Alzheimer’s disease (AD) is a chronic, progressive neurodegenerative disease, characterized by the impairment of mnesic and cognitive functions, that represents the most frequent type of dementia in older people worldwide. Aging is the most important risk factor for the sporadic form of the pathology and it is associated to the progressive impairment of the proteostasis network. The endoplasmic reticulum (ER), the main cellular actor involved in proteostasis, appears significantly compromised in AD due to the accumulation of β-amyloid (Aβ) protein and phosphorylated-tau protein. Increasing proteins misfolding activates a specific cellular response known as Unfolded Protein response (UPR) which orchestrates the recovery of ER function. The aim of the present study was to investigate the role of UPR and aging process in a murine model of AD induced by intracerebroventricular (i.c.v.) injection of Aβ1-42 oligomers at 3 or 18 months. The oligomers injection in aged animals caused the increased of memory impairment, oxidative stress, and the depletion of glutathione reserve. Furthermore, the RNA-sequencing analysis was performed and the bioinformatic analysis showed the enrichment of several pathways involved in neurodegeneration and protein regulations. The following analysis highlighted the significant dysregulation of the three branches of the UPR, the protein kinase RNA-like ER kinase (PERK), inositol-requiring protein 1α (IRE1α) and activating transcription factor 6 (ATF-6). In turn, ER stress affected the PI3K/Akt/Gsk3β and MAPK/ERK pathways, highlighting Mapkapk5 as a potential marker of the neurodegenerative process, which regulation could lead to the definition of new pharmacological and neuroprotective strategies to counteract AD.

Emotions in legal decisions: the construction of objective narratives in Italian criminal trials

Drawing on ethnographic data collected in Italian courts and prosecution offices, this dissertation offers new perspectives on legal decision-making by highlighting the importance of emotions for constructing and evaluating legal narratives. Focusing on criminal cases, it describes and dissects how judges and prosecutors use emotions in reflection and action tied to lay narratives and legal constraints. The analysis shows that legal professionals engage in different types of emotional dynamics when dealing with stories; first, they develop gut feelings, which are either endorsed or kept at distance by means of emotional reflexivity, to comply with legal ideals of objectivity and impartiality. Second, empathy emerges as a crucial tool to direct the interaction with lay people and to interpret legal prerequisites, such as credibility, and intent. Finally, the dissertation shows that lay stories lead legal professionals to become passionate and committed towards the correct application of the law, the restoration of the moral order, and the achievement of justice. In light of the empirical findings, this thesis strives to develop a theoretical understanding of legal decision-making as narrative work that includes emotional dynamics consistent with rational, objective action.