Métodos para el análisis de programas probabilistas y no-deterministas utilizando probadores de teoremas. Methods for the analysis of probabilistic and nondeterministic programs using theorem provers.

La verificación y el análisis de programas con características probabilistas es una tarea necesaria del quehacer científico y tecnológico actual. El éxito y su posterior masificación de las implementaciones de protocolos de comunicación a nivel hardware y soluciones probabilistas a problemas distribuidos hacen más que interesante el uso de agentes estocásticos como elementos de programación. En muchos de estos casos el uso de agentes aleatorios produce soluciones mejores y más eficientes; en otros proveen soluciones donde es imposible encontrarlas por métodos tradicionales. Estos algoritmos se encuentran generalmente embebidos en múltiples mecanismos de hardware, por lo que un error en los mismos puede llegar a producir una multiplicación no deseada de sus efectos nocivos.Actualmente el mayor esfuerzo en el análisis de programas probabilísticos se lleva a cabo en el estudio y desarrollo de herramientas denominadas chequeadores de modelos probabilísticos. Las mismas, dado un modelo finito del sistema estocástico, obtienen de forma automática varias medidas de performance del mismo. Aunque esto puede ser bastante útil a la hora de verificar programas, para sistemas de uso general se hace necesario poder chequear especificaciones más completas que hacen a la corrección del algoritmo. Incluso sería interesante poder obtener automáticamente las propiedades del sistema, en forma de invariantes y contraejemplos.En este proyecto se pretende abordar el problema de análisis estático de programas probabilísticos mediante el uso de herramientas deductivas como probadores de teoremas y SMT solvers. Las mismas han mostrado su madurez y eficacia en atacar problemas de la programación tradicional. Con el fin de no perder automaticidad en los métodos, trabajaremos dentro del marco de "Interpretación Abstracta" el cual nos brinda un delineamiento para nuestro desarrollo teórico. Al mismo tiempo pondremos en práctica estos fundamentos mediante implementaciones concretas que utilicen aquellas herramientas.

Diseño y Desarrollo de Nuevas Entidades Químicas de Interés Farmacéutico. Design and Development of New Chemical Entities of Pharmaceutical Interest.

Este proyecto de investigación se basa fundamentalmente en diversas actividades concernientes a la investigación y desarrollo de nuevos fármacos. Estos estudios se llevan a cabo sobre nuevos derivados de las siguientes drogas líderes utilizadas en el tratamiento del SIDA: zidovudina (AZT), lamivudina (3TC), didanosina (ddI) y un tipo particular de Inhibidores No Nucleosídicos de la Transcriptasa Reversa (INNTR) conocidos como "diarilpirimidinas" (DAPYs). Se plantean para el presente proyecto los siguientes objetivos específicos:1. Diseño racional y síntesis de nuevos compuestos,2. Evaluación de actividades biológicas y citotoxicidad,3. Estudio de las propiedades fisicoquímicas de interés biológico y farmacéutico,4. Estudios farmacocinéticos y biofarmacéuticos.De esta manera, se ha considerado un estudio integrador, tendiente a conocer y entender el posible comportamiento en el organismo de nuevas entidades químicas de interés farmacéutico (NEQF). Así, nuestra hipótesis de trabajo se sustenta en que la variación de las propiedades fisicoquímicas y farmacocinéticas de las drogas actualmente en uso o en etapas de experimentación, podrá incidir favorablemente en la farmacoterapia del SIDA.Cabe destacar que la aplicación de diversos métodos computacionales, constituye una herramienta muy importante que se utilizada para cada uno de los objetivos planteados ya que brinda información complementaria y una ayuda invalorable para el diseño racional de drogas.Así, se diseñarán, prepararán y caracterizarán NEQF, estudiando en detalle sus propiedades moleculares. Se espera que la información generada represente una contribución para el desarrollo de nuevas opciones terapéuticas efectivas frente al agente causativo del SIDA, enfermedad para la cuál la opción de una terapia efectiva está lejos de ser la ideal.Como el proyecto se desarrolla dentro de un ámbito académico, las actividades previstas permitirán a los becarios y tesistas: 1) ampliar y profundizar los conocimientos teóricos relacionados con los temas de estudio; 2) desarrollar su capacidad creativa; 3) posibilitar el trabajo multidisciplinario. Es decir, se formarán recursos humanos altamente capacitados en el diseño y desarrollo de NEQF, finalizando las tesis doctorales en ejecución e incorporando nuevos jóvenes farmacéuticos.A partir de los resultados que se logren en el campo científico y académico, se espera contribuir a la promoción del conocimiento en el área del diseño y del desarrollo de Compuestos Farmacéuticos Activos. Es de nuestro especial interés que los resultados lleven a un posicionamiento del grupo en el área de la Química Medicinal, de la Bioorgánica y de la Biofarmacia.Con relación a la importancia del proyecto, cabe destacar que la Química Medicinal es una disciplina poco desarrollada en nuestro país, por lo tanto contribuirá no sólo a la generación de conocimiento en el área, sino también a la formación de recursos humanos. Cabe destacar la participación de jóvenes farmacéuticos que son los beneficiarios de dicho proceso de formación. Por otra parte, el desarrollo de NEQF conlleva en sí mismo un impacto social y económico importante, y redunda en beneficio de la salud de la población. Teniendo en cuenta la realidad actual, y considerando que la solución final para el tratamiento del SIDA aún no se ha alcanzado, optimizar la actividad/efectividad de fármacos conocidos y estudiar nuevas moléculas que actúen sobre diversas dianas biológicas constituye una esperanza para el tratamiento eficaz de esta enfermedad. Finalmente, teniendo en cuenta que la finalidad del proyecto es desarrollar nuevos agentes anti VIH con potencial aplicación clínica, es de esperar poder interaccionar con la industria farmacéutica y transferir los resultados a la misma.

