EVALUACIÓN DE LA CONSTANTE CINÉTICA k PARA EL EJERCICIO DE LA DBO EN EFLUENTES DE LA INDUSTRIA CHACINERA

La industria chacinera genera efluentes con alto contenido de materia orgánica, la cual puede evaluarse midiendo la demanda bioquímica de oxígeno (DBO). Conocer la velocidad a la cual es oxidada por vía biológica permite diseñar adecuadamente los sistemas de depuración, como así también evaluar el impacto que su vertido puede ocasionar sobre el ambiente. En el presente trabajo se determinó la constante de velocidad de reacción (k) y la demanda bioquímica de oxígeno última (L) para el efluente generado por un frigorífico faenador de porcinos y elaborador de chacinados, considerando que el ejercicio de la DBO es directamente proporcional a la concentración del sustrato (cinética de primer orden). Se evaluaron muestras del efluente recogidas en diferentes días de la semana, incubándolas durante diez días en condiciones estándar y se midió la DBO ejercida cada 24 horas. Con los valores encontrados se procedió a calcular los parámetros cinéticos k y L utilizando el método de los mínimos cuadrados. Se encontraron valores de k de 0,25 - 0,85 d-1 (rango 0,60 d-1) y L de 1578 – 3270 mg/l (rango 1692 mg/l). La DBO ejercida luego de 5 días de incubación (DBO5) osciló de 1328 – 2730 mg/l (rango 1402 mg/l). Los resultados de este estudio indican una importante variación en la carga contaminante del efluente medida en términos de DBO5, al igual que la velocidad de estabilización por vía biológica evaluada según los valores de k. Del mismo modo, la DBO5 expresa solo una fracción de la cantidad de oxígeno que se consumirá para la estabilización del residuo en un sistema de depuración o en el ambiente luego de su vertido. Estas situaciones influirán en la eficiencia de las plantas de depuración para este tipo de efluente a los efectos de lograr una adecuada depuración. Se considera conveniente conocer los parámetros cinéticos para optimizar el diseño de las instalaciones para el tratamiento del efluente generado por la industria chacinera y evaluar adecuadamente el impacto ambiental de este residuo.

Regulación del transporte de iones a través de membranas biológicas: El transporte activo Na/K y el contratransporte Na/Ca

El contra-transporte Na-Ca presente en células excitables es un sistema que, reversiblemente, puede introducir Ca de las células en intercambio por Na. La energía requerida para el transporte de Ca en contra de su gradiente electroquímico es provista por el gradiente de Na generado por la actividad de la Na+, K+- ATPasa. Por ello, aunque estos dos mecanismos funcionan independientemente uno del otro, están íntimamente ligados en la gestión integradora de la homeostasis iónica celular. (...) El presente plan consiste en dos subproyectos que estudiarán dos sistemas de transporte de cationes a través de la membrana celular estrechamente ligados entre sí. Estos son el contratransporte Na/Ca y el transporte activo Na/K que a su vez provee de energías (el gradiente de Na) para el funcionamiento del primero. Los estudios enfatizarán la regulación metabólica, su relevancia en la maduración y diferenciación celular y los intermediarios en los ciclos de reacción. (I) Subproyecto de Intercambio Na/Ca: Los objetivos que se persiguen son: (i) avanzar en la propiedades del sitio activador externo para cationes monovalentes (SAECM); (ii) analizar el ciclo de reacción en base a las propiedades del ciclo único tratando de establecer la cinética del sistema de unión de ligandos transportados (secuencial o ping pong); (iii) analizar el/los mecanismos asociados a la estimulación por MgATP. Si la fosforilación por ATP es requerida, identificar las reacciones y estructuras involucradas. Las preparaciones a utilizar incluyen células nerviosas en cultivo, vesículas de esas células y vesículas de cerebro total y de miocardio. (II) Transporte activo Na/K: el propósito es proveer información relevante al debate respecto del mecanismo por el cual K estimula la reacción de intercambio fosforil entre ATP y ADP y revierte la inhibición por Na exterior de la actividad Na-ATPasa, de la deforilación de E2P y del intercambio ATP-ADP. La preparación a utilizar será la Na+, K+- ATPasa purificada; la ubicación topográfica de sitios de interacción se efectuará utilizando la enzima incorporada en liposomas.

K-invariantes en el algebra universal de un grupo de Lie semisimple

Tarea (A):(...) Trataremos de extender a Sp(n,1) los resultados conseguidos sobre la imagen del homomorfismo de Lepowsky cuando G es SO(n,1) ó SU(n,1). (...) Tarea (B): (...) Para todo grupo de Lie de rango uno, con rango (G) = rango (K), los elementos del álgebra B son W-invariantes y que este resultado ya ha sido establecido para los grupos SO(2n,1) y SU(n,1); durante el período correspondiente a este subsidio esperamos extender este resultado a todo grupo de Lie de rango uno con rango (G) = rango (K). Tarea (C): Durante este período esperamos también avanzar en la determinación del dual unitario del grupo Spin (2n,C).

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.