Thèses (M.Sc.)--Université de Sherbrooke (Canada), 2000. / Titre de l'écran-titre (visionné le 20 juin 2006). Publié aussi en version papier.

Thèses (M.Sc.)--Université de Sherbrooke (Canada), 2002. / Titre de l'écran-titre (visionné le 20 juin 2006). Publié aussi en version papier.

Thèse (M.Sc.)--Université Laval, 2003. / Titre de l'écran-titre (visionné le 29 mars 2004). Bibliogr.

Thèse (LL.D.)--Université Laval, 2001. / Bibliogr.: t. 2, f. 534-559. Webographie: t. 2, f. 560-567. Publié aussi en version électronique.

Th. 3e cycle--Sci. de matér.--Toulouse--I.N.P., 1985. N°: 253.

Texte remanié de: Doct. diss.--University of London, 1991. / Bibliogr. p. 269-295. Index.

Th. doct.-ing.--Sci. agron.--Nancy--I.N.P.L., 1981.

Th. 3e cycle--Chim. macromoléculaire--Lille 1, 1978. N°: 690.

Le stress prenatal augmente la vulnerabilIte a certames substances d abus chez le rat. L objectif de cette thèse était de déterminer si un stress subit in utero pouvait moduler durablement la vulnérabilité à l'éthanol. Deux aspects de Ia vulnérabilité ont été explorés: 1) la sensibilité aux effets produits par une administration d'éthanol: 2) la propension à consommer cette substance. Comparés aux témoins, les animaux adolescents stressés étaient moins sensibles aux effets d'une injection d'éthanol au niveau hormonal (activation de l'axe c0l1icotrope) et neurobiologique (activation des défenses anti¬oxydantes dans l'hippocampe). Une alcoolisation chronique avait un effet délétère sur la mémoire des rats témoins. mais de façon surprenante améliorait les performances mnésiques des stressés. Ces effets pourraient être sous-tendus par les modulations opposées des récepteurs mGlu observées dans l'hippocampe après l'alcoolisation. Chez des animaux mâles isolés (1 rat par cage), le stress prénatal n'altérait pas la préférence pour l'éthanol Cependant. un traitement chronique à l'éthanol augmentait spécifiquement chez les animaux stressés les quantités de [Delta]FosB (un facteur de transcription impliqué dans la vulnérabilité à la consommation de drogues) dans le noyau accumbens. Chez des femelles adolescentes, les conditions d'élevage (rats isolés ou par paires) modulaient différemment la consommation d'alcool des stressées et témoins. Ces données indiquent que le stress prénatal modifie durablement la vulnérabilité à l'éthanol chez le rat et soulignent l'importance de prendre en compte l'histoire de l'individu. même très précoce. pour appréhender la genèse des conduites addictives. / In rats, exposure to prenatal stress leads to a greater vulnerabiliy to several drugs of abuse (i.e. psychostimulants and opiates). The aim of the present work was to examine the impact of a prenatal stress (restraint stress of the pregnant dam) on ethanol vulnerability in adolescent and adult rats. Two distinct aspects of the vulnerability were evaluated : 1) the individual differences in the ethanol sensitivity: 2) the spontaneous consumption of ethanol Prenatally stressed rats were less sensitive than control rats to the effects of an ethanol injection during adolescence at the hormonal (HPA. axis activation) and neural (antioxidant defences in the hippocampus) levels. A chronic ethanol treatment induces memory impairments in control rats, whereas it has a beneficial effect on memory in rat subjected to a prenatal stress. These opposite effects could be mediated by the differential modulation of metabotropic glutamate receptors' levels in the hippocampus reported after the ethanol exposure. Prenatal stress has no impact on ethanol preference in isolated male rats. However. a chronic êlhanol treatment increased selectively the [Delta]FosB levels. a transcription factor involved in the vulnerability to drugs consumption, in the nucleus accumbens of prenatally stressed rats. Finally, we observed in female rats interplay between prenatal stress and rearing conditions on the ethanol consumption. Together, these data indicate that prenatal stress, in interaction with other experimental factors, can affect the ethanol sensitivity and consumption. They stress the importance to consider early life events in the study of the addictive behaviour genesis.