Diseño de sistemas de comunicaciones de alta velocidad. Design of high-speed communication systems.

El crecimiento exponencial del tráfico de datos es uno de los mayores desafíos que enfrentan actualmente los sistemas de comunicaciones, debiendo los mismos ser capaces de soportar velocidades de procesamiento de datos cada vez mas altas. En particular, el consumo de potencia se ha transformado en uno de los parámetros de diseño más críticos, generando la necesidad de investigar el uso de nuevas arquitecturas y algoritmos para el procesamiento digital de la información. Por otro lado, el análisis y evaluación de nuevas técnicas de procesamiento presenta dificultades dadas las altas velocidades a las que deben operar, resultando frecuentemente ineficiente el uso de la simulación basada en software como método. En este contexto, el uso de electrónica programable ofrece una oportunidad a bajo costo donde no solo se evaluan nuevas técnicas de diseño de alta velocidad sino también se valida su implementación en desarrollos tecnológicos. El presente proyecto tiene como objetivo principal el estudio y desarrollo de nuevas arquitecturas y algoritmos en electrónica programable para el procesamiento de datos a alta velocidad. El método a utilizar será la programación en dispositivos FPGA (Field-Programmable Gate Array) que ofrecen una buena relación costo-beneficio y gran flexibilidad para integrarse con otros dispositivos de comunicaciones. Para la etapas de diseño, simulación y programación se utilizaran herramientas CAD (Computer-Aided Design) orientadas a sistemas electrónicos digitales. El proyecto beneficiara a estudiantes de grado y postgrado de carreras afines a la informática y las telecomunicaciones, contribuyendo al desarrollo de proyectos finales y tesis doctorales. Los resultados del proyecto serán publicados en conferencias y/o revistas nacionales e internacionales y divulgados a través de charlas de difusión y/o encuentros. El proyecto se enmarca dentro de un área de gran importancia para la Provincia de Córdoba, como lo es la informática y las telecomunicaciones, y promete generar conocimiento de gran valor agregado que pueda ser transferido a empresas tecnológicas de la Provincia de Córdoba a través de consultorias o desarrollos de productos.

Estrategias estadísticas y de aprendizaje automático en genómica y proteómica funcional.

