2026-04-27T21:31:54Zhttps://uvadoc.uva.es/oai/requestoai:uvadoc.uva.es:10324/728592024-12-19T20:03:11Zcom_10324_38col_10324_787
Teoría de tipos con funciones parciales
Castro Abal, Joaquín
Aranda Utrero, Víctor
Universidad de Valladolid. Facultad de Filosofía y Letras
En este trabajo se estudia la teoría de tipos con funciones parciales. Para llevar a cabo
este estudio, se completa un amplio recorrido. El trabajo parte del contexto en el que nace la teoría
de tipos y con qué propositos. Seguidamente se exponen los sistemas de teoría de tipos Q0, Alonzo,
PF y LUTINS, de los cuales los tres últimos incluyen funciones parciales. La presentación de los
fundamentos de cada sistema permite compararlos y analizar su adecuación para la formalización
de las matemáticas y la implementación en computación. Finalmente, se concluye que la teoría
de tipos, especialmente con funciones parciales, presenta múltiples ventajas en estos ámbitos. Por
este motivo, se presenta también una propuesta pedagógica para la incorporación de la teoría de
tipos en la educación general y en las carreras ligadas a las matemáticas aplicadas y computación.
In this project type theory with partial functions is studied. To carry out this
investigation, an extensive journey is completed. The work starts from the context in which
type theory was born and for what purposes. Next, the type theory systems Q0, Alonzo, PF
and LUTINS are presented, the last three including partial functions. The presentation of
the fundamentals of each system allows to compare them and analyze their suitability for the
formalization of mathematics and implementation in computing. Finally, it is concluded that
type theory, especially with partial functions, has multiple advantages in these areas. For this
reason, a pedagogical proposal is also presented for the incorporation of type theory to general
education and careers linked to applied mathematics and computing.
2024-12-19T08:18:51Z
2024-12-19T08:18:51Z
2024
info:eu-repo/semantics/masterThesis
https://uvadoc.uva.es/handle/10324/72859
spa
info:eu-repo/semantics/openAccess
http://creativecommons.org/licenses/by-nc-nd/4.0/
Attribution-NonCommercial-NoDerivatives 4.0 Internacional