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.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | info:eu-repo/semantics/publishedVersion |
| Language: | spa |
| Published: |
2020
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/11086/15370 |
| _version_ | 1801214147683155968 |
|---|---|
| author | Tiraboschi, Ignacio |
| author2 | Ziliani, Beta |
| author_facet | Ziliani, Beta Tiraboschi, Ignacio |
| author_sort | Tiraboschi, Ignacio |
| collection | Repositorio Digital Universitario |
| 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. |
| format | info:eu-repo/semantics/publishedVersion |
| id | rdu-unc.15370 |
| institution | Universidad Nacional de Cordoba |
| language | spa |
| publishDate | 2020 |
| record_format | dspace |
| spelling | rdu-unc.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/ |
| 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 |
| title | 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_short | Generalización de meta-programas con tipado dependiente en Mtac2 |
| title_sort | generalizacion de meta programas con tipado dependiente en mtac2 |
| topic | Metaprogramación Asistentes de prueba Coq Mtac2 Theory of computation Logic Proof theory Type theory |
| url | http://hdl.handle.net/11086/15370 |
| work_keys_str_mv | AT tiraboschiignacio generalizaciondemetaprogramascontipadodependienteenmtac2 |