Proposta teórico-interpretativa em sexualidade infantil: contribuição à educação sexual a partir da Grounded Theory

Pós-graduação em Educação Escolar - FCLAR

História e natureza da ciência no ensino de biologia: perfil e concepções de professores em serviço e de materiais didáticos

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

A gestão do fluxo das informações contábeis-financeiras como subsídio do processo de decisão: estudo de caso em uma instituição de ensino superior do terceiro setor

Pós-graduação em Ciência da Informação - FFC

Molecular Analysis of the Differentiation Potential of Murine Mesenchymal Stem Cells from Tissues of Endodermal or Mesodermal Origin

Mesenchymal stem cells (MSCs) have received great attention due to their remarkable regenerative, angiogenic, antiapoptotic, and immunosuppressive properties. Although conventionally isolated from the bone marrow, they are known to exist in all tissues and organs, raising the question on whether they are identical cell populations or have important differences at the molecular level. To better understand the relationship between MSCs residing in different tissues, we analyzed the expression of genes related to pluripotency (SOX2 and OCT-4) and to adipogenic (C/EBP and ADIPOR1), osteogenic (OMD and ALP), and chondrogenic (COL10A1 and TRPV4) differentiation in cultures derived from murine endodermal (lung) and mesodermal (adipose) tissue maintained in different conditions. MSCs were isolated from lungs (L-MSCs) and inguinal adipose tissue (A-MSCs) and cultured in normal conditions, in overconfluence or in inductive medium for osteogenic, adipogenic, or chondrogenic differentiation. Cultures were characterized for morphology, immunophenotype, and by quantitative real-time reverse transcription-polymerase chain reaction for expression of pluripotency genes or markers of differentiation. Bone marrow-derived MSCs were also analyzed for comparison of these parameters. L-MSCs and A-MSCs exhibited the typical morphology, immunophenotype, and proliferation and differentiation pattern of MSCs. The analysis of gene expression showed a higher potential of adipose tissue-derived MSCs toward the osteogenic pathway and of lung-derived MSCs to chondrogenic differentiation, representing an important contribution for the definition of the type of cell to be used in clinical trials of cell therapy and tissue engineering.

Estudo do Padrão Respiratório e Movimento Toracoabdominal em Valvopatia Mitral

FUNDAMENTO: pacientes com valvopatia mitral podem evoluir com congestão pulmonar, que aumenta o trabalho dos músculos respiratórios; essa sobrecarga pode alterar o padrão respiratório com predomínio do deslocamento torácico ou presença de movimentos paradoxais. OBJETIVO: a) estudar o padrão respiratório e movimento toracoabdominal (MTA) em pacientes com doença mitral b) estudar o efeito do posicionamento nos parâmetros respiratórios c) correlacionar hipertensão pulmonar com presença de incoordenação do MTA. MÉTODOS: o padrão respiratório e o MTA de pacientes com doença mitral foram avaliados por pletismografia respiratória por indutância, nas posições dorsal e sentada, durante dois minutos de respiração tranquila. Analisou-se volume corrente (Vc) e tempos respiratórios e as variáveis do MTA. RESULTADOS: de 65 pacientes incluídos, 10 foram retirados, 29 participaram do grupo estenose mitral e 26 do grupo insuficiência mitral. O Vc, a ventilação pulmonar e o fluxo inspiratório médio aumentaram significantemente na posição sentada, sem diferenças entre os grupos. O MTA manteve-se coordenado entre os grupos e as posições; no entanto, cinco pacientes na posição dorsal apresentaram incoordenação (três no grupo estenose mitral; dois no grupo insuficiência mitral) com correlação significante com valores de pressão de artéria pulmonar (r = 0,992, p = 0,007). CONCLUSÃO: o padrão respiratório e o MTA não apresentam diferenças entre pacientes com estenose ou insuficiência mitral. A posição sentada aumenta o Vc sem alterar os tempos respiratórios. A presença de incoordenação toracoabdominal na posição dorsal esteve associação à hipertensão pulmonar.

