Revisiting the Security of the ALRED Design and Two of Its Variants: Marvin and LetterSoup

The ALRED construction is a lightweight strategy for constructing message authentication algorithms from an underlying iterated block cipher. Even though this construction's original analyses show that it is secure against some attacks, the absence of formal security proofs in a strong security model still brings uncertainty on its robustness. In this paper, aiming to give a better understanding of the security level provided by different authentication algorithms based on this design strategy, we formally analyze two ALRED variants-the MARVIN message authentication code and the LETTERSOUP authenticated-encryption scheme,-bounding their security as a function of the attacker's resources and of the underlying cipher's characteristics.

Phase Transition for the Ising Model on the Critical Lorentzian Triangulation

The ferromagnetic Ising model without external field on an infinite Lorentzian triangulation sampled from the uniform distribution is considered. We prove uniqueness of the Gibbs measure in the high temperature region and coexistence of at least two Gibbs measures at low temperature. The proofs are based on the disagreement percolation method and on a variant of the Peierls contour method. The critical temperature is shown to be constant a.s.

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.

L'a(rche)tipico Brian O'Nolan. Comico e riso dalla tradizione al post-

This study aims at analysing Brian O'Nolans literary production in the light of a reconsideration of the role played by his two most famous pseudonyms ,Flann Brien and Myles na Gopaleen, behind which he was active both as a novelist and as a journalist. We tried to establish a new kind of relationship between them and their empirical author following recent cultural and scientific surveys in the field of Humour Studies, Psychology, and Sociology: taking as a starting point the appreciation of the comic attitude in nature and in cultural history, we progressed through a short history of laughter and derision, followed by an overview on humour theories. After having established such a frame, we considered an integration of scientific studies in the field of laughter and humour as a base for our study scheme, in order to come to a definition of the comic author as a recognised, powerful and authoritative social figure who acts as a critic of conventions. The history of laughter and comic we briefly summarized, based on the one related by the French scholar Georges Minois in his work (Minois 2004), has been taken into account in the view that humorous attitude is one of man’s characteristic traits always present and witnessed throughout the ages, though subject in most cases to repression by cultural and political conservative power. This sort of Super-Ego notwithstanding, or perhaps because of that, comic impulse proved irreducible exactly in its influence on the current cultural debates. Basing mainly on Robert R. Provine’s (Provine 2001), Fabio Ceccarelli’s (Ceccarelli 1988), Arthur Koestler’s (Koestler 1975) and Peter L. Berger’s (Berger 1995) scientific essays on the actual occurrence of laughter and smile in complex social situations, we underlined the many evidences for how the use of comic, humour and wit (in a Freudian sense) could be best comprehended if seen as a common mind process designed for the improvement of knowledge, in which we traced a strict relation with the play-element the Dutch historian Huizinga highlighted in his famous essay, Homo Ludens (Huizinga 1955). We considered comic and humour/wit as different sides of the same coin, and showed how the demonstrations scientists provided on this particular subject are not conclusive, given that the mental processes could not still be irrefutably shown to be separated as regards graduations in comic expression and reception: in fact, different outputs in expressions might lead back to one and the same production process, following the general ‘Economy Rule’ of evolution; man is the only animal who lies, meaning with this that one feeling is not necessarily biuniquely associated with one and the same outward display, so human expressions are not validation proofs for feelings. Considering societies, we found that in nature they are all organized in more or less the same way, that is, in élites who govern over a community who, in turn, recognizes them as legitimate delegates for that task; we inferred from this the epistemological possibility for the existence of an added ruling figure alongside those political and religious: this figure being the comic, who is the person in charge of expressing true feelings towards given subjects of contention. Any community owns one, and his very peculiar status is validated by the fact that his place is within the community, living in it and speaking to it, but at the same time is outside it in the sense that his action focuses mainly on shedding light on ideas and objects placed out-side the boundaries of social convention: taboos, fears, sacred objects and finally culture are the favourite targets of the comic person’s arrow. This is the reason for the word a(rche)typical as applied to the comic figure in society: atypical in a sense, because unconventional and disrespectful of traditions, critical and never at ease with unblinkered respect of canons; archetypical, because the “village fool”, buffoon, jester or anyone in any kind of society who plays such roles, is an archetype in the Jungian sense, i.e. a personification of an irreducible side of human nature that everybody instinctively knows: a beginner of a tradition, the perfect type, what is most conventional of all and therefore the exact opposite of an atypical. There is an intrinsic necessity, we think, of such figures in societies, just like politicians and priests, who should play an elitist role in order to guide and rule not for their own benefit but for the good of the community. We are not naïve and do know that actual owners of power always tend to keep it indefinitely: the ‘social comic’ as a role of power has nonetheless the distinctive feature of being the only job whose tension is not towards stability. It has got in itself the rewarding permission of contradiction, for the very reason we exposed before that the comic must cast an eye both inside and outside society and his vision may be perforce not consistent, then it is satisfactory for the popularity that gives amongst readers and audience. Finally, the difference between governors, priests and comic figures is the seriousness of the first two (fundamentally monologic) and the merry contradiction of the third (essentially dialogic). MPs, mayors, bishops and pastors should always console, comfort and soothe popular mood in respect of the public convention; the comic has the opposite task of provoking, urging and irritating, accomplishing at the same time a sort of control of the soothing powers of society, keepers of the righteousness. In this view, the comic person assumes a paramount importance in the counterbalancing of power administration, whether in form of acting in public places or in written pieces which could circulate for private reading. At this point comes into question our Irish writer Brian O'Nolan(1911-1966), real name that stood behind the more famous masks of Flann O'Brien, novelist, author of At Swim-Two-Birds (1939), The Hard Life (1961), The Dalkey Archive (1964) and, posthumously, The Third Policeman (1967); and of Myles na Gopaleen, journalist, keeper for more than 25 years of the Cruiskeen Lawn column on The Irish Times (1940-1966), and author of the famous book-parody in Irish An Béal Bocht (1941), later translated in English as The Poor Mouth (1973). Brian O'Nolan, professional senior civil servant of the Republic, has never seen recognized his authorship in literary studies, since all of them concentrated on his alter egos Flann, Myles and some others he used for minor contributions. So far as we are concerned, we think this is the first study which places the real name in the title, this way acknowledging him an unity of intents that no-one before did. And this choice in titling is not a mere mark of distinction for the sake of it, but also a wilful sign of how his opus should now be reconsidered. In effect, the aim of this study is exactly that of demonstrating how the empirical author Brian O'Nolan was the real Deus in machina, the master of puppets who skilfully directed all of his identities in planned directions, so as to completely fulfil the role of the comic figure we explained before. Flann O'Brien and Myles na Gopaleen were personae and not persons, but the impression one gets from the critical studies on them is the exact opposite. Literary consideration, that came only after O'Nolans death, began with Anne Clissmann’s work, Flann O'Brien: A Critical Introduction to His Writings (Clissmann 1975), while the most recent book is Keith Donohue’s The Irish Anatomist: A Study of Flann O'Brien (Donohue 2002); passing through M.Keith Booker’s Flann O'Brien, Bakhtin and Menippean Satire (Booker 1995), Keith Hopper’s Flann O'Brien: A Portrait of the Artist as a Young Post-Modernist (Hopper 1995) and Monique Gallagher’s Flann O'Brien, Myles et les autres (Gallagher 1998). There have also been a couple of biographies, which incidentally somehow try to explain critical points his literary production, while many critical studies do the same on the opposite side, trying to found critical points of view on the author’s restless life and habits. At this stage, we attempted to merge into O'Nolan's corpus the journalistic articles he wrote, more than 4,200, for roughly two million words in the 26-year-old running of the column. To justify this, we appealed to several considerations about the figure O'Nolan used as writer: Myles na Gopaleen (later simplified in na Gopaleen), who was the equivalent of the street artist or storyteller, speaking to his imaginary public and trying to involve it in his stories, quarrels and debates of all kinds. First of all, he relied much on language for the reactions he would obtain, playing on, and with, words so as to ironically unmask untrue relationships between words and things. Secondly, he pushed to the limit the convention of addressing to spectators and listeners usually employed in live performing, stretching its role in the written discourse to come to a greater effect of involvement of readers. Lastly, he profited much from what we labelled his “specific weight”, i.e. the potential influence in society given by his recognised authority in determined matters, a position from which he could launch deeper attacks on conventional beliefs, so complying with the duty of a comic we hypothesised before: that of criticising society even in threat of losing the benefits the post guarantees. That seemingly masochistic tendency has its rationale. Every representative has many privileges on the assumption that he, or she, has great responsibilities in administrating. The higher those responsibilities are, the higher is the reward but also the severer is the punishment for the misfits done while in charge. But we all know that not everybody accepts the rules and many try to use their power for their personal benefit and do not want to undergo law’s penalties. The comic, showing in this case more civic sense than others, helped very much in this by the non-accessibility to the use of public force, finds in the role of the scapegoat the right accomplishment of his task, accepting the punishment when his breaking of the conventions is too stark to be forgiven. As Ceccarelli demonstrated, the role of the object of laughter (comic, ridicule) has its very own positive side: there is freedom of expression for the person, and at the same time integration in the society, even though at low levels. Then the banishment of a ‘social’ comic can never get to total extirpation from society, revealing how the scope of the comic lies on an entirely fictional layer, bearing no relation with facts, nor real consequences in terms of physical health. Myles na Gopaleen, mastering these three characteristics we postulated in the highest way, can be considered an author worth noting; and the oeuvre he wrote, the whole collection of Cruiskeen Lawn articles, is rightfully a novel because respects the canons of it especially regarding the authorial figure and his relationship with the readers. In addition, his work can be studied even if we cannot conduct our research on the whole of it, this proceeding being justified exactly because of the resemblances to the real figure of the storyteller: its ‘chapters’ —the daily articles— had a format that even the distracted reader could follow, even one who did not read each and every article before. So we can critically consider also a good part of them, as collected in the seven volumes published so far, with the addition of some others outside the collections, because completeness in this case is not at all a guarantee of a better precision in the assessment; on the contrary: examination of the totality of articles might let us consider him as a person and not a persona. Once cleared these points, we proceeded further in considering tout court the works of Brian O'Nolan as the works of a unique author, rather than complicating the references with many names which are none other than well-wrought sides of the same personality. By putting O'Nolan as the correct object of our research, empirical author of the works of the personae Flann O'Brien and Myles na Gopaleen, there comes out a clearer literary landscape: the comic author Brian O'Nolan, self-conscious of his paramount role in society as both a guide and a scourge, in a word as an a(rche)typical, intentionally chose to differentiate his personalities so as to create different perspectives in different fields of knowledge by using, in addition, different means of communication: novels and journalism. We finally compared the newly assessed author Brian O'Nolan with other great Irish comic writers in English, such as James Joyce (the one everybody named as the master in the field), Samuel Beckett, and Jonathan Swift. This comparison showed once more how O'Nolan is in no way inferior to these authors who, greatly celebrated by critics, have nonetheless failed to achieve that great public recognition O’Nolan received alias Myles, awarded by the daily audience he reached and influenced with his Cruiskeen Lawn column. For this reason, we believe him to be representative of the comic figure’s function as a social regulator and as a builder of solidarity, such as that Raymond Williams spoke of in his work (Williams 1982), with in mind the aim of building a ‘culture in common’. There is no way for a ‘culture in common’ to be acquired if we do not accept the fact that even the most functional society rests on conventions, and in a world more and more ‘connected’ we need someone to help everybody negotiate with different cultures and persons. The comic gives us a worldly perspective which is at the same time comfortable and distressing but in the end not harmful as the one furnished by politicians could be: he lets us peep into parallel worlds without moving too far from our armchair and, as a consequence, is the one who does his best for the improvement of our understanding of things.

