Generalización de meta-programas con tipado dependiente en Mtac2

Tesis (Lic. en Cs de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2020.

Detalles Bibliográficos
Autor principal: Tiraboschi, Ignacio
Otros Autores: Ziliani, Beta
Formato: publishedVersion bachelorThesis
Lenguaje:Español
Publicado: 2020
Materias:
Coq
Acceso en línea:http://hdl.handle.net/11086/15370
Aporte de:
id I10-R141-11086-15370
record_format dspace
spelling I10-R141-11086-153702023-12-13T18:19:00Z Generalización de meta-programas con tipado dependiente en Mtac2 Tiraboschi, Ignacio Ziliani, Beta Metaprogramación Asistentes de prueba Coq Mtac2 Theory of computation Logic Proof theory Type theory Tesis (Lic. en Cs de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2020. info:eu-repo/semantics/publishedVersion Fil: Tiraboschi, Ignacio. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. En este trabajo presentamos un nuevo meta-meta-programa lift que nos provee de una solución semiautomática para la generalización de terminos dependientes monádicos: dado cualquier metaprograma o operador (cómo bind) y una lista de dependencias (las del término que estamos bindeando), genera un nuevo operador que puede ser utilizando en un contexto donde las dependencias son esperadas. Es importante mencionar que utilizamos Mtac2 como su propio metalenguaje. In this work we present a new meta-meta-program lift that provides a semi-automatic solution to generalization of dependent monadic terms: given any meta-program or operator (like bind) and a list of dependencies (from the term we are binding), it generates a new operator that can be used in a context where such dependencies are expected. It is important to mention that we use Mtac2 as is as its own meta-language. info:eu-repo/semantics/publishedVersion Fil: Tiraboschi, Ignacio. Universidad Nacional de Córdoba. Facultad de Matemática, Astronomía, Física y Computación; Argentina. 2020-06-16T13:07:54Z 2020-06-16T13:07:54Z 2020-03 bachelorThesis http://hdl.handle.net/11086/15370 spa Atribución-CompartirIgual 4.0 Internacional http://creativecommons.org/licenses/by-sa/4.0/
institution Universidad Nacional de Córdoba
institution_str I-10
repository_str R-141
collection Repositorio Digital Universitario (UNC)
language Español
topic Metaprogramación
Asistentes de prueba
Coq
Mtac2
Theory of computation
Logic
Proof theory
Type theory
spellingShingle Metaprogramación
Asistentes de prueba
Coq
Mtac2
Theory of computation
Logic
Proof theory
Type theory
Tiraboschi, Ignacio
Generalización de meta-programas con tipado dependiente en Mtac2
topic_facet Metaprogramación
Asistentes de prueba
Coq
Mtac2
Theory of computation
Logic
Proof theory
Type theory
description Tesis (Lic. en Cs de la Computación)--Universidad Nacional de Córdoba, Facultad de Matemática, Astronomía, Física y Computación, 2020.
author2 Ziliani, Beta
author_facet Ziliani, Beta
Tiraboschi, Ignacio
format publishedVersion
bachelorThesis
author Tiraboschi, Ignacio
author_sort Tiraboschi, Ignacio
title Generalización de meta-programas con tipado dependiente en Mtac2
title_short Generalización de meta-programas con tipado dependiente en Mtac2
title_full Generalización de meta-programas con tipado dependiente en Mtac2
title_fullStr Generalización de meta-programas con tipado dependiente en Mtac2
title_full_unstemmed Generalización de meta-programas con tipado dependiente en Mtac2
title_sort generalización de meta-programas con tipado dependiente en mtac2
publishDate 2020
url http://hdl.handle.net/11086/15370
work_keys_str_mv AT tiraboschiignacio generalizaciondemetaprogramascontipadodependienteenmtac2
_version_ 1806949146249134080