El objetivo de este proyecto, enmarcado en el área de metodología de análisis en bioingeniería-biotecnología aplicadas al estudio del cáncer, es el análisis y caracterización a través de perfiles de expresión de proteínas y genes de las vías metabólicas asociadas a progresión tumoral. Dicho estudio se llevará a cabo mediante la utilización de tecnologías de alto rendimiento. Las mismas permiten evaluar miles de genes/proteínas en forma simultánea, generando así una gran cantidad de datos de expresión. Se hipotetiza que para un análisis e interpretación de la información subyacente, caracterizada por su abundancia y complejidad, podría realizarse mediante técnicas estadístico-computacionales eficientes en el contexto de modelos mixtos y técnicas de aprendizaje automático. Para que el análisis sea efectivo es necesario contemplar los efectos ocasionados por los diferentes factores experimentales ajenos al fenómeno biológico bajo estudio. Estos efectos pueden enmascarar la información subyacente y así perder informacion relevante en el contexto de progresión tumoral. La identificación de estos efectos permitirá obtener, eficientemente, los perfiles de expresión molecular que podrían permitir el desarrollo de métodos de diagnóstico basados en ellos. Con este trabajo se espera poner a disposición de investigadores de nuestro medio, herramientas y procedimientos de análisis que maximicen la eficiencia en el uso de los recursos asignados a la masiva captura de datos genómicos/proteómicos que permitan extraer información biológica relevante pertinente al análisis, clasificación o predicción de cáncer, el diseño de tratamientos y terapias específicos y el mejoramiento de los métodos de detección como así tambien aportar al entendimiento de la progresión tumoral mediante análisis computacional intensivo.

CREACIÓN DE RECURSOS INFORMÁTICOS PARA LAS LENGUAS MINORITARIAS MOCOVÍ Y QUECHUA

