Homotopy theory and applications

我的研究涉及拓扑学，代数，逻辑，计算，以及介于两者之间的各种主题。 拓扑学是研究表面和更高维度的形状，以及它们可以被拉伸，变形和映射到彼此的方式。我们研究这样的空间，探索他们与循环，球体和其他简单的几何形状。这通常会导致代数不变量，提供有关空间的定性和计算信息。拓扑学在许多其他领域也有应用，如代数、代数几何、物理学和计算机科学。有许多问题和技术，使在所有这些设置的意义，我的工作在拓扑学的主题是研究这些跨学科的问题。学科之间的这种相互作用已被证明是非常富有成效的，往往提供洞察力，导致解决开放的问题。我将继续处理这些问题，重点是涉及代数和几何的问题。 最近人们发现拓扑学和逻辑学之间有着密切的联系。类型论是数学的基础，自20世纪70年代以来，逻辑学家和计算机科学家一直在研究它，但在过去的十年中，人们发现它与拓扑学密切相关。我的部分工作涉及研究拓扑和逻辑之间的这种关系，并利用它在更基础的层面上理解这两个主题。在未来，我希望大多数数学都能得到形式化的验证，但即使在今天，形式化的验证也在工业中大量使用，例如在空中客车、英特尔、丰田和微软。 我还研究几何学的主题，这些主题概括了现有的研究光滑空间的方法，使我们能够研究在应用中自然出现的奇异空间和无限维空间。我工作的拓扑结构等空间，也研究切向量，这是重要的工具，几何应用。

My research involves topology, algebra, logic, computation, and various topics in between. Topology is the study of surfaces and higher-dimensional shapes, and the ways in which they can be stretched, deformed and mapped into each other. We study such spaces by probing them with loops, spheres and other simple geometric shapes. This generally results in algebraic invariants which provide qualitative and computational information about a space. Topology has applications in many other fields, such as algebra, algebraic geometry, physics and computer science. There are many questions and techniques that make sense in all of these settings, and the main theme of my work in topology is the study of such interdisciplinary problems. This interplay between disciplines has proven to be extremely fruitful, often providing insight that leads to solutions to open problems. I will continue to tackle such problems, with a focus on problems involving algebra and geometry. Recently it has been discovered that there is a close connection between topology and logic. Type theory is a foundation for mathematics that has been studied by logicians and computer scientists since the 1970s, but in the last decade it has been found to be intimately related to topology, in a deep and important way. Part of my work involves studying this relationship between topology and logic and using it to understand both subjects at a more fundamental level. In the future, I expect most mathematics to be formally verified, but even today formal verification is in heavy use in industry, e.g. at Airbus, Intel, Toyota and Microsoft. I also work on topics in geometry, which generalize existing methods of studying smooth spaces in a way that lets us study spaces with singularities and infinite-dimensional spaces that arise naturally in applications. I work on the topology of such spaces and also study tangent vectors, which are important tools for geometrical applications.