A Logic and tool for local reasoning about security protocols

Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática

Functional and molecular characterization of SR45, a plant-specific factor involved in sugar and stress signaling in Arabidopsis thaliana

Dissertation presented to obtain the Ph.D degree in Molecular Biology

Dissecting cross-talk between microglia and motoneurons in ALS: signaling events and soluble factors

Dissertação para obtenção do Grau de Mestre em Genética Molecular e Biomedicina

Dual track sell-out: Signaling through IPO and Underpricing

A Work Project, presented as part of the requirements for the Award of a Masters Degree in Finance from the NOVA – School of Business and Economics

Exploring motor neuron degeneration in ALS - prevention by glycoursodeoxycholic acid and signaling to microglia

Dissertação para obtenção do Grau de Mestre em Genética Molecular e Biomedicina

Role of Notch signaling on the differentiation of early lymphoid progenitors cells: a view throughout the development of the embryonic chicken thymus and spleen

Dissertação para a obtenção do grau de Mestre em Genética Molecular e Biomedicina

Planning and verification of multipath routing protocols

Conventionally the problem of the best path in a network refers to the shortest path problem. However, for the vast majority of networks present nowadays this solution has some limitations which directly affect their proper functioning, as well as an inefficient use of their potentialities. Problems at the level of large networks where graphs of high complexity are commonly present as well as the appearing of new services and their respective requirements, are intrinsically related to the inability of this solution. In order to overcome the needs present in these networks, a new approach to the problem of the best path must be explored. One solution that has aroused more interest in the scientific community considers the use of multiple paths between two network nodes, where they can all now be considered as the best path between those nodes. Therefore, the routing will be discontinued only by minimizing one metric, where only one path between nodes is chosen, and shall be made by the selection of one of many paths, thereby allowing the use of a greater diversity of the present paths (obviously, if the network consents). The establishment of multi-path routing in a given network has several advantages for its operation. Its use may well improve the distribution of network traffic, improve recovery time to failure, or it can still offer a greater control of the network by its administrator. These factors still have greater relevance when networks have large dimensions, as well as when their constitution is of high complexity, such as the Internet, where multiple networks managed by different entities are interconnected. A large part of the growing need to use multipath protocols is associated to the routing made based on policies. Therefore, paths with different characteristics can be considered with equal level of preference, and thus be part of the solution for the best way problem. To perform multi-path routing using protocols based only on the destination address has some limitations but it is possible. Concepts of graph theory of algebraic structures can be used to describe how the routes are calculated and classified, enabling to model the routing problem. This thesis studies and analyzes multi-path routing protocols from the known literature and derives a new algebraic condition which allows the correct operation of these protocols without any network restriction. It also develops a range of software tools that allows the planning and the respective verification/validation of new protocols models according to the study made.

Trans-Synaptic Signaling by Activity-Dependent Cleavage of Neuroligin-1

Throughout the brain, patterns of activity in postsynaptic neurons influence the properties of synaptic inputs. Such feedback regulation is central to neural network stability that underlies proper information processing and feature representation in the central nervous system. At the cellular level, tight coupling of presynaptic and postsynaptic function is fundamental to neural computation and synaptic plasticity. The cohort of protein complexes at the pre and postsynaptic membrane allows for tight synapse-specific segregation and integration of diverse molecular and electrical signals.(...)

The role of Hedgehog signaling during zebrafish larvae fin fold regeneration