Diaphragmatic Breathing Training Program Improves Abdominal Motion During Natural Breathing in Patients With Chronic Obstructive Pulmonary Disease: A Randomized Controlled Trial

Yamaguti WP, Claudino RC, Neto AP, Chammas MC, Gomes AC, Salge TM, Moriya HT, Cukier A, Carvalho CR. Diaphragmatic breathing training program improves abdominal motion during natural breathing in patients with chronic obstructive pulmonary disease: a randomized controlled trial. Arch Phys Med Rehabil 2012;93:571-7. Objective: To investigate the effects of a diaphragmatic breathing training program (DBTP) on thoracoabdominal motion and functional capacity in patients with chronic obstructive pulmonary disease. Design: A prospective, randomized controlled trial. Setting: Academic medical center. Participants: Subjects (N=30; forced expiratory volume in Is, 4270 +/- 13% predicted) were randomly allocated to either a training group (TG) or a control group (CG). Interventions: Subjects in the TG completed a 4-week supervised DBTP (3 individualized weekly sessions), while those in the CG received their usual care. Main Outcome Measures: Effectiveness was assessed by amplitude of the rib cage to abdominal motion ratio (RC/ABD ratio) (primary outcome) and diaphragmatic mobility (secondary outcome). The RC/ABD ratio was measured using respiratory inductive plethysmography during voluntary diaphragmatic breathing and natural breathing. Diaphragmatic mobility was measured by ultrasonography. A 6-minute walk test and health-related quality of life were also evaluated. Results: Immediately after the 4-week DBTP, the TG showed a greater abdominal motion during natural breathing quantified by a reduction in the RC/ABD ratio when compared with the CG (F=8.66; P<.001). Abdominal motion during voluntary diaphragmatic breathing after the intervention was also greater in the TG than in the CG (F=4.11; P<.05). The TG showed greater diaphragmatic mobility after the 4-week DBTP than did the CG (F=15.08; P<.001). An improvement in the 6-minute walk test and in health-related quality of life was also observed in the TG. Conclusions: DBTP for patients with chronic obstructive pulmonary disease induced increased diaphragm participation during natural breathing, resulting in an improvement in functional capacity.

Reprogramming of prostate cancer-associated stromal cells to embryonic stem-like

BACKGROUND CD90+ prostate cancer-associated (CP) stromal cells represent a diseased cell type found only in tumor tissue. They differ from their normal counterpart in gene expression and inductive signaling. Genetic reprogramming by induced pluripotent stem (iPS) cell technology can effectively change adult cells into stem-like cells through wholesale alteration of the gene expression program. This technology might be used to erase the abnormal gene expression of diseased cells. The resultant iPS cells would no longer express the disease phenotype, and behave like stem cells. METHODS CP stromal cells, isolated from tumor tissue of a surgically resected prostate by anti-CD90-mediated sorting and cultured in vitro, were transfected with in vitro packaged lentiviral expression vectors containing stem cell transcription factor genes POU5F1, LIN28, NANOG, and SOX2. RESULTS Alkaline phosphatase-positive iPS cells were obtained in about 3 weeks post-transfection at a frequency of 10-4. Their colony morphology was indistinguishable from that of human embryonic stem (ES) cells. Transcriptome analysis showed a virtually complete match in gene expression between the iPS and ES cells. CONCLUSIONS Genes of CP stromal cells could be fully inactivated by genetic reprogramming. As a consequence, the disease phenotype was cured. Prostate 72:14531463, 2012. (c) 2012 Wiley Periodicals, Inc.

Cyclic Voltammetry and Computational Chemistry Studies on the Evaluation of the Redox Behavior of Parabens and other Analogues

