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.

Desarrollo sustentable de geoestructuras compuestas por suelo loéssico compactado mejorado con agregado de materiales estabilizantes. Sustainable development of compacted loess soil geo-structures with addition of stabilizing materials.

Los suelos estabilizados mediante compactación, permiten obtener materiales con ventajas ténicas y economicas en diferentes tipos de obras de ingeniería. Ejemplos de su uso se tiene en bases viales de autopistas, rutas o calles urbanas, pistas de aterrizaje, barreras de contención para enterramientos sanitarios o lagunas de estabilización, apoyos de plateas para fundación de edificios, losas industriales, entre otras aplicaciones. Las fallas en este tipo de construcciones pueden resultar en catástrofes ambientales, sociales y elevadas pérdidas económicas, por lo que resulta de gran importancia optimizar el diseño e incrementar la seguridad de este tipo de construcciones. Las obras con estas características involucran grandes volúmenes y/o superficies que requieren controles sistemáticos durante su desarrollo, a los fines de garantizar el cumplimiento de las propiedades de los materiales establecidos en la etapa de diseño. De esta forma, es necesario contar con ensayos de campo sencillos, confiables y eficientes que permitan identificar propiedades físicas, mecánicas e hidráulicas. Las geoestructuras generadas mediante la compactación del suelo próximo al sector de construcción pueden funcionar adecuadamente, con reducidos costos de material y transporte. Su estabilización puede ejecutarse en forma natural, o con la incorporación de agregados minerales como bentonita, cal o cemento. Estas incorporaciones mejoran las propiedades hidráulicas y mecánicas del material, optimizando el comportamiento requerido para la obra. Para establecer la forma en la que estos minerales modifican el comportamiento del suelo local compactado deben realizarse investigaciones especiales con los materiales involucrados. En el ámbito internacional existen numerosas investigaciones sobre comportamiento de suelos compactados, no obstante, si bien aportan antecedentes para la planificación de estudios locales, sus resultados no pueden trasladarse de manera directa. Las características propias del suelo local constituye la principal variable debido a la diversidad en las propiedades geotécnicas de cada Región. Esta investigación, se focaliza en el empleo de suelos limosos de la formación loéssica de la zona central de Argentina. Los suelos de la llanura cordobesa poseen comportamientos particulares, los cuales son contemplados en los diseños presentados como resutado de las investigaciones internacionales. Esta particularidad se relaciona con su inestabilidad, lo que los clasifica como suelos colapsables. Los resultados obtenidos en este trabajo podrán ser extendidos a una gran superficie de la Provincia de Córdoba y a la Región Pampeana en general, a los fines de establecer recomendaciones de diseño y construcción para la confección de Pliegos de Especificaciones Técnicas de diferentes tipos de obras públicas y privadas. El estudio contempla la ejecución de un plan experimental a escala de laboratorio y campo. Los materiales corresponden a suelo limosos puros, y diferentes agregados tales como bentonita, cal y cemento. Se planifican ensayos para evaluar el desempeño del material, a partir de la confección de muestras preparadas con diferentes condiciones de compactación (energía, humedad y método), y en forma de mezcla con los distintos tipos de agregados. Se realizarán ensayos de permeabilidad en celdas de pared rígida y flexible, junto a ensayos mecánicos de compresión confinada, simple y triaxial. Para el trabajo experimental de campo se prevé la ejecución de terraplenes de prueba instrumentados con tensiómetros e infiltrómetros para evaluar el comportamiento hidraúlico en el tiempo, junto con ensayos de penetración y plato de carga para la caracterización mecánica. En forma conjunta se propone el desarrollo de modelos numéricos de caracterización hidromecánica. Stabilized soils by compaction, produce materials technical and economic advantages in different types of engineering works. For example, road bases in highways, roads or city streets, containment barriers for sanitary landfill or stabilization ponds, foundation support of building, industrial flat, and other applications. Failures can result in environmental catastrophes, social, and economic loss, so it is important to optimize the design and increase the safety of such buildings. These works involve large surfaces that require systematic tests during construction, so it is necessary to have simple field tests, reliable and efficient to identify physical, mechanical and hydraulic properties. The geo-structures generated by local soil compaction have reduced material and transportation costs. Stabilization can be naturally, or with the addition of mineral aggregates as bentonite, lime and cement. These additions improve the hydraulic and mechanical properties of the material. So, special investigations should be conducted with the materials involved. There are many international studies on compacted soils behavior but their results can not be transferred directly due to the particularities of regional soils. For this research silty soils of central Argentina are the main focus. The soils of Córdoba plains are instability, so are classified as collapsible soils. The results obtained in this work may be extended to a large area of the Province of Cordoba and the Pampas region in general, in order to establish design and construction recommendations. The study includes laboratory and field tests. The materials are pure silty soil, and different aggregates such as bentonite, lime and cement. Tests are planned to evaluate the performance. Laboratory includes rigid and flexible wall cells, confined, triaxial and simple compression tests. For field experimental instrumented embankments will be constructed. A numerical hydromechanical model will be developed.