Presenter(s)

    Joseph Kopp

    Comments

    9:00-10:15, Kennedy Union Ballroom

    Download

    Download Project (2.4 MB)

    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

    Type theory language and space mappings

    Share

    COinS