Homotopy Type Theory

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

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.