El contacto lingüístico entre diferentes comunidades en la Argentina produce una situación de diglosia que desplaza a las lenguas dominadas a favor de la dominante, en este caso, el castellano. Esta situación ha llevado a la extinción de muchas lenguas, y otras varias se encuentran en proceso de desaparición [http://www.ethnologue.com/show_country.asp?name=AR]. Con la muerte de estas lenguas no sólo se pierde un vasto bagaje cultural, sino que las comunidades indígenas se ven privadas de un elemento esencial para reafirmar su identidad y adaptarse a su medio socio-cultural. El objetivo último de este proyecto es contribuir a detener y, en lo posible, revertir estos procesos de extinción de las lenguas. Para ello, nos proponemos formalizar algunas lenguas indígenas de la Argentina para su tratamiento automático en aplicaciones computacionales que faciliten la producción lingüística, como por ejemplo la traducción automática de y hacia el castellano, ayudas a la redacción o facilitación translingüística. Este tipo de aplicaciones, además de contribuir a la preservación y multiplicación de usos de las lenguas aborígenes, facilitará que las comunidades se apropien de los procesos de inclusión digital, cuando éstos se implementen en su lengua materna. Por lo ambicioso de sus objetivos, este es un proyecto a largo plazo y con este subsidio que estamos solicitando abordaríamos el desarrollo de su fase inicial. Trabajaremos inicialmente con dos lenguas indígenas del territorio argentino que han sido bien descriptas a nivel lingüístico: el mocoví y el quechua, con la intención de extenderlo al mapundungun. A partir de las descripciones lingüísticas, propondremos una formalización computacional para cada una de estas lenguas, tratando de crear un núcleo común que facilite la adaptación de las aplicaciones computacionales a las diferentes lenguas. En una fase posterior del proyecto, la metodología y núcleo común consolidados para estas lenguas y dominios facilitarán el traslado de las aplicaciones a otras lenguas indígenas y a otros dominios semánticos. En esta fase inicial trabajaremos con aplicaciones de dominios semánticos restringidos, ya que se requiere mucho tiempo y esfuerzo para lograr un buen funcionamiento en aplicaciones de dominio general. Dos dominios en que consideramos sería beneficioso trabajar son la salud (concentrándonos por ejemplo en la información escrita sobre la prevención e higiene) y la agricultura (concentrándonos en información escrita relacionarse con el riego, la rotación de cultivos, etc). Sin embargo, planeamos hacer la elección final de dominios conjuntamente con organizaciones activas en la problemática abordada. Se trabajará a partir de datos recolectados por los propios investigadores implicados, así como datos producidos por otros proyectos, como por ejemplo los del DILA [http://www.caicyt.gov.ar/DILA], o los del proyecto Avenue [http://www.cs.cmu.edu/~avenue/].

“DESARROLLO DE GEOINDICADORES Y VALORACIÓN DE VULNERABILIDAD DE RECURSOS HÍDRICOS ASOCIADOS A LA EVALUACIÓN DEL IMPACTO PRODUCIDO POR CAMBIOS EN EL USO DEL SUELO”

La zona no saturada del suelo tiene una gran importancia en el ciclo del agua, así como en el transporte y las transformaciones de compuestos químicos. El estudio de esta zona es importante pues es el nexo entre el agua superficial y el agua subterránea. El incremento de las actividades agrícolas en la región central del país ha provocado un uso extendido de agroquímicos que contaminan las reservas hídricas subterráneas. La predicción y estimación del nivel de concentración, degradación, adsorción, retardo biológico, transporte y deposición de estos compuestos dependen de condiciones geológicas y propiedades físico-químicas del suelo. Es fundamental en este aspecto resolver con la información obtenida las ecuaciones de transporte de contaminantes para lo cual resulta de interés la mineralogía, tortuosidad, relación de vacíos y composición granulométrica del suelo. El transporte de contaminantes afecta la calidad del agua superficial (ríos, lagunas o esteros) y subterránea (napa freática y acuíferos) que constituyen fuentes de agua dulce. En este proyecto se realizan estudios que evalúan aspectos que afectan la calidad del agua superficial y subterránea debido a actividades antrópicas. En particular se analizan aspectos fenomenológicos de interés para el transporte de contaminantes en suelos para entender los mecanismos de contaminación de las aguas subterráneas. Estos estudios se realizarán en base a experimentos de laboratorio y simulaciones numéricas mediante modelos computacionales. Por otro lado, se tomarán dos casos o zonas de estudios, la primera abarca los recursos hídricos del norte de la Provincia de Córdoba, dentro de los cuales se destaca la laguna Mar Chiquita, y la segunda consiste en el estudio de la influencia del cambio del uso del suelo en la zona periurbana de la ciudad de Córdoba y el efecto que esto produce en la calidad del agua subterránea. En los estudios relacionados con la calidad y cantidad de agua que llega a la Laguna Mar Chiquita se realizarán estudios para la obtención de datos que permitan definir criterios de manejo y políticas de gestión de la cuenca intermedia, compatibles con requerimientos ambientales y sociales. Estos criterios y políticas serán una consecuencia de la interpretación del comportamiento fluvial y la respuesta del sistema hídrico ante los distintos pulsos de caudal, el cual será parcialmente aforado mediante campañas, y su interrelación con el uso del suelo en zonas que puedan afectar los afluentes de la laguna. Esto permitirá definir el caudal real que llega a la laguna y, de este modo, estimar el volumen ecológico de la misma. Al mismo tiempo, los afluentes en su trayecto reciben múltiples descargas de tipo doméstico, de origen industrial y de origen agropecuario (e.g. Río Suquía). Sin embargo, los estudios existentes sobre la calidad del agua y las actividades antrópicas son muy escasos, por lo cual resulta necesario realizar un seguimiento que permita conocer sus características y planificar su manejo. Por otro lado, se estudiará cómo el uso del suelo y fundamentalmente los cambios no controlados del mismo resultan vitales para poder preservar los recursos hídricos subterráneos. Este aspecto resulta de fundamental importancia en nuestra provincia en el caso del crecimiento acelerado que sufre la ciudad de Córdoba desde hace varias décadas por lo que éste caso se tomará como prioritario. Los resultados obtenidos permitirán generar información de gran valor para la toma de decisiones y obtener nuevos conocimientos relacionados con las características hidrodinámicas (superficial y subterránea) y del suelo en las zonas de estudio. Esto permitirá en un futuro definir o delimitar zonas de riesgo, realizar una adecuada planificación del uso del suelo en relación con las actividades agropecuarias y crecimiento de zonas urbanas y desarrollar programas para la preservación de recursos hídricos superficiales u subterráneos de la Provincia de Córdoba.

Optimización de Arquitecturas de Procesamiento Digital de Señales en Lógica Programable para Aplicaciones en Vuelos No Tripulados

En dispositivos electrónicos de última generación destinados a funciones de comunicación o control automático, los algoritmos de procesamiento digital de señales trasladados al hardware han ocupado un lugar fundamental. Es decir el estado de arte en el área de las comunicaciones y control puede resumirse en algoritmos basados en procesamiento digital de señales. Las implementaciones digitales de estos algoritmos han sido estudiadas en áreas de la informática desde hace tiempo. Sin embargo, aunque el incremento en la complejidad de los algoritmos modernos permite alcanzar desempeños atractivos en aplicaciones específicas, a su vez impone restricciones en la velocidad de operación que han motivado el diseño directamente en hardware de arquitecturas para alto rendimiento. En este contexto, los circuitos electrónicos basados en lógica programable, principalmente los basados en FPGA (Field-Programmable Gate Array), permiten obtener medidas de desempeño altamente confiables que proporcionan el acercamiento necesario hacia el diseño electrónico de circuitos para aplicaciones específicas “ASIC-VLSI” (Application Specific Integrated Circuit - Very Large Scale Integration). En este proyecto se analiza el diseño y la implementación de aquitecturas electrónicas para el procesamiento digital de señales, con el objeto de obtener medidas reales sobre el comportamiento del canal inalámbrico y su influencia sobre la estimación y el control de trayectoria en vehículos aéreos no tripulados (UAV, Unmanned Aerial Vehicle). Para esto se propone analizar un dispositivo híbrido basado en microcontroladores y circuitos FPGA y sobre este mismo dispositivo implementar mediante algoritmo un control de trayectoria que permita mantener un punto fijo en el centro del cuadro de una cámara de video a bordo de un UAV, que sea eficiente en términos de velocidad de operación, dimensiones y consumo de energía.

Dinámica y cinética de los procesos físicos y químicos del radical OH con compuestos orgánicos volátiles (COVs) de relevancia atmosférica. Dynamics and kinetics of the physical and chemical processes of OH radicals with atmospheric relevant volatile organic compounds (VOCs)

El objetivo del presente proyecto es estudiar los procesos físicos y químicos del radical OH con compuestos orgánicos volátiles (COVs), con los cuales sea factible la formación de agregados de van der Waals (vdW) responsables de la curvatura en los gráficos de Arrhenius, empleando técnicas modernas, complementarias entre si y novedosas en el país. El problema será abordado desde tres perspectivas complementarias: 1) estudios cinéticos, 2) estudios mecanísticos y de distribución de productos y 3) estudios de la dinámica de los procesos físicos y químicos. La finalidad es alcanzar una mejor comprensión de los mecanismos que intervienen en el comportamiento químico de especies presentes en la atmósfera y obtener datos cinéticos de alta calidad que puedan alimentar modelos computacionales capaces de describir la composición de la atmósfera, presente y futura. Los objetivos son estudiar: 1) mediante fotólisis láser pulsada con detección por fluorescencia inducida por láser (PLP-LIF), en reactores de flujo, la cinética de reacción del radical OH(v”=0) con COVs que presentan gráficos de Arrhenius curvos con energías de activación negativas, tales como alcoholes insaturados, alquenos halogenados, éteres halogenados, ésteres alifáticos; 2) en una cámara de simulación de condiciones atmosféricas de gran volumen (4500 L), la identidad y el rendimiento de productos de las reacciones mencionadas, a fines de evaluar su impacto atmosférico y dilucidar los mecanismos de reacción; 3) mediante haces moleculares y espectroscopía láser, la estructura y reactividad de complejos de vdW entre alcoholes insaturados o aromáticos (cresoles) y el radical OH, como modelo de los aductos propuestos como responsables de la desviación al comportamiento de Arrhenius de las reacciones mencionadas; 4) mediante PLP-LIF y expansiones supersónicas, las constantes específicas estado a estado (ksts) de relajación/reacción del radical OH(v”=1-4) vibracionalmente excitado con los COVs mencionados. Los resultados experimentales obtenidos serán contrastados con cálculos ab-initio de estructura electrónica, los cuales apoyarán las interpretaciones, permitirán proponer estructuras de estados de transición y aductos colisionales, como así también calcular las frecuencias de vibración de los complejos de vdW para su posterior asignación en los espectros LIF y REMPI. Asimismo, los mecanismos de reacción propuestos y los parámetros cinéticos medidos experimentalmente serán comparados con aquellos obtenidos por cálculos teóricos. The aim of this project is to study the physical and chemical processes of OH radicals with volatile organic compounds (VOCs) with which the formation of van der Waals (vdW) clusters, responsible for the observed curvature in the Arrhenius plots, might be feasible. The problem will be addressed as follow : 1) kinetic studies; 2) products distribution and mechanistic studies and 3) dynamical studies of the physical and chemical processes. The purpose is to obtain a better understanding of the mechanisms that govern the chemical behavior of species present in the atmosphere and to obtain high quality kinetic data to be used as input to computational models. We will study: 1) the reaction kinetics of OH (v”=0) radicals with VOCs such as unsaturated alcohols, halogenated alkenes, halogenated ethers, aliphatic esters, which show curved Arrhenius plots and negative activation energies, by PLP-LIF, in flow systems; 2) in a large volume (4500 L) atmospheric simulation chamber, reaction products yields in order to evaluate their atmospheric impact and reaction mechanisms; 3) using molecular beams and laser spectroscopy, the structure and reactivity of the vdW complexes formed between the unsaturated or aromatic alcohols and the OH radicals as a model of the adducts proposed as responsible for the non-Arrhenius behavior; 4) the specific state-to-state relaxation/reaction rate constants (ksts) of the vibrationally excited OH (v”=1-4) radical with the VOCs by PLP-LIF and supersonic expansions. Ab-initio calculations will be carried out to support the interpretation of the experimental results, to obtain the transition state and collisional adducts structures, as well as to calculate the vibrational frequencies of the vdW complexes to assign to the LIF and REMPI spectra. Also, the proposed reaction mechanisms and the experimentally measured kinetic parameters will be compared with those obtained from theoretical calculations.

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.

