Type inference for conversation types

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

A logical foundation for session-based concurrent computation

Linear logic has long been heralded for its potential of providing a logical basis for concurrency. While over the years many research attempts were made in this regard, a Curry-Howard correspondence between linear logic and concurrent computation was only found recently, bridging the proof theory of linear logic and session-typed process calculus. Building upon this work, we have developed a theory of intuitionistic linear logic as a logical foundation for session-based concurrent computation, exploring several concurrency related phenomena such as value-dependent session types and polymorphic sessions within our logical framework in an arguably clean and elegant way, establishing with relative ease strong typing guarantees due to the logical basis, which ensure the fundamental properties of type preservation and global progress, entailing the absence of deadlocks in communication. We develop a general purpose concurrent programming language based on the logical interpretation, combining functional programming with a concurrent, session-based process layer through the form of a contextual monad, preserving our strong typing guarantees of type preservation and deadlock-freedom in the presence of general recursion and higher-order process communication. We introduce a notion of linear logical relations for session typed concurrent processes, developing an arguably uniform technique for reasoning about sophisticated properties of session-based concurrent computation such as termination or equivalence based on our logical approach, further supporting our goal of establishing intuitionistic linear logic as a logical foundation for sessionbased concurrency.

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.

Verificación de Sistemas Basada en Teoría de Tipos

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.

Long-term follow-up of topical 5-aminolaevulinic acid photodynamic therapy diode laser single session for non-melanoma skin cancer