I diplomi militari: una fonte epigrafica ufficiale per lo studio delle flotte provinciali romane

This work analyzes the role of roman provincial fleets, mainly through the use of military diplomas. All the evidence has been collected, ordered and commented with special attention to the role of diplomas as official documents for the study of the naval provincial garrisons in the Ist and IInd centuries A.D.. Problems deriving from diplomas as still imperfect proofs for a full reconstruction of the history of roman fleets have been registered. Epigraphic evidence has been also taken into account to describe the history of the fleets.

New target tracking and monitoring guidance laws for UAV

A pursuer UAV tracking and loitering around a target is the problem analyzed in this thesis. The UAV is assumed to be a fixed-wing vehicle and constant airspeed together with bounded lateral accelerations are the main constraints of the problem. Three different guidance laws are designed for ensuring a continuos overfly on the target. Different proofs are presented to demonstrate the stability properties of the laws. All the algorithms are tested on a 6DoF Pioneer software simulator. Classic control design methods have been adopted to develop autopilots for implementig the simulation platform used for testing the guidance laws.

Cellulose based Lithium ion polymer electrolytes for Lithium batteries

The separator membrane in batteries and fuel cells is of crucial importance for the function of these devices. In lithium ion batteries the separator membrane as well as the polymer matrix of the electrodes consists of polymer electrolytes which are lithium ion conductors. To overcome the disadvantage of currently used polymer electrolytes which are highly swollen with liquids and thus mechanically and electrochemically unstable, the goal of this work is a new generation of solid polymer electrolytes with a rigid backbone and a soft side chain structure. Moreover the novel material should be based on cheap substrates and its synthesis should not be complicated aiming at low overall costs. The new materials are based on hydroxypropylcellulose and oligoethyleneoxide derivatives as starting materials. The grafting of the oligoethyleneoxide side chains onto the cellulose was carried out following two synthetic methods. One is based on a bromide derivative and another based on p-toluolsulfonyl as a leaving group. The side chain reagents were prepared form tri(ethylene glycol) monoethyl ether. In order to improve the mechanical properties the materials were crosslinked. Two different conceptions have been engaged based on either urethane chemistry or photosensitive dimethyl-maleinimide derivatives. PEO - graft - cellulose derivatives with a high degree of substitution between 2,9 and 3,0 were blended with lithium trifluoromethane-sulfonate, lithium bis(trifluorosulfone)imide and lithium tetrafluoroborate. The molar ratios were in the range from 0,02 to 0,2 [Li]/[O]. The products have been characterized with nuclear magnetic resonance (NMR), gel permeation chromatography (GPC) and laserlight scattering (LS) with respect to their degree of substitution and molecular weight. The effect of salt concentration on ionic conductivity, thermal behaviour and morphology has been investiga-ted with impedance spectroscopy, differential scanning calorimetry (DSC) and thermal gravimetric analysis (TGA). The crosslinking reactions were controlled with dynamic mechanical analysis (DMS). The degree of substitution of our products is varying between 2,8 and 3,0 as determined by NMR. PEO - graft - cellulose derivatives are highly viscous liquids at room temperature with glass transition temperatures around 215 K. The glass transition temperature for the Lithium salt complexes of PEO - graft - cellulose deri-vatives increase with increasing salt content. The maximum conductivity at room temperature is about 10-4 and at 100°C around 10-3 Scm-1. The presence of lithium salt decreases the thermal stability of the complexes in comparison to pure PEO - graft - cellulose derivatives. Complexes heated over 140 – 150°C completely lose their ionic conductivity. The temperature dependence of the conductivity presented as Arrhenius-type plots for all samples is similar in shape and follows a VTF behaviour. This proofs that the ionic transport is closely related to the segmental motions of the polymer chains. Novel cellulose derivatives with grafted oligoethylen-oxide side chains with well-defined chemical structure and high side chain grafting density have been synthesized. Cellulose was chosen as stiff, rod like macromolecule for the backbone while oligoethylen-oxides are chosen as flexible side chains. A maximum grafting density of 3.0 have been obtained. The best conductivity reaches 10-3 Scm-1 at 100°C for a Li-triflate salt complex with a [Li]/[O] ratio of 0.8. The cross-linked complexes containing the lithium salts form elastomeric films with convenient mechanical stability. Our method of cellulose modification is based on relatively cheap and commercially available substrates and as such appears to be a promising alternative for industrial applications.

