Mecanización de semántica de lenguajes de programación: teoría, implementación y desarrollo.

El presente proyecto se enmarca en el área de métodos formales para computación; el objetivo de los métodos formales es asegurar, a través de herramientas lógicas y matemáticas, que sistemas computacionales satisfacen ciertas propiedades. El campo de semántica de lenguajes de programación trata justamente de construir modelos matemáticos que den cuenta de las diferentes características de cada lenguaje (estado mutable, mecanismos de paso de parámetros, órdenes de ejecución, etc.); permitiendo razonar de una manera abstracta, en vez de lidiar con las peculiaridades de implementaciones o las vaguezas de descripciones informales. Como las pruebas formales de corrección son demasiado intrincadas, es muy conveniente realizar estos desarrollos teóricos con la ayuda de asistentes de prueba. Este proceso de formalizar y corrobar aspectos semánticos a través de un asistente se denomina mecanización de semántica. Este proyecto – articulado en tres líneas: semántica de teoría de tipos, implementación de un lenguaje con tipos dependientes y semántica de lenguajes imperativos con alto orden - se propone realizar avances en el estudio semántico de lenguajes de programación, mecanizar dichos resultados, e implementar un lenguaje con tipos dependientes con la intención de que se convierta, en un mediano plazo, en un asistente de pruebas. En la línea de semántica de teoría de tipos los objetivos son: (a) extender el método de normalización por evaluación para construcciones no contempladas aun en la literatura, (b) probar la adecuación de la implementación en Haskell de dicho método de normalización, y (c) construir nuevos modelos categóricos de teoría de tipos. El objetivo de la segunda línea es el diseño e implementación de un lenguaje con tipos dependientes con la intención de que el mismo se convierta en un asistente de pruebas. Una novedad de esta implementación es que el algoritmo de chequeo de tipos es correcto y completo respecto al sistema formal, gracias a resultados ya obtenidos; además la implementación en Haskell del algoritmo de normalización (fundamental para el type-checking) también tendrá su prueba de corrección. El foco de la tercera línea está en el estudio de lenguajes de programación que combinan aspectos imperativos (estado mutable) con características de lenguajes funcionales (procedimientos y funciones). Por un lado se avanzará en la mecanización de pruebas de corrección de compiladores para lenguajes Algollike. El segundo aspecto de esta línea será la definición de semánticas operacional y denotacional del lenguaje de programación Lua y la posterior caracterización del mismo a partir de ellas. Para lograr dichos objetivos hemos dividido las tareas en actividades con metas graduales y que constituyen en sí mismas aportes al estado del arte de cada una de las líneas. La importancia académica de este proyecto radica en los avances teóricos que se propone en la línea de semántica de teoría de tipos, en las contribución para la construcción de pruebas mecanizadas de corrección de compiladores, en el aporte que constituye la definición de una semántica formal para el lenguaje Lua, y en el desarrollo de un lenguaje con tipos dependientes cuyos algoritmos más importantes están respaldados por pruebas de corrección. Además, a nivel local, este proyecto permitirá incorporar cuatro integrantes al grupo de “Semántica de la programación”.

Filososofía y Ciencia Computacional: Aspectos epistemológicos, ontológicos y metodológicos. Philosophy and Computing Sciencs: Epistemological, Ontological and Methodological Aspects.

Uno de los temas centrales del proyecto concierne la naturaleza de la ciencia de la computación. La reciente aparición de esta disciplina sumada a su origen híbrido como ciencia formal y disciplina tecnológica hace que su caracterización aún no esté completa y menos aún acordada entre los científicos del área. En el trabajo Three paradigms of Computer Science de A. Eden, se presentan tres posiciones admitidamente exageradas acerca de como entender tanto el objeto de estudio (ontología) como los métodos de trabajo (metodología) y la estructura de la teoría y las justificaciones del conocimiento informático (epistemología): La llamada racionalista, la cual se basa en la idea de que los programas son fórmulas lógicas y que la forma de trabajo es deductiva, la tecnocrática que presenta a la ciencia computacional como una disciplina ingenieril y la ahi llamada científica, la cual asimilaría a la computación a las ciencias empíricas. Algunos de los problemas de ciencia de la computación están relacionados con cuestiones de filosofía de la matemática, en particular la relación entre las entidades abstractas y el mundo. Sin embargo, el carácter prescriptivo de los axiomas y teoremas de las teorías de la programación puede permitir interpretaciones alternativas y cuestionaría fuertemente la posibilidad de pensar a la ciencia de la computación como una ciencia empírica, al menos en el sentido tradicional. Por otro lado, es posible que el tipo de análisis aplicado a las ciencias de la computación propuesto en este proyecto aporte nuevas ideas para pensar problemas de filosofía de la matemática. Un ejemplo de estos posibles aportes puede verse en el trabajo de Arkoudas Computers, Justi?cation, and Mathematical Knowledge el cual echa nueva luz al problema del significado de las demostraciones matemáticas.Los objetivos del proyecto son: Caracterizar el campo de las ciencias de la computación.Evaluar los fundamentos ontológicos, epistemológicos y metodológicos de la ciencia de la computación actual.Analizar las relaciones entre las diferentes perspectivas heurísticas y epistémicas y las practicas de la programación.

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.

Supervivencia y crecimiento de las exportaciones argentinas: un estudio a nivel regional

