2026-05-05T19:56:57Zhttps://uvadoc.uva.es/oai/request

oai: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 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 info:eu-repo/semantics/masterThesis spa Departamento de Filosofía (Filosofía, Lógica y Filosofía de la Ciencia, Teoría e Historia de la Educación, Filosofía Moral, Estética y Teoría de las Artes) https://uvadoc.uva.es/handle/10324/72859 https://uvadoc.uva.es/bitstream/10324/72859/3/license.txt 289d98c1665ee0d20312360f0e8643c8 https://uvadoc.uva.es/bitstream/10324/72859/1/TFM_F_2024_030.pdf 3052f39fe2f69251174147b53a9374c8 Attribution-NonCommercial-NoDerivatives 4.0 Internacional