dor_id: 1500781

506.#.#.a: Público

650.#.4.x: Físico Matemáticas y Ciencias de la Tierra

336.#.#.b: other

336.#.#.3: Registro de colección de proyectos

336.#.#.a: Registro de colección universitaria

351.#.#.b: Proyectos Universitarios PAPIIT (PAPIIT)

351.#.#.a: Colecciones Universitarias Digitales

harvesting_group: ColeccionesUniversitarias

270.1.#.p: Dirección General de Repositorios Universitarios. contacto@dgru.unam.mx

590.#.#.c: Otro

270.#.#.d: MX

270.1.#.d: México

590.#.#.b: Concentrador

883.#.#.u: https://datosabiertos.unam.mx/

883.#.#.a: Portal de Datos Abiertos UNAM, Colecciones Universitarias

590.#.#.a: Administración central

883.#.#.1: http://www.ccud.unam.mx/

883.#.#.q: Dirección General de Repositorios Universitarios

850.#.#.a: Universidad Nacional Autónoma de México

856.4.0.u: http://datosabiertos.unam.mx/DGAPA:PAPIIT:IN117711

100.1.#.a: Favio Ezequiel Miranda Perea

524.#.#.a: Dirección de Desarrollo Académico, Dirección General de Asuntos del Personal Académico (DGAPA). "Formalismos lógico categóricos para la programación funcional", Proyectos Universitarios PAPIIT (PAPIIT). En "Portal de datos abiertos UNAM" (en línea), México, Universidad Nacional Autónoma de México.

720.#.#.a: Favio Ezequiel Miranda Perea

245.1.0.a: Formalismos lógico categóricos para la programación funcional

502.#.#.c: Universidad Nacional Autónoma de México

561.1.#.a: Facultad de Ciencias, UNAM

264.#.0.c: 2011

264.#.1.c: 2011

307.#.#.a: 2019-05-23 18:40:21.491

653.#.#.a: Teoría y meta-teoría de lenguajes de programación; Ciencias de la computación

506.1.#.a: La titularidad de los derechos patrimoniales de este recurso digital pertenece a la Universidad Nacional Autónoma de México. Su uso se rige por una licencia Creative Commons BY 4.0 Internacional, https://creativecommons.org/licenses/by/4.0/legalcode.es, fecha de asignación de la licencia 2011, para un uso diferente consultar al responsable jurídico del repositorio por medio de contacto@dgru.unam.mx

041.#.7.h: spa

500.#.#.a: 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_

046.#.#.j: 2019-11-14 12:26:40.706

264.#.1.b: Dirección General de Asuntos del Personal Académico

handle: 53ccbfbe16594db8

harvesting_date: 2019-11-14 12:26:40.706

856.#.0.q: text/html

last_modified: 2019-11-22 00:00:00

license_url: https://creativecommons.org/licenses/by/4.0/legalcode.es

license_type: by

No entro en nada

No entro en nada 2