Homotopy Type Theory

类型理论最初是由罗素发展起来的，作为避免罗素悖论等悖论的数学基础。它是由丘奇和马丁-L等人进一步开发的。与集合论不同，集合论必须在高阶逻辑等逻辑框架内使用，马丁-L的类型理论(MLTT，或从属类型理论)内化了直觉主义逻辑的布劳沃-海廷-科尔莫戈洛夫解释，这与丘奇的Lambda演算的计算模型相对应。这种直观解释的一个显著优点是，内涵MLTT中的每一项都可以归结为规范形式，并且每个函数都是可计算的，而在集合论中可以定义不可计算的函数。这使得开发定理证明系统成为可能，其中类型检查是可确定的。商集在数学中广泛存在。当前一代依赖类型的定理证明系统不能很容易地产生涉及商的证明。在非正式的数学实践中，人们经常通过说明如何处理等式类的代表来描述商集上的结构，让读者检查它是否定义良好，即尊重等价关系。这项研究的目的之一是找到更容易的方法来产生涉及商归纳类型(QIT)的正式机器检查证明，理想的方式是以一种更适合现有非正式数学实践的方式。它将建立在Steenkamp硕士关于QIT的项目中研究的技术之上。更广泛地说，它计划研究更高归纳类型(HITS)在定理证明和函数式编程中的使用。该领域的两个悬而未决的问题是寻找HITS的通用模式和给出计算解释。许多研究人员已经认识到该领域的重要性，其对数学和形式验证技术的影响不容小觑。已故的沃沃茨基和其他人的目标之一是：“在不太遥远的将来，数学家将能够在证明助手中验证他们自己论文的正确性[……]，即使对于纯粹的数学家来说，这样做也是很自然的(就像大多数数学家现在用TeX排版自己的论文一样)。”-Awodey，Pelayo，Warren(2013)。其优势是显而易见的：大型或复杂的证明可以更有把握地处理，任何拥有计算机的人都有能力验证证明。这将允许对研究进行公平的评估，而不是以名字或地位为偏见，也许会导致数学研究更快的进展和更多的想法。类型理论研究的另一个主要应用是开发编程语言的类型系统，这保证了某些类型的错误不会发生。经验告诉我们，弱类型的语言会导致错误丛生、不可维护的代码。业界逐渐远离弱类型语言的趋势，以及最近开发的具有更强类型系统的语言，如SWIFT、GO、TypeScrip和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.