Integración de tecnologías de alto rendimiento, información clínica y funcional para el estudio funcional de cáncer de mama.

El objetivo general de este proyecto es contribuir al desarrollo de metodologías bioinformáticas que integren la información sobre niveles de expresión de genes obtenida mediante el uso de tecnologías de alto rendimiento en proteómica, microarreglos de ADN y/o secuenciamiento de nueva generación, junto con información clínica y funcional, a los efectos de mejorar la comprensión del fenómeno biológico bajo estudio. Como modelo de trabajo utilizaremos el cáncer de mama; sin embargo, las herramientas resultantes serán de aplicación más general. El proyecto consta de dos objetivos específicos: 1. Integrar información de expresión genómica, clínica y ontológica, para establecer si existen características funcionales que distinguen los diferentes tipos moleculares definidos para el cáncer de mama, y que puedan ser determinables utilizando las variables mencionadas. Los algoritmos de integración de los datos se desarrollarán en forma independiente de la plataforma tecnológica y población bajo estudio, utilizando información disponible en repositorios de libre acceso. 2. Aplicar la metodología de integración surgida del objetivo 1 para caracterizar los diferentes tipos de cáncer de mama de la población argentina, utilizando datos clínicos e información de diferentes tecnologías de alto rendimiento (proteómica, transcriptómica y genómica).