A dictionary of modular threefolds

The thesis deals with the modularity conjecture for three-dimensional Calabi-Yau varieties. This is a generalization of the work of A. Wiles and others on modularity of elliptic curves. Modularity connects the number of points on varieties with coefficients of certain modular forms. In chapter 1 we collect the basics on arithmetic on Calabi-Yau manifolds, including general modularity results and strategies for modularity proofs. In chapters 2, 3, 4 and 5 we investigate examples of modular Calabi-Yau threefolds, including all examples occurring in the literature and many new ones. Double octics, i.e. Double coverings of projective 3-space branched along an octic surface, are studied in detail. In chapter 6 we deal with examples connected with the same modular forms. According to the Tate conjecture there should be correspondences between them. Many correspondences are constructed explicitly. We finish by formulating conjectures on the occurring newforms, especially their levels. In the appendices we compile tables of coefficients of weight 2 and weight 4 newforms and many examples of double octics.

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.

On the geometry of the spin-statistics connection in quantum mechanics

The Spin-Statistics theorem states that the statistics of a system of identical particles is determined by their spin: Particles of integer spin are Bosons (i.e. obey Bose-Einstein statistics), whereas particles of half-integer spin are Fermions (i.e. obey Fermi-Dirac statistics). Since the original proof by Fierz and Pauli, it has been known that the connection between Spin and Statistics follows from the general principles of relativistic Quantum Field Theory. In spite of this, there are different approaches to Spin-Statistics and it is not clear whether the theorem holds under assumptions that are different, and even less restrictive, than the usual ones (e.g. Lorentz-covariance). Additionally, in Quantum Mechanics there is a deep relation between indistinguishabilty and the geometry of the configuration space. This is clearly illustrated by Gibbs' paradox. Therefore, for many years efforts have been made in order to find a geometric proof of the connection between Spin and Statistics. Recently, various proposals have been put forward, in which an attempt is made to derive the Spin-Statistics connection from assumptions different from the ones used in the relativistic, quantum field theoretic proofs. Among these, there is the one due to Berry and Robbins (BR), based on the postulation of a certain single-valuedness condition, that has caused a renewed interest in the problem. In the present thesis, we consider the problem of indistinguishability in Quantum Mechanics from a geometric-algebraic point of view. An approach is developed to study configuration spaces Q having a finite fundamental group, that allows us to describe different geometric structures of Q in terms of spaces of functions on the universal cover of Q. In particular, it is shown that the space of complex continuous functions over the universal cover of Q admits a decomposition into C(Q)-submodules, labelled by the irreducible representations of the fundamental group of Q, that can be interpreted as the spaces of sections of certain flat vector bundles over Q. With this technique, various results pertaining to the problem of quantum indistinguishability are reproduced in a clear and systematic way. Our method is also used in order to give a global formulation of the BR construction. As a result of this analysis, it is found that the single-valuedness condition of BR is inconsistent. Additionally, a proposal aiming at establishing the Fermi-Bose alternative, within our approach, is made.