Parabens are antimicrobial preservatives widely used in pharmaceutical, cosmetic and food industries. The alkyl chain connected to the ester group defines some important physicochemical characteristics of these compounds, including the partition coefficient and redox properties. The voltammetric and computational analyses were carried out in order to evaluate the redox behavior of these compounds and other phenolic analogues. A strong correlation between chemical substituents inductive effects of parabens with redox potentials was observed. Using cyclic voltammetry and glassy carbon working electrode, only one irreversible anodic peak was observed around 0.8 V for methylparaben (MP), ethylparaben (EP), propylparaben (PP), butylparaben (BP), benzylparaben (BzP) and p-substituted phenolic analogues. The electrodonating inductive effect of alkyl groups was demonstrated by the anodic oxidation potential shift to lower values as the carbon number increases and, therefore the parabens (and other phenolic analogues) oxidation processes to the quinonoidic forms showed great dependence on the substituent pattern.

Cyclic voltammetry and computational chemistry studies on the evaluation of the redox behavior of parabens and other analogues

Parabens are antimicrobial preservatives widely used in pharmaceutical, cosmetic and food industries. The alkyl chain connected to the ester group defines some important physicochemical characteristics of these compounds, including the partition coefficient and redox properties. The voltammetric and computational analyses were carried out in order to evaluate the redox behavior of these compounds and other phenolic analogues. A strong correlation between chemical substituents inductive effects of parabens with redox potentials was observed. Using cyclic voltammetry and glassy carbon working electrode, only one irreversible anodic peak was observed around 0.8 V for methylparaben (MP), ethylparaben (EP), propylparaben (PP), butylparaben (BP), benzylparaben (BzP) and p-substituted phenolic analogues. The electrodonating inductive effect of alkyl groups was demonstrated by the anodic oxidation potential shift to lower values as the carbon number increases and, therefore the parabens (and other phenolic analogues) oxidation processes to the quinonoidic forms showed great dependence on the substituent pattern.

Skyddandets förnuft : En studie om anhöriga till hjälpbehövande äldre som invandrat sent i livet

This dissertation aims to examine and deepen the knowledge of family member caregiving where the care recipient is an elderly person who immigrated late in life. It also aims to contribute to the knowledge of the complexities underlying informal care giving and add to our understandings of what it means to be an immigrant in Sweden. The caregiver is in focus. The research conducted is explorative and partly inductive. The main material used is a qualitative interview study carried out with family members from different countries who are providing informal care to elderly immigrant relatives. The analysis gives three patterns of caregiving. One shows help from informal caregivers only who are not compensated economically. Another shows help from family members who are compensated. The third shows help from family members and staff from the public care system. Three ideal-typical informal caregiver roles show different positions vis-à-vis the new: “guardian”, “filter” and “reinterpreter of traditional care ideals”. Swedish born and immigrated informal caregivers are also compared through analysis of data gathered in telephone interviews with a representative selection of inhabitants in the County of Stockholm. A philosophy of action together with theory on integration and multiculturalism serves as theoretical frameworks to understand discrepancies and ambiguities in the data. Young immigrants experience different integration processes than do the older ones. They strive to protect older family members from changes linked to the migration experience. Talk about dependence on culture underlines family feelings and legitimates the processes of protection. Preconceptions about great differences between Swedish born and immigrant families are not supported by quantitative data. A conclusion is that protection can be understood in relation both to the traditional and the new, the latter in the forms of meetings with Swedish society where unequal relations prevail. It is a kind of counter-strategy where the range of actions is diminished, and thus it has its own logic. Protection can be loosened up when the circumstances change and the range of actions grow.

User interaction widgets for interactive theorem proving