Dans cette thèse, nous cherchons à développer de nouvelles techniques pour écrire plus simplement des programmes formellement vérifiés. Nous procédons en étudiant l'utilisation de Coq en tant que langage de programmation dans différents environnements. Coq étant un langage purement fonctionnel, nous nous concentrons surtout sur la représentation et la spécification d'effets impurs, tel que les exceptions, les références mutables, les entrées-sorties et la concurrence.Nous travaillons premièrement sur deux projets préliminaires qui nous aident à comprendre les défis existants dans la programmation en Coq. Le premier projet, Cybele, est un plugin Coq pour écrire des preuves par réflexion efficaces avec effets. Nous compilons et nous exécutons les effets impurs en OCaml pour générer une prophétie, une forme de certificat, et interprétons les effets dans Coq en utilisant cette prophétie. Le second projet, le compilateur CoqOfOCaml, importe des programmes OCaml avec effets dans Coq en utilisant un système d'inférence d'effets.Puis nous décrivons différentes représentations génériques et composables d'effets impurs en Coq. Les calculs avec pause combinent les effets d'exceptions et de références mutables avec un mécanisme de pause. Ce mécanisme de pause permet de rendre explicite les étapes d'évaluation dans le but de représenter l'évaluation concurrente de deux termes. En implémentant le serveur web Pluto en Coq, nous réalisons que les entrées-sorties asynchrones sont l'effet le plus utile : cet effet est présent dans la plupart des programmes et ne peux être encodé de façon purement fonctionnelle. Nous concevons alors les "calculs asynchrones" comme moyen pour représenter et compiler des programmes avec événements en Coq.Finalement, nous étudions des techniques pour prouver des propriétés à propos de programmes avec effets. Nous commençons avec la vérification du système de blog ChickBlog écrit dans le langage des "calculs interactifs". Ce blog lance un fil d'exécution par client. Nous vérifions notre blog en utilisant une méthode de spécification par cas d'utilisation. Nous adaptons cette technique à la théorie des types en exprimant un cas d'utilisation comme un co-programme bien typé. Grâce à ce formalisme, nous pouvons présenter un cas d'utilisation comme un programme de test symbolique et le déboguer symboliquement, étape par étape, en utilisant le mode interactif de Coq. À notre connaissance, ceci représente la première telle adaptation de la spécification par cas d'utilisation en théorie des types. Nous pensons que la spécification formelle par cas d'utilisation est l'une des clés pour vérifier des programmes avec effets, sachant que la méthode des cas d'utilisation s'est avérée utile dans l'industrie pour exprimer des spécifications informelles. Nous étendons notre formalisme aux programmes concurrents et potentiellement non-terminants, avec le langage des "calculs concurrents". Nous concevons également un vérificateur de modèles pour vérifier l'absence d'interblocage dans un programme concurrent, en compilant la composition parallèle vers l'opérateur de choix non-déterministe. / In this thesis, we develop new techniques to conveniently write formally verified programs. To proceed, we study the use of Coq as a programming language in different settings. Coq being a purely functional language, we mainly focus on the representation and on the specification of impure effects, like exceptions, mutable references, inputs-outputs, and concurrency.First, we work on two preliminary projects helping us to understand the challenges of programming in Coq. The first project, Cybele, is a Coq plugin to write efficient proofs by reflection with effects. We compile and execute the impure effects in OCaml to generate a prophecy, a kind of certificate, and then interpret the effects in Coq using the prophecy. The second project, the compiler CoqOfOCaml, imports OCaml programs with effects into Coq, using an effect inference system.Next, we describe different generic and composable representations of impure effects in Coq. The breakable computations combine the standard exceptions and mutable references effects, with a pause mechanism to make explicit the evaluation steps in order to represent the concurrent evaluation of two terms. By implementing the Pluto web server in Coq, we realize that the most important effects to program are the asynchronous inputs-outputs. Indeed, these effects are ubiquitous and cannot be encoded in a purely functional manner. Thus, we design the asynchronous computations as a first way to represent and compile programs with events and handlers in Coq.Then, we study techniques to prove properties about programs with effects. We start with the verification of the blog system ChickBlog written in the language of the interactive computations. This blog runs one worker with synchronous inputs-outputs per client. We verify our blog using the method of specification by use cases. We adapt this technique to type theory by expressing a use case as a well-typed co-program over the program we verify. Thanks to this formalism, we can present a use case as a symbolic test program and symbolically debug it, step by step, using the interactive proof mode of Coq. To our knowledge, this is the first such adaptation of the use case specifications in type theory. We believe that the formal specification by use cases is one of the keys to verify effectful programs, as the method of use cases proved to be convenient to express (informal) specifications in the software industry. We extend our formalism to concurrent and potentially non-terminating programs with the language of concurrent computations. Apart from the use case method, we design a model-checker to verify the deadlock freedom of concurrent computations, by compiling the parallel composition to the non-deterministic choice operator using the language of blocking computations