Rational manipulation of mRNA folding free energy allows rheostat control of pneumolysin production by Streptococcus pneumoniae

Rational manipulation of mRNA folding free energy allows rheostat control of pneumolysin production by Streptococcus pneumoniae

Free-standing multilayered membranes based on graphene and natural polymers for biomedical applications

Dissertação de mestrado integrado em Engenharia Biomédica (área de especialização em Biomateriais, Reabilitação e Biomecânica)

Utilização de gás natural comprimido em veículos pesados de passageiros

Dissertação de mestrado em Engenharia Mecânica

MemoBoard familiar

Dissertação de mestrado integrado em Engenharia e Gestão de Sistemas de Informação

ADSNARK: Nearly practical and privacy-preserving proofs on authenticated data

We study the problem of privacy-preserving proofs on authenticated data, where a party receives data from a trusted source and is requested to prove computations over the data to third parties in a correct and private way, i.e., the third party learns no information on the data but is still assured that the claimed proof is valid. Our work particularly focuses on the challenging requirement that the third party should be able to verify the validity with respect to the specific data authenticated by the source — even without having access to that source. This problem is motivated by various scenarios emerging from several application areas such as wearable computing, smart metering, or general business-to-business interactions. Furthermore, these applications also demand any meaningful solution to satisfy additional properties related to usability and scalability. In this paper, we formalize the above three-party model, discuss concrete application scenarios, and then we design, build, and evaluate ADSNARK, a nearly practical system for proving arbitrary computations over authenticated data in a privacy-preserving manner. ADSNARK improves significantly over state-of-the-art solutions for this model. For instance, compared to corresponding solutions based on Pinocchio (Oakland’13), ADSNARK achieves up to 25× improvement in proof-computation time and a 20× reduction in prover storage space.

Exploring scenario exploration

Model finders are very popular for exploring scenarios, helping users validate specifications by navigating through conforming model instances. To be practical, the semantics of such scenario exploration operations should be formally defined and, ideally, controlled by the users, so that they are able to quickly reach interesting scenarios. This paper explores the landscape of scenario exploration operations, by formalizing them with a relational model finder. Several scenario exploration operations provided by existing tools are formalized, and new ones are proposed, namely to allow the user to easily explore very similar (or different) scenarios, by attaching preferences to model elements. As a proof-of-concept, such operations were implemented in the popular Alloy Analyzer, further increasing its usefulness for (user-guided) scenario exploration.

A new page on the road book of inorganic mercury in fish body - tissue distribution and elimination following waterborne exposure and post-exposure periods

prova tipográfica / uncorrected proof

A Prova por reconhecimento de pessoas produzida ex novo em sede de audiência de julgamento: fiabilidade e impacto na descoberta da verdade material

Dissertação de mestrado em Direito Judiciário (Direitos Processuais e Organização Judiciária)

Mobilidade geográfica dos trabalhadores e implicações processuais

Dissertação de mestrado em Direito Judiciário

Microfluidic based on aqueous two-phase system for plasmidic DNA purification

Dissertação de mestrado em Bioquímica Aplicada (área de especialização em Biotecnologia)

BIOMedical search engine framework: lightweight and customized implementation of domain-specific biomedical search engines

The Smart Drug Search is publicly accessible at http://sing.ei.uvigo.es/sds/. The BIOMedical Search Engine Framework is freely available for non-commercial use at https://github.com/agjacome/biomsef

A aprendizagem de tópicos da circunferência com recurso ao GeoGebra: uma experiência com alunos do 9.º ano de escolaridade

Relatório de estágio de mestrado em Ensino de Matemática no 3.º ciclo do Ensino Básico e no Ensino Secundário

Anaerobic oxidation of methane associated with sulfate reduction in a natural freshwater gas source

