课题基金 / 基金详情

Investigating Inductive Types within Dependent Type Theory

研究依赖类型理论中的归纳类型

批准号：

2594512

负责人：

金额：

$0.0万

依托单位：

University of Nottingham

依托单位国家：

英国

项目类别：

Studentship

财政年份：

2021

资助国家：

英国

项目状态：

未结题

起止时间：

2021 至 --

来源：

https://gtr.ukri.org/projects?ref=studentship-2594512

关键词：

Investigating Inductive Types within Dependent

项目摘要

项目成果

相似基金

相关文献

中文摘要

翻译

点击翻译按钮获取中文摘要

英文摘要

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)

会议论文