Investigating Inductive Types within Dependent Type Theory
Lead Research Organisation:
University of Nottingham
Department Name: School of Computer Science
Abstract
Martin-Lof's dependent type theory is a formal language developed on the principles of constructive mathematics. Inductive types play a central role within this theory. My research aims to explore their formalisations and how different classes of inductive types compare to each other. This has applications in generic programming, software verification, and proof assistants.
Organisations
People |
ORCID iD |
| Thorsten Altenkirch (Primary Supervisor) | |
| Stefania Damato (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/R513283/1 | 01/10/2018 | 30/09/2023 | |||
| 2594512 | Studentship | EP/R513283/1 | 01/10/2021 | 31/03/2025 | Stefania Damato |
| EP/T517902/1 | 01/10/2020 | 30/09/2025 | |||
| 2594512 | Studentship | EP/T517902/1 | 01/10/2021 | 31/03/2025 | Stefania Damato |