The occurrence of anaerobic oxidation of methane (AOM) and trace methane oxidation (TMO) was investigated in a freshwater natural gas source. Sediment samples were taken and analyzed for potential electron acceptors coupled to AOM. Long-term incubations with 13C-labeled CH4 (13CH4) and different electron acceptors showed that both AOM and TMO occurred. In most conditions, 13C-labeled CO2 (13CO2) simultaneously increased with methane formation, which is typical for TMO. In the presence of nitrate, neither methane formation nor methane oxidation occurred. Net AOM was measured only with sulfate as electron acceptor. Here, sulfide production occurred simultaneously with 13CO2 production and no methanogenesis occurred, excluding TMO as a possible source for 13CO2 production from 13CH4. Archaeal 16S rRNA gene analysis showed the highest presence of ANME-2a/b (ANaerobic MEthane oxidizing archaea) and AAA (AOM Associated Archaea) sequences in the incubations with methane and sulfate as compared with only methane addition. Higher abundance of ANME-2a/b in incubations with methane and sulfate as compared with only sulfate addition was shown by qPCR analysis. Bacterial 16S rRNA gene analysis showed the presence of sulfate-reducing bacteria belonging to SEEP-SRB1. This is the first report that explicitly shows that AOM is associated with sulfate reduction in an enrichment culture of ANME-2a/b and AAA methanotrophs and SEEP-SRB1 sulfate reducers from a low-saline environment.

Verificación de Sistemas Basada en Teoría de Tipos. System verification in type theory

Este proyecto se enmarca en la utlización de métodos formales (más precisamente, en la utilización de teoría de tipos) para garantizar la ausencia de errores en programas. Por un lado se plantea el diseño de nuevos algoritmos de chequeo de tipos. Para ello, se proponen nuevos algoritmos basados en la idea de normalización por evaluación que sean extensibles a otros sistemas de tipos. En el futuro próximo extenderemos resultados que hemos conseguido recientemente [16,17] para obtener: una simplificación de los trabajos realizados para sistemas sin regla eta (acá se estudiarán dos sistemas: a la Martin Löf y a la PTS), la formulación de estos chequeadores para sistemas con variables, generalizar la noción de categoría con familia utilizada para dar semántica a teoría de tipos, obtener una formulación categórica de la noción de normalización por evaluación y finalmente, aplicar estos algoritmos a sistemas con reescrituras. Para los primeros resultados esperados mencionados, nos proponemos como método adaptar las pruebas de [16,17] a los nuevos sistemas. La importancia radica en que permitirán tornar más automatizables (y por ello, más fácilmente utilizables) los asistentes de demostración basados en teoría de tipos. Por otro lado, se utilizará la teoría de tipos para certificar compiladores, intentando llevar adelante la propuesta nunca explorada de [22] de utilizar un enfoque abstracto basado en categorías funtoriales. El método consistirá en certificar el lenguaje "Peal" [29] y luego agregar sucesivamente funcionalidad hasta obtener Forsythe [23]. En este período esperamos poder agregar varias extensiones. La importancia de este proyecto radica en que sólo un compilador certificado garantiza que un programa fuente correcto se compile a un programa objeto correcto. Es por ello, crucial para todo proceso de verificación que se base en verificar código fuente. Finalmente, se abordará la formalización de sistemas con session types. Los mismos han demostrado tener fallas en sus formulaciones [30], por lo que parece conveniente su formalización. Durante la marcha de este proyecto, esperamos tener alguna formalización que dé lugar a un algoritmo de chequeo de tipos y a demostrar las propiedades usuales de los sistemas. La contribución es arrojar un poco de luz sobre estas formulaciones cuyos errores revelan que el tema no ha adquirido aún suficiente madurez o comprensión por parte de la comunidad. This project is about using type theory to garantee program correctness. It follows three different directions: 1) Finding new type-checking algorithms based on normalization by evaluation. First, we would show that recent results like [16,17] extend to other type systems like: Martin-Löf´s type theory without eta rule, PTSs, type systems with variables (in addition to systems in [16,17] which are a la de Bruijn), systems with rewrite rules. This will be done by adjusting the proofs in [16,17] so that they apply to such systems as well. We will also try to obtain a more general definition of categories with families and normalization by evaluation, formulated in categorical terms. We expect this may turn proof-assistants more automatic and useful. 2) Exploring the proposal in [22] to compiler construction for Algol-like languages using functorial categories. According to [22] such approach is suitable for verifying compiler correctness, claim which was never explored. First, the language Peal [29] will be certified in type theory and we will gradually add funtionality to it until a correct compiler for the language Forsythe [23] is obtained. 3) Formilizing systems for session types. Several proposals have shown to be faulty [30]. This means that a formalization of it may contribute to the general understanding of session types.

Estudos experimentais sôbre a origem do milho