Sítios endocárdicos alternativos na estimulação cardíaca artificial

A estimulação ventricular direita convencional pode estar associada a efeitos deletérios sobre a função cardíaca. A necessidade de uma estimulação cardíaca artificial mais fisiológica é, indiscutivelmente, um dos pontos mais importantes na área da eletroterapia cardíaca. Os algoritmos de programação para a manutenção da condução atrioventricular própria, a estimulação de sítios endocárdicos alternativos e a terapia de ressincronização cardíaca são utilizados com o intuito de alcançar este objetivo. A estimulação do feixe de His e a estimulação septal têm sido estudadas como sítios endocárdicos alternativos para o posicionamento do eletrodo no ventrículo direito. A estimulação septal representa uma alternativa simples, prática e sem custos adicionais e com potenciais benefícios na redução dos efeitos deletérios da estimulação do ventrículo direito. Entretanto, esse sítio alternativo envolve um grupo heterogêneo de pacientes e apresenta resultados conflitantes quanto ao seu benefício clínico a longo prazo. Este artigo faz uma revisão das evidências científicas sobre os sítios alternativos de estimulação ventricular direita, com ênfase na segurança do procedimento, na medida dos parâmetros eletrofisiológicos, na avaliação da função ventricular esquerda e no acompanhamento clínico dos pacientes.