Several studies have demonstrated that although the structure of the adult and larval zebrafish caudal fin is different, there are similarities at the cellular and molecular level that turn larval zebrafish fin fold a useful model to study the basic principles of regeneration. In this process, while the essential role for Hedgehog (Hh) signaling is well established in the adult zebrafish caudal fin system, its involvement in juvenile tissue regeneration is still unknown. The aim of this Master thesis was therefore to evaluate the contribution of the Hh signaling pathway to the larval zebrafish fin fold regeneration process. Accordingly, we analyzed the expression of several Hh signaling components through in situ hybridization. Here, we showed that several of these genes are effectively expressed in the larval regenerating fin tissue, suggesting a role for Hh signaling also during larval regeneration. However, divergence in the regulation of few Hh signaling components appears to exist between the adult and larval zebrafish fin regeneration processes. Nevertheless, similarly to adult caudal fin regeneration, when Hh signaling was blocked, by using cyclopamine, the larval fin fold regenerative outgrowth is severely impaired. Since larval zebrafish fin fold is ciliated, and primary cilia are closely related to Hh signaling regulation in vertebrate systems, we further addressed the role of primary cilia during larval fin fold regeneration process. To this end, we used the zebrafish iguana mutant, in which primary cilia are not formed, to study the modulation of Hh signaling expression during larval fin fold regeneration in the absence of primary cilia. Here, we found that several genes were expressed with a delay, coincident with the delay in the mutant fin fold regeneration observed in previous work. We show that Hh signaling in the fin fold is crucial to promote cell proliferation. When Hh signaling is blocked using cyclopamine there is a strong blockage of cell proliferation and regeneration is also blocked. Surprisingly, in iguana mutants where Hh signaling is impaired but not totally blocked, cell proliferation is not detected but regeneration still occurs. This raises the question about the requirement of cell proliferation in larvae fin fold regeneration. By blocking the cell cycle using aphidicolin we demonstrate that cell proliferation is not necessary for zebrafish larvae fin fold regeneration.

Primary cilia and the regulation of hedgehog signaling: link to cardiac development