Photodynamic therapy (PDT) is based on the association of a light source and tight sensitive agents in order to cause the selective death of tumor cells. To evaluate topical 5-aminolaevulinic acid (5-ALA) and diode laser photodynamic single session therapy single session for non-melanoma skin cancer (NMSC), a long-term follow-up was performed. Nineteen Bowen`s disease (BD) and 15 basal cell. carcinoma (BCC) lesions were submitted to 6-h topical and occlusive 20% 5-ALA plus DMSO and EDTA, and later were exposed to 630 nm diode laser, 100 or 300 J cm(-2) dose. At 3 months tumor-free rate was 91.2% (31/34) whereas at 60 months, 57.7% (15/26), slightly higher in BCC (63.6%; 7/11). The relation between the reduction of the clinical response and the increase of tumor dimension observed at 18 months was lost at 60 months. The sBCC recurrence was earlier compared to the nBCC one. ALA-PDT offered important advantages: it is minimally invasive, an option for patients under risk of surgical complications; clinical feasibility; treatment of multiple lesions in only one session or lesions in poor heating sites and superior esthetical results. However, the recurrence rate increase after ALA-PDT diode laser single session can be observed at tong-term follow-up, and the repetitive sessions, an additional. advantage of the method, is strongly recommended. The clinical response and recurrence time seem to be related to the laser light dose and NMSC types/sub-types, thickness and dimension, which must be considered for the choice of the ALA-PDT. (C) 2009 Elsevier B.V. All rights reserved.

Effects of a single habituation session on neuromuscular isokinetic profile at different movement velocities

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Overall and differentiated session ratings of perceived exertion at different time points following a circuit weight training workout

Session ratings of perceived exertion (SRPE) have been considered to provide a quantitative evaluation of the entire exercise session in different types of resistance training. In this study we investigated the ability of SRPE to assess exercise strain in a circuit weight training (CWT) workout and the influence of time lag to report SRPE. Ten healthy male volunteers (22.3±2.8 years, 72.5±6.5kg, and 175±5cm) completed a CWT session involving three circuits of five multiple joint exercises with single sets of 20 repetitions at 30% one repetition maximum (1-RM). Heart rate [63.7-75.0% maximum heart rate (%HRmax)], blood lactate (5.6-7.6mM) as well as overall, chest, and active muscle RPE increased significantly (p<0.05) throughout the CWT, but no significant differences were found between ratings of perceived exertion (RPE) types. Overall, chest and active muscle SRPE were accessed 10 minutes, 20 minutes, and 30 minutes after the workout, with no significant main effects or SRPE type×time interaction being found (p>0.05). Finally, no significant differences (p>0.05) were observed between averaged SRPE and RPE responses (overall: 3.7±0.6 vs. 3.5±0.9; chest: 3.8±0.7 vs. 3.6±0.8; active muscle; 3.7±0.7 vs. 3.5±0.7). These results suggest SRPE, irrespective of the moment at which it is taken, to be a useful tool for assessing global exercise strain in a CWT workout, providing coaches, physicians, and exercisers a practical way for monitoring this type of resistance training. © 2013.

Physical activity in the school setting: cognitive performance is not affected by three different types of acute exercise

Recent studies indicate that a single bout of physical exercise can have immediatepositive effects on cognitive performance of children and adolescents. However, thetype of exercise that affects cognitive performance the most in young adolescents isnot fully understood. Therefore, this controlled study examined the acute effects ofthree types of 12-min classroom-based exercise sessions on information processingspeed and selective attention. The three conditions consisted of aerobic, coordination,and strength exercises, respectively. In particular, this study focused on the feasibilityand efficiency of introducing short bouts of exercise in the classroom. One hundredand ninety five students (5th and 6th grade; 10–13 years old) participated in a doublebaseline within-subjects design, with students acting as their own control. Exercise typewas randomly assigned to each class and acted as between-subject factor. Before andimmediately after both the control and the exercise session, students performed twocognitive tests that measured information processing speed (Letter Digit SubstitutionTest) and selective attention (d2 Test of Attention). The results revealed that exercisingat low to moderate intensity does not have an effect on the cognitive parameters testedin young adolescents. Furthermore, there were no differential effects of exercise type.The results of this study are discussed in terms of the caution which should be takenwhen conducting exercise sessions in a classroom setting aimed at improving cognitive performance.

Phytochemical Markers Of Different Types Of Red Propolis.

Propolis is a resin that bees collect from different plant sources and use in the defense of the bee community. The intricate composition of propolis varies depending on plant sources from different geographic regions and many types have been reported. Red coloured propolis found in several states in Brazil and in other countries has known antimicrobial and antioxidant activity. Different analytical methods have been applied to studies regarding the chemical composition and plant origins of red propolis. In this study samples of red propolis from different regions have been characterised using direct infusion electrospray ionisation mass spectrometry (ESI(-)-MS) fingerprinting. Data from the fingerprints was extracted and analysed by multivariate analysis to group the samples according to their composition and marker compounds. Despite similar colour, the red coloured propolis samples were divided into three groups due to contrasting chemical composition, confirming the need to properly characterise the chemical composition of propolis.

Overlapped Sequence Types (sts) And Serogroups Of Avian Pathogenic (apec) And Human Extra-intestinal Pathogenic (expec) Escherichia Coli Isolated In Brazil.

Avian pathogenic Escherichia coli (APEC) strains belong to a category that is associated with colibacillosis, a serious illness in the poultry industry worldwide. Additionally, some APEC groups have recently been described as potential zoonotic agents. In this work, we compared APEC strains with extraintestinal pathogenic E. coli (ExPEC) strains isolated from clinical cases of humans with extra-intestinal diseases such as urinary tract infections (UTI) and bacteremia. PCR results showed that genes usually found in the ColV plasmid (tsh, iucA, iss, and hlyF) were associated with APEC strains while fyuA, irp-2, fepC sitDchrom, fimH, crl, csgA, afa, iha, sat, hlyA, hra, cnf1, kpsMTII, clpVSakai and malX were associated with human ExPEC. Both categories shared nine serogroups (O2, O6, O7, O8, O11, O19, O25, O73 and O153) and seven sequence types (ST10, ST88, ST93, ST117, ST131, ST155, ST359, ST648 and ST1011). Interestingly, ST95, which is associated with the zoonotic potential of APEC and is spread in avian E. coli of North America and Europe, was not detected among 76 APEC strains. When the strains were clustered based on the presence of virulence genes, most ExPEC strains (71.7%) were contained in one cluster while most APEC strains (63.2%) segregated to another. In general, the strains showed distinct genetic and fingerprint patterns, but avian and human strains of ST359, or ST23 clonal complex (CC), presented more than 70% of similarity by PFGE. The results demonstrate that some zoonotic-related STs (ST117, ST131, ST10CC, ST23CC) are present in Brazil. Also, the presence of moderate fingerprint similarities between ST359 E. coli of avian and human origin indicates that strains of this ST are candidates for having zoonotic potential.

Post Hoc Analysis Of The Patricia Randomized Trial Of The Efficacy Of Human Papillomavirus Type 16 (hpv-16)/hpv-18 As04-adjuvanted Vaccine Against Incident And Persistent Infection With Nonvaccine Oncogenic Hpv Types Using An Alternative Multiplex Type-specific Pcr Assay For Hpv Dna.

The efficacy of the human papillomavirus type 16 (HPV-16)/HPV-18 AS04-adjuvanted vaccine against cervical infections with HPV in the Papilloma Trial against Cancer in Young Adults (PATRICIA) was evaluated using a combination of the broad-spectrum L1-based SPF10 PCR-DNA enzyme immunoassay (DEIA)/line probe assay (LiPA25) system with type-specific PCRs for HPV-16 and -18. Broad-spectrum PCR assays may underestimate the presence of HPV genotypes present at relatively low concentrations in multiple infections, due to competition between genotypes. Therefore, samples were retrospectively reanalyzed using a testing algorithm incorporating the SPF10 PCR-DEIA/LiPA25 plus a novel E6-based multiplex type-specific PCR and reverse hybridization assay (MPTS12 RHA), which permits detection of a panel of nine oncogenic HPV genotypes (types 16, 18, 31, 33, 35, 45, 52, 58, and 59). For the vaccine against HPV types 16 and 18, there was no major impact on estimates of vaccine efficacy (VE) for incident or 6-month or 12-month persistent infections when the MPTS12 RHA was included in the testing algorithm versus estimates with the protocol-specified algorithm. However, the alternative testing algorithm showed greater sensitivity than the protocol-specified algorithm for detection of some nonvaccine oncogenic HPV types. More cases were gained in the control group than in the vaccine group, leading to higher point estimates of VE for 6-month and 12-month persistent infections for the nonvaccine oncogenic types included in the MPTS12 RHA assay (types 31, 33, 35, 45, 52, 58, and 59). This post hoc analysis indicates that the per-protocol testing algorithm used in PATRICIA underestimated the VE against some nonvaccine oncogenic HPV types and that the choice of the HPV DNA testing methodology is important for the evaluation of VE in clinical trials. (This study has been registered at ClinicalTrials.gov under registration no. NCT00122681.).

Mineral Nutrition Of Campos Rupestres Plant Species On Contrasting Nutrient-impoverished Soil Types.

In Brazil, the campos rupestres occur over the Brazilian shield, and are characterized by acidic nutrient-impoverished soils, which are particularly low in phosphorus (P). Despite recognition of the campos rupestres as a global biodiversity hotspot, little is known about the diversity of P-acquisition strategies and other aspects of plant mineral nutrition in this region. To explore nutrient-acquisition strategies and assess aspects of plant P nutrition, we measured leaf P and nitrogen (N) concentrations, characterized root morphology and determined the percentage arbuscular mycorrhizal (AM) colonization of 50 dominant species in six communities, representing a gradient of soil P availability. Leaf manganese (Mn) concentration was measured as a proxy for carboxylate-releasing strategies. Communities on the most P-impoverished soils had the highest proportion of nonmycorrhizal (NM) species, the lowest percentage of mycorrhizal colonization, and the greatest diversity of root specializations. The large spectrum of leaf P concentration and variation in root morphologies show high functional diversity for nutritional strategies. Higher leaf Mn concentrations were observed in NM compared with AM species, indicating that carboxylate-releasing P-mobilizing strategies are likely to be present in NM species. The soils of the campos rupestres are similar to the most P-impoverished soils in the world. The prevalence of NM strategies indicates a strong global functional convergence in plant mineral nutrition strategies among severely P-impoverished ecosystems.