Investigating Inductive Types within Dependent Type Theory
Investigating Inductive Types within Dependent Type Theory
研究依赖类型理论中的归纳类型
批准号：
2594512
负责人：
金额：
$0.0万
依托单位：
依托单位国家：
英国
项目类别：
Studentship
财政年份：
2021
资助国家：
英国
项目状态：
未结题
起止时间：
2021 至 --
中文摘要
翻译
马丁-洛夫的依赖类型理论是在建构主义数学原理基础上发展起来的一种形式语言。归纳类型在这一理论中起着核心作用。我的研究旨在探索它们的形式化，以及不同类别的归纳类型之间的比较。这在泛型编程、软件验证和证明助手中都有应用。
英文摘要
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.
期刊论文(0)
专著(0)
科研奖励(0)
会议论文
海外基金
