Resumen de Teoría de Tipos Dependientes: Una primera aproximación

Fernando Chu Rivera

• español

  Presentamos la Teoría de Tipos Dependientes, que uniformiza los conceptos de proposiciones y de conjuntos en uno solo más general, el de “tipos”. Desarrollamos las nociones principales de esta teoría, y observamos que esta puede funcionar como un fundamento para estudiar las matemáticas, reemplazando la teoría de conjuntos. Ejemplificamos esto estudiando el caso de los números naturales, y explicamos cómo el uso de los asistentes de prueba nos permite tener una base más sólida para los resultados matemáticos.

• English

  We present Dependent Type Theory, which combines the concepts of propositions and sets in a more general one, that of “types”. We develop the main notions of this theory, and observe that it can serve as a foundation of mathematics, replacing set theory. We exemplify this studying the natural numbers, and explain how the use of proof assistants gives us a more rigorous foundation for mathematical results.