Sistemas supramoleculares autoensamblados con proyección a la Química Sustentable y sus aplicaciones en síntesis y reacciones de transferencia de electrones.

Este proyecto combina una serie de líneas de trabajo que, en esencia, estudian interacciones moleculares débiles y propiedades fisicoquímicas de diversos solutos en distintos medios. En todos los casos se procura comprender los factores que determinan la interacción de un soluto con su medio ya sea homogéneo o heterogéneo y aplicar estos conocimientos a diversos procesos, fundamentalmente en medios supramoleculares auto-organizados. Los medios supramoleculares que se estudian son: micelas inversas con agua u otros solventes polares sustitutos confinados en su corazón polar y vesículas. En este proyecto se desarrollan métodos que optimizan la detección de diferentes tipos de interacciones no-covalentes con distintas moléculas pruebas en los diferentes medios y, a partir de esto obtener aplicaciones diversas. Se trata de comprender los factores que determinan la solubilización, ubicación y/o reactividad de las moléculas pruebas en diferentes sitios del medio supramolecular y de esta manera obtener información acerca de las diferentes interacciones específicas en cada sitio del sistema supramolecular, lo cual es fundamental para el reconocimiento molecular ("inteligencia"). En definitiva estos estudios están orientados a: i) entender la adaptabilidad de nuevos sistemas supramoleculares para utilizar los resultados en el diseño de métodos de síntesis, electrosíntesis y catálisis dentro de los principios de la química sostenible o química verde y en la prevención a problemas de impacto ambiental tal como la remediación de aguas contaminadas por hidrocarburos y la degradación de pesticidas utilizando estrategias no convencionales; ii) la comprensión de fenómenos de transferencia de carga en sistemas auto-organizados y membranas biológicas; iii) el desarrollo de nuevos métodos de detección electroquímicos para compuestos de interés biológico, en medicina, alimentos y farmacología. También, dentro de los objetivos hay una componente muy fuerte de formación de recursos humanos como se aprecia en el número de becarios ya incorporados y a incorporar. La integración de estos conocimientos multidisciplinarios crea un ámbito sumamente beneficioso para la formación de doctorandos tan necesarios para el país ya que tendrán la oportunidad de participar en temas de investigación variados, relacionados con disciplinas diferentes, lo que sin duda será un valor añadido en su formación.

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”.