Search

Cyclic adenosine monophosphate (cAMP) is a ubiquitous secondary messenger that plays a central role in endocrine tissue function, particularly in the synthesis of steroid hormones. The intracellular concentration of cAMP is regulated through its synthesis by cyclases and its degradation by cyclic nucleotide phosphodiesterases (PDEs). Although the expression and activity of PDEs impact the specificity and the amplitude of the cAMP response, it is becoming increasingly clear that the sub-cellular localization of PDE emphasizes the spatial regulation of the cell signalling processes that are essential for normal cellular function. We first examined the expression of PDE8A in porcine ovarian cells. PDE8A is expressed in granulosa cells, cumulus cells and oocytes. Second, we assessed the mitochondrial sub-cellular localization of PDE8A. Using western blotting with isolated mitochondrial fractions from granulosa cells and cumulus-oocyte complexes revealed immuno-reactive bands. PDE assay of isolated mitochondrial fractions from granulosa cells measured specific PDE8 cAMP-PDE activity as PF-04957325-sensitive. The immune-reactive PDE8A signal and MitoTracker labelling co-localized supporting mitochondrial sub-cellular localization of PDE8A, which was confirmed using immuno-electron microscopy. Finally, the effect of PDE8 on progesterone production was assessed during the in-vitro maturation of cumulus-oocyte complexes. Using PF-04957325, we observed a significant increase (P < 0.05) in progesterone secretion with follicle-stimulating hormone (FSH). Active mitochondria stained with MitoTracker orange CMTMRos were also increased by the specific PDE8 inhibitor supporting its functional regulation. In conclusion, we propose the occurrence of mitochondrial sub-cellular localization of PDE8A in porcine granulosa cells and cumulus cells. This suggests that there is potential for new strategies for ovarian stimulation and artificial reproductive technologies, as well as the possib

Cyclic adenosine monophosphate (cAMP) is a ubiquitous secondary messenger that plays a central role in endocrine tissue function, particularly in the synthesis of steroid hormones. The intracellular concentration of cAMP is regulated through its synthesis by cyclases and its degradation by cyclic nucleotide phosphodiesterases (PDEs). Although the expression and activity of PDEs impact the specifcity and the amplitude of the cAMP response, it is becoming increasingly clear that the subcellular localization of PDE emphasizes the spatial regulation of the cell signalling processes that are essential for normal cellular function. We frst examined the expression of PDE8A in porcine ovarian cells. PDE8A is expressed in granulosa cells, cumulus cells and oocytes. Second, we assessed the mitochondrial sub-cellular localization of PDE8A. Using western blotting with isolated mitochondrial fractions from granulosa cells and cumulus-oocyte complexes revealed immuno-reactive bands. PDE assay of isolated mitochondrial fractions from granulosa cells measured specifc PDE8 cAMP-PDE activity as PF-04957325-sensitive. The immune-reactive PDE8A signal and MitoTracker labelling colocalized supporting mitochondrial sub-cellular localization of PDE8A, which was confrmed using immuno-electron microscopy. Finally, the efect of PDE8 on progesterone production was assessed during the in-vitro maturation of cumulus-oocyte complexes. Using PF-04957325, we observed a signifcant increase (P<0.05) in progesterone secretion with follicle-stimulating hormone (FSH). Active mitochondria stained with MitoTracker orange CMTMRos were also increased by the specifc PDE8 inhibitor supporting its functional regulation. In conclusion, we propose the occurrence of mitochondrial sub-cellular localization of PDE8A in porcine granulosa cells and cumulus cells. This suggests that there is potential for new strategies for ovarian stimulation and artifcial reproductive technologies, as well as the possibility for us

103 p. , ill. , 30 cm, L’utilisation des programmes informatiques dans des applications critiques nécessite l’utilisation des méthodes formelles basées sur la rigueur mathématique pour établir leur correction conformément à leurs spécifications. La méthode formelle Why permet de générer, à partir d’un programme C spécifié avec Caduceus, un ensemble d’obligations de preuves qu’il faut prouver à l’aide d’un assistant de preuve pour établir la correction du programme. Le calcul matriciel est intensivement utilisé dans les programmes scientifiques Ceci a engendré le développement de plusieurs librairies dont BLAS (Basic Linear Algebra Subroutines), pour permettre une écriture rapide et efficace des programmes de calcul matriciel. Dans notre travail, nous avons utilisé la méthode Why pour prouver deux programmes issus des BLAS : le produit matriciel et la résolution des systèmes. Nous avons utilisé l’assistant de preuve coq pour décharger les obligations de preuves. Pour mener les preuves, nous avons proposé une nouvelle définition du type matrice qui peut être utilisé pour prouver d’autres programmes

103 p. , ill. , 30 cm, L’utilisation des programmes informatiques dans des applications critiques nécessite l’utilisation des méthodes formelles basées sur la rigueur mathématique pour établir leur correction conformément à leurs spécifications. La méthode formelle Why permet de générer, à partir d’un programme C spécifié avec Caduceus, un ensemble d’obligations de preuves qu’il faut prouver à l’aide d’un assistant de preuve pour établir la correction du programme. Le calcul matriciel est intensivement utilisé dans les programmes scientifiques Ceci a engendré le développement de plusieurs librairies dont BLAS (Basic Linear Algebra Subroutines), pour permettre une écriture rapide et efficace des programmes de calcul matriciel. Dans notre travail, nous avons utilisé la méthode Why pour prouver deux programmes issus des BLAS : le produit matriciel et la résolution des systèmes. Nous avons utilisé l’assistant de preuve coq pour décharger les obligations de preuves. Pour mener les preuves, nous avons proposé une nouvelle définition du type matrice qui peut être utilisé pour prouver d’autres programmes

Program transformation has gained a wide interest since it is used for several purposes: altering semantics of a program, adding features to a program or performing optimizations. In this paper we focus on program transformations at the bytecode level. Because these transformations may introduce errors, our goal is to provide a formal way to verify the update and establish its correctness. The formal framework presented includes a definition of a formal semantics of updates which is the base of a static verification and a scheme based on Hoare triples and weakest precondition calculus to reason about behavioral aspects in bytecode transformation, Comment: In Proceedings SCSS 2012, arXiv:1307.8029