Matita (that means pencil in Italian) is a new interactive theorem prover under development at the University of Bologna. When compared with state-of-the-art proof assistants, Matita presents both traditional and innovative aspects. The underlying calculus of the system, namely the Calculus of (Co)Inductive Constructions (CIC for short), is well-known and is used as the basis of another mainstream proof assistant—Coq—with which Matita is to some extent compatible. In the same spirit of several other systems, proof authoring is conducted by the user as a goal directed proof search, using a script for storing textual commands for the system. In the tradition of LCF, the proof language of Matita is procedural and relies on tactic and tacticals to proceed toward proof completion. The interaction paradigm offered to the user is based on the script management technique at the basis of the popularity of the Proof General generic interface for interactive theorem provers: while editing a script the user can move forth the execution point to deliver commands to the system, or back to retract (or “undo”) past commands. Matita has been developed from scratch in the past 8 years by several members of the Helm research group, this thesis author is one of such members. Matita is now a full-fledged proof assistant with a library of about 1.000 concepts. Several innovative solutions spun-off from this development effort. This thesis is about the design and implementation of some of those solutions, in particular those relevant for the topic of user interaction with theorem provers, and of which this thesis author was a major contributor. Joint work with other members of the research group is pointed out where needed. The main topics discussed in this thesis are briefly summarized below. Disambiguation. Most activities connected with interactive proving require the user to input mathematical formulae. Being mathematical notation ambiguous, parsing formulae typeset as mathematicians like to write down on paper is a challenging task; a challenge neglected by several theorem provers which usually prefer to fix an unambiguous input syntax. Exploiting features of the underlying calculus, Matita offers an efficient disambiguation engine which permit to type formulae in the familiar mathematical notation. Step-by-step tacticals. Tacticals are higher-order constructs used in proof scripts to combine tactics together. With tacticals scripts can be made shorter, readable, and more resilient to changes. Unfortunately they are de facto incompatible with state-of-the-art user interfaces based on script management. Such interfaces indeed do not permit to position the execution point inside complex tacticals, thus introducing a trade-off between the usefulness of structuring scripts and a tedious big step execution behavior during script replaying. In Matita we break this trade-off with tinycals: an alternative to a subset of LCF tacticals which can be evaluated in a more fine-grained manner. Extensible yet meaningful notation. Proof assistant users often face the need of creating new mathematical notation in order to ease the use of new concepts. The framework used in Matita for dealing with extensible notation both accounts for high quality bidimensional rendering of formulae (with the expressivity of MathMLPresentation) and provides meaningful notation, where presentational fragments are kept synchronized with semantic representation of terms. Using our approach interoperability with other systems can be achieved at the content level, and direct manipulation of formulae acting on their rendered forms is possible too. Publish/subscribe hints. Automation plays an important role in interactive proving as users like to delegate tedious proving sub-tasks to decision procedures or external reasoners. Exploiting the Web-friendliness of Matita we experimented with a broker and a network of web services (called tutors) which can try independently to complete open sub-goals of a proof, currently being authored in Matita. The user receives hints from the tutors on how to complete sub-goals and can interactively or automatically apply them to the current proof. Another innovative aspect of Matita, only marginally touched by this thesis, is the embedded content-based search engine Whelp which is exploited to various ends, from automatic theorem proving to avoiding duplicate work for the user. We also discuss the (potential) reusability in other systems of the widgets presented in this thesis and how we envisage the evolution of user interfaces for interactive theorem provers in the Web 2.0 era.

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.

Analyse der temporären Neuroblastenbildung und der segmentalen Spezifizierung des Neuroblasten 6-4 im embryonalen zentralen Nervensystem von Drosophila melanogaster