Adaptação e aplicabilidade de um algoritmo de diurético para pacientes com insuficiência cardíaca

FUNDAMENTO: Estados congestivos podem ser identificados e manejados através de algoritmos como o Diuretic Treatment Algorithm (DTA) para ajuste de diurético por telefone, com enfoque na avaliação clínica. Porém, o DTA está disponível somente em língua inglesa. OBJETIVO: Adaptar o DTA e testar sua aplicabilidade para uso no Brasil em pacientes ambulatoriais com IC. MÉTODOS: Seguiram-se as etapas de tradução, síntese, retrotradução, avaliação por comitê de especialistas e pré-teste (aplicabilidade clínica por meio de ensaio clínico randomizado). O DTA foi denominado, na versão para o Brasil, algoritmo de ajuste de diurético (AAD). Os pacientes foram randomizados para grupo intervenção (GI) - ajuste de diurético conforme o AAD - ou grupo controle (GC) - ajuste convencional. Foi avaliado o escore clínico de congestão (ECC) e o peso para ambos os grupos. RESULTADOS: Foram realizadas 12 modificações no DTA. Incluíram-se 34 pacientes. Para aqueles congestos, o aumento de diurético guiado pelo AAD resultou em maior resolução da congestão, com redução de dois pontos no ECC para 50% da amostra -2 (-3,5; -1,0), enquanto a mediana para o GC foi 0 (-1,25; -1,0), (p < 0,001). A mediana de variação de peso foi maior no GI -1,4 (-1,7; -0,5) quando comparado ao GC 0,1 (1,2; -0,6), p = 0,001. CONCLUSÕES: O ADD mostrou-se aplicável na prática clínica após adaptação e parece resultar em melhor controle da congestão em pacientes com IC. A efetividade clínica da ferramenta merece ser testada em amostra maior de pacientes visando sua validação para uso no Brasil (Universal Trial Number: U1111-1130-5749) (Arq Bras Cardiol. 2013; [online]. ahead print, PP.0-0).

Custo-Efetividade de Diferentes Estratégias Diagnósticas de Doença Coronária Estável em Portugal

