Sistemas de Tipos para Verificación de Programas Concurrentes. Type Systems for Concurrent Programs Verification.

La programación concurrente es una tarea difícil aún para los más experimentados programadores. Las investigaciones en concurrencia han dado como resultado una gran cantidad de mecanismos y herramientas para resolver problemas de condiciones de carrera de datos y deadlocks, problemas que surgen por el mal uso de los mecanismos de sincronización. La verificación de propiedades interesantes de programas concurrentes presenta dificultades extras a los programas secuenciales debido al no-determinismo de su ejecución, lo cual resulta en una explosión en el número de posibles estados de programa, haciendo casi imposible un tratamiento manual o aún con la ayuda de computadoras. Algunos enfoques se basan en la creación de lenguajes de programación con construcciones con un alto nivel de abstración para expresar concurrencia y sincronización. Otros enfoques tratan de desarrollar técnicas y métodos de razonamiento para demostrar propiedades, algunos usan demostradores de teoremas generales, model-checking o algortimos específicos sobre un determinado sistema de tipos. Los enfoques basados en análisis estático liviano utilizan técnicas como interpretación abstracta para detectar ciertos tipos de errores, de una manera conservativa. Estas técnicas generalmente escalan lo suficiente para aplicarse en grandes proyectos de software pero los tipos de errores que pueden detectar es limitada. Algunas propiedades interesantes están relacionadas a condiciones de carrera y deadlocks, mientras que otros están interesados en problemas relacionados con la seguridad de los sistemas, como confidencialidad e integridad de datos. Los principales objetivos de esta propuesta es identificar algunas propiedades de interés a verificar en sistemas concurrentes y desarrollar técnicas y herramientas para realizar la verificación en forma automática. Para lograr estos objetivos, se pondrá énfasis en el estudio y desarrollo de sistemas de tipos como tipos dependientes, sistema de tipos y efectos, y tipos de efectos sensibles al flujo de datos y control. Estos sistemas de tipos se aplicarán a algunos modelos de programación concurrente como por ejemplo, en Simple Concurrent Object-Oriented Programming (SCOOP) y Java. Además se abordarán propiedades de seguridad usando sistemas de tipos específicos. Concurrent programming has remained a dificult task even for very experienced programmers. Concurrency research has provided a rich set of tools and mechanisms for dealing with data races and deadlocks that arise of incorrect use of synchronization. Verification of most interesting properties of concurrent programs is a very dificult task due to intrinsic non-deterministic nature of concurrency, resulting in a state explosion which make it almost imposible to be manually treat and it is a serious challenge to do that even with help of computers. Some approaches attempts create programming languages with higher levels of abstraction for expressing concurrency and synchronization. Other approaches try to develop reasoning methods to prove properties, either using general theorem provers, model-checking or specific algorithms on some type systems. The light-weight static analysis approach apply techniques like abstract interpretation to find certain kind of bugs in a conservative way. This techniques scale well to be applied in large software projects but the kind of bugs they may find are limited. Some interesting properties are related to data races and deadlocks, while others are interested in some security problems like confidentiality and integrity of data. The main goals of this proposal is to identify some interesting properties to verify in concurrent systems and develop techniques and tools to do full automatic verification. The main approach will be the application of type systems, as dependent types, type and effect systems, and flow-efect types. Those type systems will be applied to some models for concurrent programming as Simple Concurrent Object-Oriented Programming (SCOOP) and Java. Other goals include the analysis of security properties also using specific type systems.

Mecanismos de Fotopercepción No-Visual y Control Circadiano en la Retina Interna de Vertebrados en Condiciones Fisiológicas y en un Modelo Animal de Ceguera. Mechanisms of Non-visual Perception and Circadian Control in the Vertebrate Inner Retina under Physiological Conditions and in Animal Model of Blindness.