RESUMO: As células eucarióticas evoluíram um sistema de sinalização complexo que lhes permite responder aos sinais extracelulares e intracelulares. Desta forma, as vias de sinalização são essenciais para a sobrevivência da célula e do organismo, uma vez que regulam processos fundamentais, tais como o desenvolvimento, o crescimento, a imunidade, e a homeostase dos tecidos. A via de transdução de sinal Hedgehog (Hh) envolve o receptor Patched1 (Ptch1), que tem um efeito inibidor sobre a proteína Smoothened (Smo) na ausência dos seus ligandos, as proteínas Sonic hedgehog (Shh). Estas proteínas são reguladores fundamentais do desenvolvimento embrionário, como ilustrado pelas malformações drásticas observadas em embriões humanos e de murganho com perturbações da transdução de sinal da via Hh e que incluem polidactilia, defeitos craniofaciais e malformações ósseas. Igualmente importantes são as consequências da ativação inapropriada da via de sinalização Hh na formação de tumores. Curiosamente, os componentes desta via localizam-se nos cílios primários. Além disso, demonstrou-se que esta localização é crucial para a sinalização através da via Hh. Na presença dos ligandos, Ptch1 é internalizado e destinado a degradação ou sequestrado num compartimento da célula de onde não pode desempenhar o seu papel inibitório. A proteína Arl13b é uma pequena GTPase pertencente à família Arf/Arl da superfamília Ras de pequenas GTPases e foi implicada no síndrome de Joubert, uma ciliopatia caracterizada por ataxia congénita cerebelar, hipotonia, atrso mental e cardiopatia congénita. Murganhos deficientes para Arl13b, chamado hennin (hnn) morrem morrem prematuramente ao dia 13,5 de gestação (E13,5) e exibem anomalias morfológicas nos cílios que levam à interrupção da sinalização Hh. Além disso, a Arl13b está diretamente envolvida na regulação da via Hh, controlando a localização de vários componentes desta via nos cílios primários. Neste trabalho, mostramos que a Arl13b se localiza em circular dorsal ruffles (CDRs), que são estruturas de actina envolvidas em macropinocitose e internalização de recetores, e que regula a sua formação. Além disso, aprofundámos o conhecimento do processo de ativação da via de sinalização Hh, mostrando que as CDRs sequestram seletivamente e internalizam o recetor Ptch1. As CDRs formam-se minutos após ativação da via por ligandos Shh ou pelo agonista de Smo SAG e continuam a ser formadas a partir daí, sugerindo uma indução contínua da reorganização do citoesqueleto de actina quando a via está ativada. Observámos ainda que a inibição da formação de CDRs através do silenciamento de WAVE1, uma proteína necessária para a formação destas estruturas, resulta na diminuição da ativação da via de sinalização Hh. Além disso, o bloqueio da macropinocitose, que se segue ao fecho das CDRs, através do silenciamento de uma proteína necessária para a cisão de macropinossomas, nomeadamente a proteína BARS, tem um efeito semelhante. Estes resultados sugerem que as CDRs e a macropinocitose são necessárias para a ativação da via de sinalização Hh e indicam que esta via de internalização controla os níveis de sinal Hh. Durante o desenvolvimento, as células proliferativas dependem do cílio primário para a transdução de várias vias de sinalização. A via Hh induz a diferenciação do músculo cardíaco. Por conseguinte, os murganhos deficientes na via de sinalização Hh exibem uma variedade de defeitos de lateralidade, incluindo alteração do looping do coração, como pode ser visto em murganhos deficientes para Arl13b. Por conseguinte, investigámos o papel da Arl13b no desenvolvimento do coração. Mostramos que a Arl13b é altamente expressa no coração de embriões de murganho e de murganhos adultos ao nível do mRNA e da proteína. Além disso, o perfil de distribuição da Arl13b no coração segue o dos cílios primários, que são essenciais para o desenvolvimento cardíaco. Corações de murganhos hnn no estadio E12,5 mostram um canal átrio-ventricular aberto, espessamento da camada compacta ventricular e aumento do índice mitótico no ventrículo esquerdo. Além disso, um atraso de 1 a 2 dias no desenvolvimento é observado em corações de murganhos hnn, quando comparados com controlos selvagens no estadio E13,5. Assim, estes resultados sugerem que a Arl13b é necessária para o desenvolvimento embrionário do coração e que defeitos cardíacos podem contribuir para a letalidade embrionária de murganhos hnn. Em suma, foi estabelecido um novo mecanismo para a regulação dos níveis de superfície do recetor Ptch1, que envolve a remodelação do citoesqueleto de actina e a formação de CDRs após a ativação da via de sinalização Hh. Este mecanismo permite um feedback negativo que evita a repressão excessiva da via através da remoção de Ptch1 da superfície da célula. Além disso, determinou-se que uma mutação de perda de função na Arl13b causa defeitos cardíacos durante o desenvolvimento, possivelmente relacionados com a associação dos defeitos em cílios primários e na sinalização Hh, existentes em murganhos deficientes para Arl13b. A via de sinalização Hh tem tido um papel central entre as vias de sinalização, uma vez que a sua regulação é crucial para o funcionamento apropriada da célula. Assim, a descoberta de um novo mecanismo de tráfego através de macropinocitose e CDRs que controla a ativação e repressão da via de sinalização Hh traz novas perspetivas de como esta via pode ser regulada e pode ainda conduzir à identificação de novos alvos e estratégias terapêuticas. --------------------ABSTRACT: Eukaryotic cells have evolved a complex signaling system that allows them to respond to extracellular and intracellular cues. Signaling pathways are essential for cell and organism survival, since they regulate fundamental processes such as development, growth, immunity, and tissue homeostasis. The Hedgehog (Hh) pathway of signal transduction involves the receptor Patched1 (Ptch1), which has an inhibitory effect on Smoothened (Smo) in the absence of its ligands, the Sonic hedgehog (Shh) proteins. These proteins are fundamental regulators of embryonic development, as illustrated by the dramatic malformations seen in human and mouse embryos with perturbed Hh signal transduction that include polydactyly, craniofacial defects and skeletal malformations. Equally important are the consequences of inappropriate activation of the Hh signaling response in tumor formation. Interestingly, the components of this pathway localize to primary cilia. Moreover, it has been shown that this localization is crucial for Hh signaling. However, in the presence of the ligands, Ptch1 is internalized and destined for degradation or sequestered in a cell compartment where it no longer can play its inhibitory role. ADP-ribosylation factor-like (Arl) 13b, a small GTPase belonging to Arf/Arl family of the Ras superfamily of small GTPases has been implicated in Joubert syndrome, a ciliopathy characterized by congenital cerebellar ataxia, hypotonia, intellectual disability and congenital heart disease. Arl13b-deficient mice, called hennin (hnn) die at embryonic day 13.5 (E13.5) and display morphological abnormalities in primary cilia that lead to the disruption of Hh signaling. Furthermore, Arl13b is directly involved in the regulation of Hh signaling by controlling the localization of several components of this pathway to primary cilia. Here, we show that Arl13b localizes to and regulates the formation of circular dorsal rufles (CDRs), which are actin-basedstructures known to be involved in macropinocytosis and receptor internalization. Additionally, we extended the knowledge of the Hh signaling activation process by showing that CDRs selectively sequester and internalize Ptch1 receptors. CDRs are formed minutes after Hh activation by Shh ligands or the Smo agonist SAG and keep being formed thereafter, suggesting a continuous induction of actin reorganization when the pathway is switched on. Importantly, we observed that disruption of CDRs by silencing WAVE1, a protein required for CDR formation, results in down-regulation of Hh signaling activation. Moreover, the blockade of macropinocytosis, which follows CDR closure, through silencing of a protein necessary for the fission of macropinosomes, namely BARS has a similar effect. These results suggest that CDRs and macropinocytosis are necessary for activation of Hh signaling and indicate that this pathway of internalization controls Hh signal levels. During development, proliferating cells rely on the primary cilium for the transduction of several signaling pathways. Hh induces the differentiation of cardiac muscle. Accordingly, Hh-deficient mice display a variety of laterality defects, including alteration of heart looping, as seen in Arl13b-deficient mice. Therefore, we investigated the role of Arl13b in heart development. We show that Arl13b is highly expressed in the heart of both embryonic and adult mice at mRNA and protein levels. Also, Arl13b localization profile mimics that of primary cilia, which have been shown to be essential to early heart development. E12.5 hnn hearts show an open atrioventricular channel, increased thickening of the ventricular compact layer and increased mitotic index in the left ventricle. Moreover, a delay of 1 to 2 days in development is observed in hnn hearts, when compared to wild-type controls at E13.5. Hence, these results suggest that Arl13b is necessary for embryonic heart development and that cardiac defects might contribute to the embryonic lethality of hnn mice. Altogether, we established a novel mechanism for the regulation of Ptch1 surface levels, involving cytoskeleton remodeling and CDR formation upon Hh signaling activation. This mechanism allows a negative feedback loop that prevents excessive repression of the pathway by removing Ptch1 from the cell surface. Additionally, we determined that the Arl13b loss-offunction mutation causes cardiac defects during development, possibly related to the associated ciliary and Hh signaling defects found in Arl13b-deficient mice. Hh signaling has taken a center stage among the signaling pathways since its regulation is crucial for the appropriate output and function of the cell. Hence, the finding of a novel trafficking mechanism through CDRs and macropinocytosis that controls Hh signaling activation and repression brings new insights to how this pathway can be regulated and can lead to the discovery of novel therapeutic targets and strategies.

