权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

Homotopy Type Theory

同伦型理论

基本信息

批准号：
2119809
负责人：
金额：
--
依托单位：
University of Cambridge
依托单位国家：
英国
项目类别：
Studentship
财政年份：
2018
资助国家：
英国
起止时间：
2018 至无数据
项目状态：
已结题

来源：
https://gtr.ukri.org/projects?ref=studentship-2119809
关键词：
Homotopy Type Theory

项目摘要

Type theory was originally developed by Russell as a foundation of mathematics which avoids paradoxes such as Russell's paradox. It was further developed by Church and Martin-Löf, amongst others. Unlike Set Theory, which must be used inside a logical framework such as Higher Order Logic, Martin-Löf's type theory (MLTT, or dependent type theory) internalises the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic, which corresponds to the computational model of Church's lambda calculus. One notable advantage of this intuitionistic interpretation is that every term in intensional MLTT can be reduced to a canonical form, and every function is computable, whereas in Set Theory it is possible to define incomputable functions. This makes it possible to develop theorem-proving systems where type checking is decidable.Quotient sets occur widely in mathematics. The current generation of dependently-typed theorem-proving systems do not make it very easy to produceproofs involving quotients. In informal mathematical practice one often describes constructions on quotient sets by saying what to do on a representative of an equality class, leaving the reader to check that it is well defined, that is, respects the equivalence relation. One aim of this research is to find easier ways to produce formal machine-checked proofs involving Quotient Inductive Types (QITs), ideally in a way that fits better with existing informal mathematical practice. It will build on the techniques researched in Steenkamp's Master's project on QITs. More generally it plans to investigate the use of Higher Inductive Types (HITs) in both theorem proving and functional programming. Two open problems in this field are finding a general schema for HITs, and giving a computational interpretation.Many researchers have identified the importance of this field, and the implications for mathematics and formal verification techniques should not beunderstated. One of the goals of the late Voevodsky and others is: "[T]hat, in a not too distant future, mathematicians will be able to verify the correctness of their own papers [...] in a proof assistant and that doing so will become natural even for pure mathematicians (in the same way that most mathematicians now typeset their own papers in TeX)." - Awodey, Pelayo, Warren (2013). The advantages are clear: Big or complex proofs can be tackled with much higher assurance, and anyone with a computer would have the capability of verifying a proof. This would allow fair assessment of research, not biased by name or status, perhaps leading to faster progress and a greater variety of ideas in mathematical research.Another major application of type theory research is in the development of type systems for programming languages, which guarantee certain kinds of error cannot occur. Experience has taught us that weakly typed languages result in bug-ridden, unmaintainable code. This is evidenced by the trend in industry away from weakly-typed languages and the recent development of languages with stronger type systems, such as Swift, Go, TypeScript, and C#. One notable example is Rust, in which the type system guarantees memory safety and thread safety. As the scale and complexity of computer programs continues to increase it is vital that research is carried out in type theory to ensure that future programs are robust, particularly in aerospace, medicine, security, and other high-assurance domains.Existing techniques such as unit tests cannot check for bugs such as "Will this program ever get stuck in an infinite loop?". Formal verification techniques can be used to prove that a program always terminates. Most formal verification techniques require translating the program into a model. This integration of program and proof will increase the adoption of verification tools, and the productivity of software developers using them.

类型论最初是由罗素作为数学的基础而发展起来的，它避免了像罗素悖论这样的悖论。它由Church和Martin-Löf等人进一步发展。与必须在高阶逻辑等逻辑框架内使用的集合论不同，马丁-洛夫的类型论（MLTT，或依赖类型论）内在化了直觉主义逻辑的布劳威尔-海廷-柯尔莫哥洛夫解释，这对应于丘奇的lambda演算的计算模型。这种直觉主义解释的一个显著优点是，内涵MLTT中的每一项都可以简化为标准形式，并且每个函数都是可计算的，而在集合论中，可以定义不可计算的函数。这使得开发类型检查是可判定的定理证明系统成为可能。商集在数学中广泛存在。当前一代的依赖型定理证明系统并不容易产生涉及到证明的证明。在非正式的数学实践中，人们经常通过说在一个等式类的代表上做什么来描述商集上的构造，让读者检查它是否定义良好，也就是说，尊重等价关系。本研究的一个目的是找到更简单的方法来产生正式的机器检查证明涉及商归纳类型（QIT），理想的方式，更适合现有的非正式的数学实践。它将建立在Steenkamp的QIT硕士项目中研究的技术基础上。更一般地说，它计划研究在定理证明和函数式编程中使用高级归纳类型（HIT）。在这一领域的两个开放性问题是找到一个通用的模式，并给出一个计算解释，许多研究人员已经认识到这一领域的重要性，数学和形式化验证技术的影响不应该被低估。已故的Voevodsky和其他人的目标之一是：“在不久的将来，数学家将能够验证自己论文的正确性。在一个证明助手，这样做将成为自然，甚至纯数学家（以同样的方式，大多数数学家现在打字自己的论文在TeX）。- Awodey，Pelayo，Warren（2013）.优点很明显：大型或复杂的证明可以更高的保证来处理，任何拥有计算机的人都有能力验证证明。这将允许对研究进行公平的评估，而不是以名称或地位为偏见，也许会导致数学研究的更快进展和更多样化的想法。类型论研究的另一个主要应用是开发编程语言的类型系统，这保证了某些类型的错误不会发生。经验告诉我们，弱类型的语言会导致bug缠身、不可维护的代码。这一点可以从工业界远离弱类型语言的趋势以及最近开发的具有更强类型系统的语言（如Swift，Go，TypeScript和C#）中得到证明。一个值得注意的例子是Rust，其中类型系统保证内存安全和线程安全。随着计算机程序的规模和复杂性不断增加，对类型理论的研究至关重要，以确保未来的程序是健壮的，特别是在航空航天，医学，安全和其他高保证领域。现有的技术，如单元测试，不能检查错误，如“这个程序会陷入无限循环吗？".形式验证技术可以用来证明程序总是终止的。大多数形式验证技术需要将程序转换为模型。这种程序和证明的集成将增加验证工具的采用，以及使用它们的软件开发人员的生产力。