Die vorliegende Arbeit gewährte neue Einblicke in zwei fundamentale Vorgänge der frühen Neurogenese von Drosophila melanogaster. Der erste Teil untersuchte die zeitliche Spezifizierung der Neuroblastenidentitäten. Durch die Expression verschiedener Gene entlang der Dorsoventral- und der Anterioposteriorachse wird ein kartesisches Koordinatensystem aufgebaut, indem ein Neuroblast (NB), der in einem bestimmten Quadranten entsteht, eine spezifische Identität erhält. Die Delamination der NBs erfolgt in fünf Segregationswellen, wobei in jeder Welle die gleiche Population NBs gebildet wird. In dieser Arbeit konnte nun gezeigt werden, dass es nicht nur einen räumlichen, sondern auch einen zeitlichen Aspekt bei der Entstehung der NBs gibt: So zeigten Transplantationsexperimente, dass sowohl im frühen als auch im späten Neuroektoderm extrinsische induktive Signale an der Spezifizierung der Neuroblastenidentität beteiligt sind. Die Natur dieser Signale bleibt noch unklar. Allerdings stellen die Segmentpolaritätsgene aufgrund ihrer dynamischen Expression eine potenzielle Kandidatengruppe dar. Der zweite Teil beschäftigte sich mit der segmentalen Spezifizierung der Neuroblasten. Für diesen Prozess zeigten frühere Genexpressionsstudien, dass NBs, die zwar an korrespondierenden Positionen innerhalb des kartesischen Systems, aber in unterschiedlichen Segmenten gebildet werden, die gleichen Genexpressionsmuster aufweisen und fast identische Zellstammbäume hervorbringen. Einige dieser seriell homologen NBs generieren jedoch segmentspezifische Zellstammbäume – ein solches Beispiel ist der NB6-4, der als Modellsystem benutzt wurde. Für die thorakale Variante dieses NBs konnte ich zeigen, dass die Homöotischen Gene zur Spezifizierung nicht notwendig sind – thorakales Schicksal ist eine Grundidentität. Diese wird in abdominalen Segmenten jedoch durch die Funktion der Homöotischen Gene abdominal-A (abd-A) und Abdominal-B (Abd-B) in abdominales Schicksal transformiert. Dieser segmentale Unterschied wird durch die Regulation des Zellzyklusgens CycE bewerkstelligen. Genauer: CycE ist notwendig, um neurogliales Schicksal in thorakalen Segmenten zu generieren und ausreichend, dieses Schicksal ebenfalls in abdominalen Segmenten zu erzeugen. Eine direkte Inhibierung der Expression von CycE durch Abd-A in abdominalen Segmenten führt dagegen zu einer differenziellen Expression von CycE im neuronalen thorakalen Anteil des Zellstammbaums. Weiterhin konnten in einem Enhancerelement, das für die Expression von CycE im Nervensystem verantwortlich ist, mehrere Bindestellen für Abd-A und Abd-B gefunden werden. Die gewonnen Daten legen – in Verbindung mit bereits bekannten Ergebnissen – den Schluss nahe, dass diese neuronspezifizierende Funktion von CycE unabhängig von seiner Rolle im Zellzyklus ist.

Does improvisation lead to outcome deviation? A conceptual framework of improvisation, its antecedents and outcome deviation

Management and organization literature has extensively noticed the crucial role that improvisation assumes in organizations, both as a learning process (Miner, Bassoff & Moorman, 2001), a creative process (Fisher & Amabile, 2008), a capability (Vera & Crossan, 2005), and a personal disposition (Hmielesky & Corbett, 2006; 2008). My dissertation aims to contribute to the existing literature on improvisation, addressing two general research questions: 1) How does improvisation unfold at an individual level? 2) What are the potential antecedents and consequences of individual proclivity to improvise? This dissertation is based on a mixed methodology that allowed me to deal with these two general research questions and enabled a constant interaction between the theoretical framework and the empirical results. The selected empirical field is haute cuisine and the respondents are the executive chefs of the restaurants awarded by Michelin Guide in 2010 in Italy. The qualitative section of the dissertation is based on the analysis of 26 inductive case studies and offers a multifaceted contribution. First, I describe how improvisation works both as a learning and creative process. Second, I introduce a new categorization of individual improvisational scenarios (demanded creative improvisation, problem solving improvisation, and pure creative improvisation). Third, I describe the differences between improvisation and other creative processes detected in the field (experimentation, brainstorming, trial and error through analytical procedure, trial and error, and imagination). The quantitative inquiry is founded on a Structural Equation Model, which allowed me to test simultaneously the relationships between proclivity to improvise and its antecedents and consequences. In particular, using a newly developed scale to measure individual proclivity to improvise, I test the positive influence of industry experience, self-efficacy, and age on proclivity to improvise and the negative impact of proclivity to improvise on outcome deviation. Theoretical contributions and practical implications of the results are discussed.

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.