Type theory language and space mappings

Authors

Presenter(s)

Joseph Kopp

Comments

9:00-10:15, Kennedy Union Ballroom

Files

Description

we explore the integration of constructive type theory within formal mathematical languages, focusing on its implementation in the Lean proof assistant. We delve into the Curry-Howard correspondence, which establishes a profound connection between logic and type theory, enabling propositions to be represented as types and proofs as programs. In particular, those concepts involving mappings between spaces, can be effectively modeled within this formal system.

Publication Date

4-23-2025

Project Designation

Capstone Project

Primary Advisor

Jun Li

Primary Advisor's Department

Mathematics

Keywords

Stander Symposium, College of Arts and Sciences

Institutional Learning Goals

Scholarship

Recommended Citation

"Type theory language and space mappings" (2025). Stander Symposium Projects. 4073.
https://ecommons.udayton.edu/stander_posters/4073