Rely-guarantee protocols for safe interference over shared memory

Mutable state can be useful in certain algorithms, to structure programs, or for efficiency purposes. However, when shared mutable state is used in non-local or nonobvious ways, the interactions that can occur via aliases to that shared memory can be a source of program errors. Undisciplined uses of shared state may unsafely interfere with local reasoning as other aliases may interleave their changes to the shared state in unexpected ways. We propose a novel technique, rely-guarantee protocols, that structures the interactions between aliases and ensures that only safe interference is possible. We present a linear type system outfitted with our novel sharing mechanism that enables controlled interference over shared mutable resources. Each alias is assigned separate, local roles encoded in a protocol abstraction that constrains how an alias can legally use that shared state. By following the spirit of rely-guarantee reasoning, our rely-guarantee protocols ensure that only safe interference can occur but still allow many interesting uses of shared state, such as going beyond invariant and monotonic usages. This thesis describes the three core mechanisms that enable our type-based technique to work: 1) we show how a protocol models an alias’s perspective on how the shared state evolves and constrains that alias’s interactions with the shared state; 2) we show how protocols can be used while enforcing the agreed interference contract; and finally, 3) we show how to check that all local protocols to some shared state can be safely composed to ensure globally safe interference over that shared memory. The interference caused by shared state is rooted at how the uses of di↵erent aliases to that state may be interleaved (perhaps even in non-deterministic ways) at run-time. Therefore, our technique is mostly agnostic as to whether this interference was the result of alias interleaving caused by sequential or concurrent semantics. We show implementations of our technique in both settings, and highlight their di↵erences. Because sharing is “first-class” (and not tied to a module), we show a polymorphic procedure that enables abstract compositions of protocols. Thus, protocols can be specialized or extended without requiring specific knowledge of the interference produce by other protocols to that state. We show that protocol composition can ensure safety even when considering abstracted protocols. We show that this core composition mechanism is sound, decidable (without the need for manual intervention), and provide an algorithm implementation.