1) It may seem rather strange that, in spite of the efforts of a considerable number of scientists, the problem of the origin of indian corn or maize still has remained an open question. There are no fossil remains or archaeological relics except those which are quite identical with types still existing. (Fig. 1). The main difficulty in finding the wild ancestor- which may still exist - results from the fact that it has been somewhat difficult to decide what it should be like and also where to look for it. 2) There is no need to discuss the literature since an excellent review has recently been published by MANGELSDORF and REEVES (1939). It may be sufficient to state that there are basically two hypotheses, that of ST. HILAIRE (1829) who considered Brazilian pod corn as the nearest relative of wild corn still existing, and that of ASCHERSON (1875) who considered Euchlaena from Central America as the wild ancestor of corn. Later hypotheses represent or variants of these two hypotheses or of other concepts, howewer generally with neither disproving their predecessors nor showing why the new hypotheses were better than the older ones. Since nearly all possible combinations of ideas have thus been put forward, it har- dly seems possible to find something theoretically new, while it is essential first to produce new facts. 3) The studies about the origin of maize received a new impulse from MANGELSDORF and REEVES'S experimental work on both Zea-Tripsacum and Zea-Euchlaena hybrids. Independently I started experiments in 1937 with the hope that new results might be obtained when using South American material. Having lost priority in some respects I decided to withold publication untill now, when I can put forward more concise ideas about the origin of maize, based on a new experimental reconstruction of the "wild type". 4) The two main aspects of MANGELSDORF and REEVES hypothesis are discussed. We agree with the authors that ST. HILAIRE's theory is probably correct in so far as the tunicata gene is a wild type relic gene, but cannot accept the reconstruction of wild corn as a homozygous pod corn with a hermaphroditic tassel. As shown experimentally (Fig. 2-3) these tassels have their central spike transformed into a terminal, many rowed ear with a flexible rachis, while possessing at the same time the lateral ear. Thus no explanation is given of the origin of the corn ear, which is the main feature of cultivated corn (BRIEGER, 1943). The second part of the hypothesis referring to the origin of Euchlaena from corn, inverting thus ASCHERSON's theory, cannot be accepted for several reasons, stated in some detail. The data at hand justify only the conclusion that both genera, Euchlaena and Zea, are related, and there is as little proof for considering the former as ancestor of the latter as there is for the new inverse theory. 5) The analysis of indigenous corn, which will be published in detail by BRIEGER and CUTLER, showed several very primitive characters, but no type was found which was in all characters sufficiently primitive. A genetical analysis of Paulista Pod Corn showed that it contains the same gene as other tunicates, in the IV chromosome, the segregation being complicated by a new gametophyte factor Ga3. The full results of this analysis shall be published elsewhere. (BRIEGER). Selection experiments with Paulista Pod Corn showed that no approximation to a wild ancestor may be obtained when limiting the studies to pure corn. Thus it seemed necessary to substitute "domesticated" by "wild type" modifiers, and the only means for achieving this substitution are hybridizations with Euchlaena. These hybrids have now been analysed init fourth generation, including backcrosses, and, again, the full data will be published elsewhere, by BRIEGER and ADDISON. In one present publication three forms obtained will be described only, which represent an approximation to wild type corn. 6) Before entering howewer into detail, some arguments against ST. HILAIRE's theory must be mentioned. The premendelian argument, referring to the instability of this character, is explained by the fact that all fertile pod corn plants are heterozygous for the dominant Tu factor. But the sterility of the homozygous TuTu, which phenotypically cannot be identified, is still unexplained. The most important argument against the acceptance of the Tunicata faetor as wild type relic gene was removed recently by CUTLER (not yet published) who showed that this type has been preserved for centuries by the Bolivian indians as a mystical "medicine". 7) The main botanical requirements for transforming the corn ear into a wild type structure are stated, and alternative solutions given. One series of these characters are found in Tripsacum and Euchlaena : 2 rows on opposite sides of the rachis, protection of the grains by scales, fragility of the rachis. There remains the other alternative : 4 rows, possibly forming double rows of female and male spikelets, protection of kernels by their glumes, separation of grains at their base from the cob which is thin and flexible. 8) Three successive stages in the reconstruction of wild corn, obtained experimentally, are discussed and illustrated, all characterized by the presence of the Tu gene. a) The structure of the Fl hybrids has already been described in 1943. The main features of the Tunicata hybrids (Fig. -8), when compared with non-tunicate hybrids (Fig. 5-6), consist in the absence of scaly protections, the fragility of the rachis and finally the differentiation of the double rows into one male and one female spikelet. As has been pointed out, these characters represent new phenotypic effects of the tunicate factor which do not appear in the presence of pure maize modifiers. b) The next step was observed among the first backcross to teosinte (Fig. 9). As shown in the photography, Fig. 9D, the features are essencially those of the Fl plants, except that the rachis is more teosinte like, with longer internodes, irregular four-row-arrangement and a complete fragility on the nodes. c) In the next generation a completely new type appeared (Fig. 10) which resembles neither corn nor teosinte, mainly in consequence of one character: the rachis is thin and flexible and not fragile, while the grains have an abscission layer at the base, The medium sized, pointed, brownish and hard granis are protected by their well developed corneous glumes. This last form may not yet be the nearest approach to a wild grass, and I shall try in further experiments to introduce other changes such as an increase of fertile flowers per spikelet, the reduction of difference between terminal and lateral inflorescences, etc.. But the nature of the atavistic reversion is alveadwy such that it alters considerably our expectation when looking for a still existing wild ancestor of corn. 9) The next step in our deductions must now consist in an reversion of our question. We must now explain how we may obtain domesticated corn, starting from a hypothetical wild plant, similar to type c. Of the several changes which must have been necessary to attract the attention of the Indians, the following two seem to me the most important: the disappearance of all abscission layers and the reduction of the glumes. This may have been brought about by an accumulation of mutations. But it seems much more probable to assume that some crossing with a tripsacoid grass or even with Tripsacum australe may have been responsible. In such a cross, the two types of abscission layer would be counterbalanced as shown by the Flhybrids of corn, Tripsacum and Euchlaena. Furthermore in later generations a.tu-allele of Tripsacum may become homozygous and substitute the wild tunicate factor of corn. The hypothesis of a hybrid origin of cultivated corn is not completely new, but has been discussed already by HARSHBERGER and COLLINS. Our hypothesis differs from that of MANGELSDORF and REEVES who assume that crosses with Tripsacum are responsible only for some features of Central and North American corn. 10) The following arguments give indirects evidence in support of our hypothesis: a) Several characters have been observed in indigenous corn from the central region of South America, which may be interpreted as "tripsacoid". b) Equally "zeoid" characters seem to be present in Tripsacum australe of central South-America. c) A system of unbalanced factors, combined by the in-tergeneric cross, may be responsible for the sterility of the wild type tunicata factor when homozygous, a result of the action of modifiers, brought in from Tripsacum together with the tuallele. d) The hybrid theory may explain satisfactorily the presence of so many lethals and semilethals, responsible for the phenomenon of inbreeding in cultivated corn. It must be emphasized that corn does not possess any efficient mechanism to prevent crossing and which could explain the accumulation of these mutants during the evolutionary process. Teosinte which'has about the same mechanism of sexual reproduction has not accumulated such genes, nor self-sterile plants in spite of their pronounced preference for crossing. 11) The second most important step in domestication must have consisted in transforming a four rowed ear into an ear with many rows. The fusion theory, recently revived byLANGHAM is rejected. What happened evidently, just as in succulent pXants (Cactus) or in cones os Gymnosperms, is that there has been a change in phyllotaxy and a symmetry of longitudinal rows superimposed on the original spiral arrangement. 12) The geographical distribution of indigenous corn in South America has been discussed. So far, we may distinguish three zones. The most primitive corn appears in the central lowlands of what I call the Central Triangle of South America: east of the Andies, south of the Amazone-Basin, Northwest of a line formed by the rivers São Prancisco-Paraná and including the Paraguay-Basin. The uniformity of the types found in this extremely large zone is astonishing (BRIEGER and CUTLER). To the west, there is the well known Andian region, characterized by a large number of extremely diverse types from small pop corn to large Cuszco, from soft starch to modified sweet corn, from large cylindrical ears to small round ears, etc.. The third region extends along the atlantic coast in the east, from the Caribean Sea to the Argentine, and is characterized by Cateto, an orange hard flint corn. The Andean types must have been obtained very early, and undoubtedly are the result of the intense Inca agriculture. The Cateto type may be obtained easily by crosses, for instance, of "São Paulo Pointed Pop" to some orange soft corn of the central region. The relation of these three South American zones to Central and North America are not discussed, and it seems essential first to study the intermediate region of Ecuador, Colombia and Venezuela. The geograprical distribution of chromosome knobs is rapidly discussed; but it seems that no conclusions can be drawn before a large number of Tripsacum species has been analysed.