Evaluación y Gestión de los riesgos relacionados con la inocuidad de los alimentos, asociados al rol del consumidor, en familias con niños en edad escolar primaria de la ciudad de Córdoba

El proyecto de investigación, desde un enfoque científico, multidisciplinario y regional, tiene por objetivo general identificar, evaluar y gestionar los riesgos asociados al rol de consumidor, que atentan contra la inocuidad de los alimentos en niños que cursan el nivel primario de escolaridad de la ciudad de Córdoba. La cadena agroalimentaria se extiende desde los productores primarios hasta los consumidores. La tarea de asegurar i) una disponibilidad suficiente, ii) la idoneidad nutricional y iii) la inocuidad de los alimentos suministrados es cada vez más compleja y requiere esfuerzos considerables. La ciencia y la tecnología han avanzado, para identificar, evaluar y gestionar los riesgos relacionados con los suministros de alimentos. Sin embargo, las enfermedades transmitidas por alimentos siguen siendo un motivo de grave preocupación para los consumidores. La distribución de los brotes según el origen en la Argentina para los casos relevados desde 1993 a 2002, indica que entre los comedores y la vivienda, se concentra el 95 % de los casos. (Sistema Regional de Vigilancia Epidemiológica de las ETA del Instituto Panamericano de Protección de Alimentos y Zoonosis) Todas las partes interesadas en la cadena agroalimentaria, comparten la responsabilidad de asegurar alimentos inocuos y nutritivos, desempeñando los consumidores una función decisiva, durante su preparación, almacenamiento y consumo. Como hipótesis del presente trabajo nos planteamos que la evaluación de los riesgos asociados al rol del consumidor en la ciudad de Córdoba, permitirá identificar la prevalencia y la incidencia de las prácticas que atentan contra la preservación de la inocuidad de un alimento y contribuirá en el desarrollo de actividades de gestión de riesgos acorde a las necesidades detectadas en la población de estudio. La realización de análisis del riesgo utilizando datos locales con el fin de abordar los riesgos de interés para la región, constituye una de las recomendaciones dadas por la FAO para América Latina. Abarca tres componentes importantes (evaluación del riesgo, gestión del riesgo y comunicación del riesgo), proporcionando un enfoque sistemático y disciplinado para la adopción de medidas apropiadas en materia de inocuidad de los alimentos. Proporciona la información y las pruebas que se necesitan para adoptar decisiones eficaces, contribuyendo a la obtención de mejores resultados en materia de inocuidad de los alimentos y a la mejora de la salud pública. (FAO 2008)

Estación Astronómica Polar J. L. Sersic

- El grupo IATE del Observatorio Astronómico Córdoba está desarrollando un proyecto observacional en el antártico, desde 1989, denominado ASTROLABEL. Las observaciones se realizan en Base Antártica Belgrano, a 78º S y 34º W, siendo el sitio más adecuado según la prospección hecha en las bases argentinas de actividad permanente. - Se pretende determinar cualitativamente la aptitud de la atmósfera polar para realizar observaciones astronómicas en el rango visible del espectro. Las especiales cirscunstancias de la región, como lo son su prolongado período de oscuridad invernal, la inexistencia de contaminación atmosférica y lumínica y los bajos niveles de humedad relativa, han despertado el interés de los investigadores. - Las tareas se desarrollan en convenio con el Instituto Antártico Argentino (IAA). Objetivos Se pretende determinar cualitativa y cuantitativamente las condiciones del cielo del lugar, para la ejecución de trabajos astronómicos de interés. (...) La disponibilidad de muchas horas de observación continuada hace posible el monitoreo de estrellas con una frecuencia de varias veces al día, lo que permitirá obtener su curva de luminosidad completa, sin interrumpir las observaciones por la salida del sol. Esta situación es la que permitirá la observación de Eta Carina, estrella que presenta bruscos y sorprendentes cambios en su luminosidad. Similar es el caso de las estrellas variables R Corona Borealis con cambios esporádicos, aunque de bajo valor en su brillo. Estas observaciones demandan de un monitoreo constante y con una frecuencia de al menos dos o tres veces diarias. Se pretende obtener una conclusión sobre la transparencia en el UV, cuando se produce la apertura de la depresión de ozono, para lo cual se obtendrá una correlación entre las mediciones de los índices de esa banda y las mediciones de ozono hechas en el lugar con medidores Brewer y EVA. También se tomarán datos con radiómetro de sol durante el verano.

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.

Verificación de Sistemas Basada en Teoría de Tipos

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.