La retina juega un rol esencial en el funcionamiento del sistema circadiano de los vertebrados al ser la encargada de sensar las condiciones de iluminación ambiental que ajustan el reloj interno con el fotoperíodo exterior a través de un circuito no-visual. Este circuito es independiente de la vía de formación de imágenes e involucra a las células ganglionares retinianas (CGRs) que proyectan a varias estructuras no-visuales del cerebro; esta vía es la encargada de regular el reflejo pupilar, la sincronización de los ritmos diarios de actividad, el sueño y la supresión de melatonina pineal. La retina contiene además un reloj autónomo que genera ritmos diarios autosostenidos en distintas funciones bioquímicas y fisiológicas, que le confiere la capacidad de predecir el tiempo y anticiparse en su fisiología a los cambios lumínicos a lo largo del ciclo día-noche. Este laboratorio ha demostrado por 1ra vez que las CGRs de pollo poseen osciladores endógenos que generan variaciones diarias en la biosíntesis de fosfolípidos (Guido et al, J Neurochem. 2001; Garbarino et al., J Neurosci Res. 2004a) y de la hormona melatonina con niveles máximos durante el día (Garbarino et al., J Biol Chem 2004b). Aún más, cultivos primarios de CGRs responden a la luz a través de una cascada bioquímica de fototransducción similar a la de invertebrados y que involucra la activación de la enzima fosfolipasa C (PLC) (Contin et al., FASEB J 2006). Estos cultivos fueron obtenidos a estadios embrionarios muy tempranos en dónde solo las CGRs son postmitóticas y mayoritariamente maduras. A estos estadios, los cultivos expresan marcadores de especificación de células ganglionares (pax6, brn3), la proteina Gq y los fotopigmentos melanopsina y criptocromos con gran homología con marcadores descriptos para fotorreceptores rabdoméricos de invertebrados (Contin et al, 2006). Recientemente comenzamos a investigar la percepción de luz en pollos GUCY1*, un modelo de ceguera, en animales que carecen de células fotorreceptoras-conos y bastones-funcionales. Resultados preliminares indicarían que la retina interna, y potencialmente las CGRs de estos animales conservarían la capacidad de responder a la luz regulando el reflejo pupilar y sincronizando los ritmos diarios de alimentación. La convergencia de osciladores y fotopigmentos en la población de CGRs podría contribuir al control temporal de la fisiología del organismo y regulación de funciones no-visuales. Son objetivos de este proyecto: a) Investigar el rol de las CGRs en el sistema circadiano estudiando: i- su habilidad para sintetizar melatonina y, su regulación por luz y dopamina; ii- su capacidad fotorreceptora intrínseca, investigando la presencia de fotopigmentos y componentes de la cascada de fototransducción fundamentalmente la vía de los fosfoinosítidos y la activación de PLC, mediante ensayos moleculares, bioquímicos y farmacológicos; b) Extender estos estudios a cultivos primarios de CGRs inmunopurificadas midiendo la respuesta a la luz sobre la síntesis de melatonina, y los niveles de los mensajeros 2rios Ca2+ y AMP cíclico, la inducción de genes tempranos y la regulación de la actividad NAT, enzima clave en la síntesis de melatonina; y c) Investigar la percepción de luz en pollos GUCY1*(ciegos), sobre distintas funciones no-visuales tales como el reflejo pupilar, la sincronización de los ritmos diarios de alimentación, la síntesis de melatonina y la expresión génica en animales expuestos a estimulación lumínica de distintas intensidades y longitudes de onda. Estos estudios permitirán construir el espectro de acción de la respuesta a la luz en los pollos ciegos a fin de identificar el/los fotopigmentos intervinientes en este fenómeno. Este proyecto profundizará el conocimiento sobre la capacidad fotorreceptora-no visual de la retina interna y particularmente de las CGRs, de la naturaleza de la cascada bioquímica que opera en las mismas y de los mecanismos de regeneración del cromóforo utilizado.