Entschlüsselung des Carotinoid-Metabolismus im marinen Schwamm Suberites domuncula

Die Enzyme des Carotinoidstoffwechsels spalten Provitamin A-Carotinoide in wichtige Retinoide (z.B. Vitamin A, Retinsäure), die Organismen während der Entwicklung und in visuellen Systemen benötigen. Die vorliegende Arbeit präsentiert erstmalig eine Carotinoxygenase (BCO) aus Schwämmen (S. domuncula), die einzigartig im Tierreich ist und nur einen orthologen Vertreter in Pflanzen (Crocus sativus) wieder findet. Das Enzym ist eine 7,8(7’,8’)-Carotinoxygenase, die C40-Carotinoide zu einem C10-Apocarotinoid und 8’-Apocarotinal spaltet. Mittels HPLC wurden sowohl die Primärspaltprodukte von β-Carotin, Lykopin und Zeaxanthin als auch das für alle identische innere Kettenstück (Crocetin) bei Doppelspaltung nachgewiesen. Der Nachweis der BCO-Transkripte (unter anderem in-situ) belegt eine Beteiligung des Enzyms während Entwicklungsprozessen und offenbart sowohl eine streng räumlich-zeitliche als auch eine über Rückkopplungsprozesse gesteuerte Regulierung des Enzyms. Ein weiteres hier identifiziertes Gen ähnelt einer bakteriellen Apocarotinoidoxygenase (ACO), welche das 8’-Apocarotinal der BCO erneut spaltet und so Retinal generiert. Letzteres dient als Chromophor zahlreicher visueller Systeme und kann über Enzyme des Retinoidstoffwechsels entweder gespeichert, oder in das wichtige Morphogen Retinsäure umgesetzt werden. Hier werden zwei potentielle Enzyme vorgestellt, die an dieser Interkonversion Retinal/Retinol (Speicher) beteiligt sein könnten als auch eines, das evtl. Retinal zu Retinsäure umsetzt. Die hier vorgestellten Ergebnisse unterstützen die Hypothese, dass Retinsäure kein autapomorphes Morphogen der Chordaten darstellt.

