El proyecto se plantea dentro del marco de la teoría y meta-teoría de los lenguajes de programacion. Especificamente proponemos el desarrollo de lógicas de orden superior y de otros formalismos lógicos, llamados sistemas tipados de reescritura de términos, que capturen y que garanticen el funcionamiento correcto de algunos métodos avanzados de programacion y de definición de tipos de datos para el paradigma funcional. En dicho paradigma de programación un programa no es más que una serie de definiciones de función que, en ausencia de efectos laterales como los causados por el enunciado de asignación, resultan ser funciones en el sentido_x000D_ matemático. En particular nos interesa estudiar algunos aspectos de los tipos de datos anidados o no-regulares, los cuales son familias de tipos de datos indizados sobre todos los tipos y donde distintos miembros de la familia se relacionan mediante distintos constructores, en el sentido de que existe al menos un constructor de tipos que relaciona a dos miembros de la familia con índices diferentes, por ejemplo List A y List AxA. El término “anidado” se debe a que la recursion se anida en un cambio de parámetro. Estas familias de tipos se han estudiado ampliamente en el caso inductivo [AM03,AMU05,BM98,BP99a,BP99b,JG09] y resultan útiles para definir estructuras puramente funcionales que requieran de ciertos invariantes, los cuales se garantizan mediante la definicion misma del tipo y no externamente como en el caso de la programación imperativa u orientada a objetos, por ejemplo los árboles roji-negros, las listas de acceso aleatorio o los árboles binarios perfectamente balanceados [Ok98]. A este respecto deseamos ampliar formalismos existentes desarrollados previamente por miembros del proyecto [AMU05,Ma10, Mi09] de manera que se verifiquen ciertas propiedades universales conocidas (leyes de operadores de plegado), asi como incluir también_x000D_ tipos de datos coinductivos anidados, los cuales sirven para representar estructuras de datos perezosas (potencialmente infinitas). Nuestra principal herramienta será el llamado enfoque categorico de la programacion [Ha87,Ha87b,MFP91], el cual utiliza diversos conceptos de la teoria de las categorias para formalizar metodologias de programacion. Las investigaciones propuestas en este protocolo cuentan con la participación de al menos dos académicos que, reuniendo sus conocimientos, estarán en posibilidad de abordar los problemas con mayor facilidad. Cabe mencionar que si bien el responsable del proyecto y el investigador extranjero involucrado no tienen aun publicaciones en comun, ambos han trabajado muy cercanamente durante los estudios doctorales del responsable llevados a cabo en la universidad de Munich en el periodo septiembre 2000 a diciembre 2004. En particular la publicacion [Mi09] del responsable se basa ampliamente y extiende diversos resultados de la_x000D_ tesis doctoral del investigador extranjero [Ma99]._x000D_ _x000D_ _x000D_ _x000D_ _x000D_ _x000D_ _x000D_ _x000D_ _x000D_ _x000D_ _x000D_ _x000D_

1) Poner a disposición de los científicos de la computación, en especial a aquellos interesados en la teoría de los lenguajes de programación, lógicas y sistemas de tipos polimórficos de orden superior que capturen leyes ecuacionales y propiedades universales de los operadores de plegado. Esto se logrará mediante los fundamentos de la programacion funcional que proporciona la teoria de las categorias. En particular se desea extender el trabajo de [Ma10] de manera que se puedan verificar nuevas leyes como las presentadas en [MGB04,Hi00]. _x000D_ _x000D_ 2) Implementar los sistemas obtenidos, en la medida de lo posible, mediante el asistente de prueba Coq [Co09]. Tal implementación traerá consigo una verificacion de los esquemas de programacion generados por los operadors de plegado así como la certificacion de su funcionamiento correcto. Esto es una contribución importante a la meta-teoría de los lenguajes de programacion funcional._x000D_ _x000D_ _x000D_ 3) Adicionalmente se planea contribuir a la teoría y meta-teoría de los lenguajes de programación con mecanismo de evaluación perezosa. Esto se hará mediante el estudio de familias de tipos de datos coinductivos anidados, proporcionando casos de estudio que muestren la utilidad de los formalismos obtenidos. Por ejemplo mediante el estudio de estructuras cíclicas, es decir, estructuras finitas o potencialmente infinitas con apuntadores hacia atras (back-pointers) [GHU06]._x000D_ _x000D_ _x000D_ _x000D_