Por favor, use este identificador para citar o enlazar este ítem:
https://hdl.handle.net/10495/27314| Título : | Simply typed lambda calculus with opposite types |
| Autor : | Pinilla Barrera, Alejandro |
| metadata.dc.contributor.advisor: | Agudelo Agudelo, Juan Carlos Sicard Ramírez, Andrés |
| metadata.dc.subject.*: | Lambda calculus Type theory Curry-Howard isomorphism Logic, symbolic and mathematical Lógica simbólica y matemática Tipos opuestos Normalización fuerte http://id.loc.gov/authorities/subjects/sh85074174 http://id.loc.gov/authorities/subjects/sh85139126 http://id.loc.gov/authorities/subjects/sh2001002954 http://id.loc.gov/authorities/subjects/sh85078115 |
| Fecha de publicación : | 2022 |
| Resumen : | ABSTRACT: In this article we present an extension of simply typed lambda calculus by introducing the idea of opposite types developed by Agudelo-Agudelo and Sicard-Ramírez (2021). The rules for these new types are based on the rules of a fragment of the logic system presented by the same authors. Two of the main properties of type systems are proven: The strong normalization theorem and the Curry-Howard correspondence. |
| Aparece en las colecciones: | Matemáticas |
Ficheros en este ítem:
| Fichero | Descripción | Tamaño | Formato | |
|---|---|---|---|---|
| PinillaAlejandro_2022_SimplyTypedLambda.pdf | Trabajo de grado de pregrado | 410.31 kB | Adobe PDF | Visualizar/Abrir |
Este ítem está sujeto a una licencia Creative Commons Licencia Creative Commons