Mixnets e EasyCrypt: dimostrazioni crittografiche assistite da calcolatore

Negli ultimi anni l'avanzamento della ricerca in campo crittografico ha portato alla necessità di utilizzare strumenti software per la verifica delle prove formali. EasyCrypt è un tool, in fase di sviluppo, ideato per dimostrazioni basate su sequenze di giochi. Nella presente tesi viene presentato un caso di studio riguardante l'applicabilità di EasyCrypt alle mixing networks (abbr. mixnets). è presente un'esaustiva rassegna delle mixnets proposte in letteratura ed è descritta la teoria alla base delle dimostrazioni critografiche basate su sequenze di giochi. EasyCrypt viene analizzato nei suoi fondamenti teorici nonché nelle applicazioni pratiche, con riferimento particolare agli esperimenti svolti per la dimostrazione di proprietà di sicurezza delle mixnets.

Extending Implicit Computational Complexity and Abstract Machines to Languages with Control

The Curry-Howard isomorphism is the idea that proofs in natural deduction can be put in correspondence with lambda terms in such a way that this correspondence is preserved by normalization. The concept can be extended from Intuitionistic Logic to other systems, such as Linear Logic. One of the nice conseguences of this isomorphism is that we can reason about functional programs with formal tools which are typical of proof systems: such analysis can also include quantitative qualities of programs, such as the number of steps it takes to terminate. Another is the possiblity to describe the execution of these programs in terms of abstract machines. In 1990 Griffin proved that the correspondence can be extended to Classical Logic and control operators. That is, Classical Logic adds the possiblity to manipulate continuations. In this thesis we see how the things we described above work in this larger context.

