Motilidad Orientada de Células Neurales: La comunicación celular a distancia. Oriented neural cell motility: Cell comunication at a distance.

La motilidad celular orientada (o mecanismo quimiotáctico de orientación), es una respuesta celular a señales moleculares de su micro-ambiente necesaria para modular la distribución celular en sitios específicos y con elevada precisión. Nuestra hipótesis establece que la migración orientada de células neurales es regulada por gradientes de concentración de moléculas solubles liberadas por sus regiones "blanco". Este proyecto es continuación del estudio de la quimiotaxis de células de cresta neural (CCN) y de neuronas ventriculares (NV) inducida respectivamente por factores difusibles de la región del futuro ganglio ciliar y del bulbo olfatorio.En el sistema de CCN, hemos caracterizado como moléculas quimiotácticas a la quimioquina Stromal Cell-Derived Factor-1, y los factores tróficos Stem Cell Factor y Neurotrophic Factor-3, habiendo determinado la expresión de sus respectivos receptores CXCR4, TrkC y p75 en la población de CCN mesencefálicas de ambrión de pollo. Actualmente, estamos desarrollando experimentos con el Ciliary Neurotrophic Factor y factores de la familia Bone Morphogenetic Proteins. Además de la estrategia experimental in vitro, hemos determinado en el embrión entero la expresión de las moléculas quimioatractantes mediante hibridación in situ del ARNm y la presencia de las respectivas proteínas mediante inmunocitoquímica. En el sistema de NV, estamos analizando la motilidad celular en relación con moléculas liberadas por el bulbo olfatorio. En los dos sistemas biológicos, estamos analizando elementos de la transducción de señales y cambios en el citoesqueleto, en ambos casos asociados con la respuesta temprana en la orientación quimiotáctica de la célula. Asimismo, en ambos sistemas biológicos, evaluamos los efectos del etanol sobre la migración y distribución celular, en condiciones equivalentes a las que inducen el Sindrome Fetal Alcohólico en mamíferos.En base a resultados ya obtenidos en experimentos in vitro, en la presente etapa intentaremos su caracterización in vivo mediante el bloqueo funcional de las moléculas quimiotácticas (y/o sus receptores) sobre embriones enteros, mediante silenciamiento con ARNsi (o morfolinos específicos) mediante electroporación, y posterior determinación de la distribución celular mediante marcadores específicos anti-CCN (o lipofílicos de tipo DiI).Los resultados permitirán mejorar el conocimiento del mecanismo de la migración celular orientada y aportar al diseño de recursos diagnósticos, terapéuticos o de control de anomalías embrionarias o patologías tumorales por mala distribución celular como las Neurocristopatías, o inducidas por tóxicos exógenos como el Sindrome Fetal Alcohólico.

Análisis comparativo entre actividades de aprendizaje diseñadas con Estudio de Casos y Aprendizaje Basado en Problemas, y actividades de tipo tradicional, como dispositivos didácticos en Educación a Distancia. Comparative analysis of learning activities designed with Problem Based Learning and Case Study approaches, and activities designed with traditional methods, in Distance Education.

Identificación y caracterización del problema: El problema que guía este proyecto, pretende dar respuesta a interrogantes tales como: ¿De qué modo el tipo de actividades que se diseñan, se constituyen en dispositivos posibilitadores de la comprensión de los temas propios de cada asignatura, por parte de los alumnos? A partir de esta pregunta, surge la siguiente: Al momento de resolver las actividades, ¿qué estrategias cognitivas ponen en juego los estudiantes? y ¿cuáles de ellas favorecen procesos de construcción del conocimiento? Hipótesis: - Las asignaturas cuyas actividades están elaboradas bajo la metodología de Aprendizaje Basado en Problemas y Estudio de Casos, propician aprendizajes significativos por parte de los estudiantes. - Las actividades elaboradas bajo la metodología del Aprendizaje Basado en Problemas y el Estudio de Casos requieren de procesos cognitivos más complejos que los que se implementan en las de tipo tradicional. Objetivo: - Identificar el impacto que tienen las actividades de aprendizaje de tipo tradicional y las elaboradas bajo la metodología de Aprendizaje Basado en Problemas y Estudio de Casos, en el aprendizaje de los alumnos. Materiales y Métodos: a) Análisis de las actividades de aprendizaje del primero y segundo año de la carrera de Abogacía, bajo lamodalidad a Distancia. b) Entrevistas tanto a docentes contenidistas como así también a los tutores. c) Encuestas y entrevistas a los alumnos. Resultados esperados: Se pretende confirmar que las actividades de aprendizaje, diseñadas bajo la metodología del Aprendizaje Basado en Problemas y el Estudio de Casos, promueven aprendizajes significativos en los alumnos. Importancia del proyecto y pertinencia: La relevancia del presente proyecto se podría identificar a través de dos grandes variables vinculadas entre sí: la relacionada con el dispositivo didáctico (estrategias implementadas por los alumnos) y la referida a lo institucional (carácter innovador de la propuesta de enseñanza y posibilidad de extenderla a otras cátedras). El presente proyecto pretende implementar mejoras en el diseño de las actividades de aprendizaje, a fin de promover en los alumnos la generación de ideas y soluciones responsables y el desarrollo de su capacidad analítica y reflexiva.

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.