I am 谢 宇恒, an independent Chinese researcher in Foundations of Mathematics.
The area of my inquiry is beautifully formulated by Vladimir Voevodsky as the following,
A formal deduction system together with a correspondence
between its components and objects and actions in the world of mathematical thoughts
which can be used to formalize all subject areas of mathematics
is called a foundational system for mathematics or "Foundations of Mathematics".
I design programming languages
and use them as formal deduction systems
to formalize areas of mathematics which I am interested in.
I am specially interested in the formalization of Algebraic topology,
(I am trying to find an algebraic definition of infinity groupoids
that would satisfy the Grothendieck correspondence.)
and its applications in Geometric modeling.
I am also specially interested in the formalization of Category theory,
and its applications in the design of programming language's type systems.
(Which relates back to my language designs.)
This kind of applications are called Categorical semantics or Categorical logic.
(It is called "Categorical logic" because type systems are equivalent to logic deduction systems.)