Circulating Fibrocytes, their role in renal fibrosis and molecular pathways involved. Possible biomarkers of fibrogenesis in chronic kidney disease

Circulating Fibrocytes (CFs) are bone marrow-derived mesenchymal progenitor cells that express a similar pattern of surface markers related to leukocytes, hematopoietic progenitor cells and fibroblasts. CFs precursor display an ability to differentiate into fibroblasts and Myofibroblasts, as well as adipocytes. Fibrocytes have been shown to contribute to tissue fibrosis in the end-stage renal disease (ESRD), as well as in other fibrotic diseases, leading to fibrogenic process in other organs including lung, cardiac, gut and liver. This evidence has been confirmed by several experimental proofs in mice models of kidney injury. In the present study, we developed a protocol for the study of CFs, by using peripheral blood monocytes cells (PBMCs) samples collected from healthy human volunteers. Thanks to a flow cytometry method, in vitro culture assays and the gene expression assays, we are able to study and characterize this CFs population. Moreover, results confirmed that these approaches are reliable and reproducible for the investigation of the circulating fibrocytes population in whole blood samples. Our final aim is to confirm the presence of a correlation between the renal fibrosis progression, and the different circulating fibrocyte levels in Chronic Kidney Disease (CKD) patients. Thanks to a protocol study presented and accepted by the Ethic Committee we are continuing the study of CFs induction in a cohort of sixty patients affected by CKD, divided in three distinct groups for different glomerular filtration rate (GFR) levels, plus a control group of thirty healthy subjects. Ongoing experiments will determine whether circulating fibrocytes represent novel biomarkers for the study of CKD progression, in the early and late phases of this disease.

Efficient certification of feasibility and objective value of linear programs and its applications

The use of linear programming in various areas has increased with the significant improvement of specialized solvers. Linear programs are used as such to model practical problems, or as subroutines in algorithms such as formal proofs or branch-and-cut frameworks. In many situations a certified answer is needed, for example the guarantee that the linear program is feasible or infeasible, or a provably safe bound on its objective value. Most of the available solvers work with floating-point arithmetic and are thus subject to its shortcomings such as rounding errors or underflow, therefore they can deliver incorrect answers. While adequate for some applications, this is unacceptable for critical applications like flight controlling or nuclear plant management due to the potential catastrophic consequences. We propose a method that gives a certified answer whether a linear program is feasible or infeasible, or returns unknown'. The advantage of our method is that it is reasonably fast and rarely answers unknown'. It works by computing a safe solution that is in some way the best possible in the relative interior of the feasible set. To certify the relative interior, we employ exact arithmetic, whose use is nevertheless limited in general to critical places, allowing us to rnremain computationally efficient. Moreover, when certain conditions are fulfilled, our method is able to deliver a provable bound on the objective value of the linear program. We test our algorithm on typical benchmark sets and obtain higher rates of success compared to previous approaches for this problem, while keeping the running times acceptably small. The computed objective value bounds are in most of the cases very close to the known exact objective values. We prove the usability of the method we developed by additionally employing a variant of it in a different scenario, namely to improve the results of a Satisfiability Modulo Theories solver. Our method is used as a black box in the nodes of a branch-and-bound tree to implement conflict learning based on the certificate of infeasibility for linear programs consisting of subsets of linear constraints. The generated conflict clauses are in general small and give good rnprospects for reducing the search space. Compared to other methods we obtain significant improvements in the running time, especially on the large instances.