Este proyecto pretende aportar ideas para la elaboración de políticas de promoción de exportaciones a nivel nacional y regional. Uno de los argumentos más utilizados en la elaboración de tales políticas es que la apertura a nuevos mercados y la diversificación de los productos exportados (que se conoce en la literatura como margen extensivo) contribuye al logro de mayores tasas de crecimiento de las exportaciones. No obstante, numerosos trabajos demuestran que la capacidad de mantener las relaciones comerciales en el tiempo y poder intensificarlas también juegan un rol importante. Teniendo en cuenta los resultados alcanzados en numerosas investigaciones, se parte de la hipótesis de que las diferencias en las tasas de crecimiento de las exportaciones de las provincias argentinas pueden explicarse teniendo en cuenta el rol que han tenido los márgenes intensivo y extensivo. Los principales objetivos del trabajo son: a) estudiar el crecimiento de las exportaciones argentinas a nivel provincial, distinguiendo entre el surgimiento de nuevos productos y mercados (margen extensivo) y la supervivencia e incremento de las relaciones comerciales ya existentes (margen intensivo); b) demostrar que la supervivencia de las relaciones de exportación entre las provincias y los países de destino es una condición necesaria para una posterior intensificación de las mismas; c) determinar el rol de la duración de las relaciones comerciales en el crecimiento de las exportaciones; d) identificar la importancia de las políticas públicas en relación a las diferencias encontradas en las tasas de crecimiento de las exportaciones de las provincias. La metodología que se utilizará se basa en Besedes y Prusa (2007) y ampliada por Minondo y Requena (2010) quienes descomponen el crecimiento absoluto de las exportaciones entre dos años consecutivos en cuatro partes: supervivencia, profundización, fracaso y margen extensivo. El componente de supervivencia es la cantidad de relaciones de exportación que se mantiene entre dos períododos consecutivos; el de profundización proporciona el crecimiento absoluto promedio de las relaciones de exportación que han sobrevivido; el componente fracaso es el valor de las relaciones de exportación que no continúan. La combinación de estos tres primeros componentes proporciona el incremento en las exportaciones que resultan del cambio en el valor de las relaciones comerciales que permanecen activas entre dos períodos consecutivos y se conoce en la literatura como el margen intensivo. El margen extensivo es el valor de las nuevas relaciones de comercio que ocurren cada año. Luego se descompone el margen extensivo en volumen y valor y se expresan todos los componentes en tasas de crecimineto. Se llevará a cabo además un análisis contrafáctico con el propósito de responder a la siguiente pregunta: ¿Cuál hubiera sido la performance exportadora de una provincia si su comportamiento respondiera a las características de otra región elegida como referencia ?. Si se observaran cambios importantes en las tasas de crecimiento, se podría concluir que los valores de los componentes sustituidos sirven para explicar esas diferencias. Los resultados que se obtengan en este trabajo podrán compararse con los alcanzados en investigaciones sobre el tema para otros países y que han utilizado una metodología similar y con los realizados para Argentina utilizando información a nivel de las firmas. Desde el punto de vista de la política económica, los resultados y conclusiones podrán ser considerados especialmente como referencia en la elaboración de políticas económicas regionales.

El comercio justo, su impacto en la inclusión social y las exportaciones.

El comercio justo está poco difundido en Argentina. Tanto para los posibles exportadores como para los consumidores, uno que sea respetuoso del medio ambiente, de las condiciones dignas de los trabajadores y la inclusión social de la familia. La identificación del comercio justo actual, el reconocimiento de la producción que podría ser potencialmente certificada como de “Comercio Justo” colaborarían a acceder a este tipo de bienes a mercados internacionales con compradores de mayor poder adquisitivo. Con mayores datos sobre el comercio justo actual y el potencial, es posible instrumentar una política de promoción de este tipo de comercio y exportaciones. Y por lo tanto, la promoción del “Comercio Justo” en la región colaborará con la inclusión social el productor; y también la aparición de un consumidor más responsable. Una clave del sistema de Comercio Justo es la certificación, y no existen organismos oficiales que la realicen. Esto termina perdiendo veracidad ante el mercado consumidor. La investigación contará de cinco etapas principales: 1. Relevamiento del comercio exterior de Córdoba y detección de las exportaciones realizadas con etiquetado de Comercio Justo. Para este relevamiento se utilizarán las estadísticas de los organismos oficiales, así como información de Cámaras. 2. Se realizará una encuesta a empresas exportadoras sobre si conocen sobre la existencia de Comercio Justo, si analizaron su utilización o algún tipo de programa de Responsabilidad Social Empresaria, que tenga vinculación con el Medio Ambiente, las condiciones de los trabajadores, etc., de manera de realizar un diagnóstico del conocimiento y difusión del tema entre el mercado objetivo. 3. Análisis de la producción y exportaciones cordobesas que potencialmente podría n realizar exportaciones o ventas internas con etiquetado de comercio justo. Con el relevamiento de las exportaciones sumada al de la Matriz Productiva Provincial, se detectarán aquellos sectores en los cuales este tipo de comercio y/o certificación podrían favorecer el acceso a mercados, y una mayor implicancia social de la empresa en su entorno. 4. Identificación de los inconvenientes existentes que imposibilitan un mayor comercio de mercaderías con Comercio Justo. 5. Elaborar las pautas para un programa provincial de Comercio Justo que incentive estas exportaciones e incluya un proyecto de sistema de certificación de etiquetado.