Fundamento: O custo-efetividade é um fator de crescente importância na escolha de um exame ou terapêutica. Objetivo: Avaliar o custo-efetividade de vários métodos habitualmente empregados no diagnóstico de doença coronária estável em Portugal. Métodos: Foram avaliadas sete estratégias diagnósticas. O custo-efetividade de cada estratégia foi definido como o custo por cada diagnóstico correto (inclusão ou exclusão de doença arterial coronária obstrutiva) num doente sintomático. Os custos e a eficácia de cada método foram avaliados por meio de inferência bayesiana e análise de árvores de decisão, fazendo variar a probabilidade pré-teste entre 10 e 90%. Resultados: O custo-efetividade das várias estratégias diagnósticas é fortemente dependente da probabilidade pré-teste. Em doentes com probabilidade pré-teste ≤ 50%, os algoritmos diagnósticos, que incluem a angiotomografia computadorizada cardíaca são os mais custo-efetivos. Nesses doentes, dependendo da probabilidade pré-teste e da disponibilidade para pagar por diagnóstico correto adicional, a angiotomografia computadorizada pode ser usada como teste de primeira linha ou ser reservada a doentes com teste ergométrico positivo/inconclusivo ou escore de cálcio > 0. Em doentes com probabilidade pré-teste ≥ 60%, o envio direto para angiografia coronária invasiva parece ser a estratégia mais custo-efetiva. Conclusão: Os algoritmos diagnósticos, que incluem a angiotomografia computadorizada cardíaca, são os mais custo-efetivos em doentes sintomáticos com suspeita de doença arterial coronária estável e probabilidade pré-teste ≤ 50%. Em doentes de risco mais elevado (probabilidade pré-teste ≥ 60%), o envio direto para coronariografia invasiva parece ser a estratégia mais custo-efetiva. Em todas as probabilidades pré-teste, as estratégias baseadas em testes de isquemia parecem ser mais onerosas e menos eficazes que aquelas baseadas em testes anatômicos.

Simulación Monte Carlo de las dosis en tumores de pulmón en tratamientos de radioterapia estereotáxica extracraneal

Estudio elaborado a partir de una estancia en el Karolinska University Hospital, Suecia, entre marzo y junio del 2006. En la radioterapia estereotáxica extracraneal (SBRT) de tumores de pulmón existen principalmente dos problemas en el cálculo de la dosis con los sistemas de planificación disponibles: la precisión limitada de los algoritmos de cálculo en presencia de tejidos con densidades muy diferentes y los movimientos debidos a la respiración del paciente durante el tratamiento. El objetivo de este trabajo ha sido llevar a cabo la simulación con el código Monte Carlo PENELOPE de la distribución de dosis en tumores de pulmón en casos representativos de tratamientos con SBRT teniendo en cuenta los movimientos respiratorios y su comparación con los resultados de varios planificadores. Se han estudiado casos representativos de tratamientos de SBRT en el Karolinska University Hospital. Los haces de radiación se han simulado mediante el código PENELOPE y se han usado para la obtención de los resultados MC de perfiles de dosis. Los resultados obtenidos para el caso estático (sin movimiento respiratorio ) ponen de manifiesto que, en comparación con la MC, la dosis (Gy/MU) calculada por los planificadores en el tumor tiene una precisión del 2-3%. En la zona de interfase entre tumor y tejido pulmonar los planificadores basados en el algoritmo PB sobrestiman la dosis en un 10%, mientras que el algoritmo CC la subestima en un 3-4%. Los resultados de la simulación mediante MC de los movimientos respiratorios indican que los resultados de los planificadores son suficientemente precisos en el tumor, aunque en la interfase hay una mayor subestimación de la dosis en comparación con el caso estático. Estos resultados son compatibles con la experiencia clínica adquirida durante 15 años en el Karolinska University Hospital. Los resultados se han publicado en la revista Acta Oncologica.

Calibración TLR y LRM en MATLAB para medidas con guías de onda

En este proyecto, lo primero que hemos hecho ha sido desarrollar un algoritmo en Matlab que implementara el método de calibración TRL, el funcionamiento del cual hemos comprobado en primera instancia mediante simulaciones y, posteriormente, mediante un ejemplo real. Posteriormente, hemos desarrollado otro algoritmo en Matlab para implementar el método de calibración LRM. Este algoritmo sólo lo hemos podido comprobar a nivel de simulación. A continuación, mediante los dos algoritmos, hemos realizado una comparación entre ambos sistemas de calibración a través de simulaciones. Finalmente, analizando los resultados de varias simulaciones calibradas con nuestro programa del método TRL, hemos buscado cuáles pueden ser los motivos para la aparición de picos indeseados y hemos encontrado uno de ellos.