Inner

Ones Inner Universe

I am (xiè) 宇()(héng), 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.)

I am also interested in the formalization of Lattice theory,
and its applications in formal concept analysis.

Contains

Connects

友人 / Friends

有的曾经相互鼓励过
有的正在相互鼓励中

友人 (按相识顺序)
Friends (Sorted by the day we know each other.)

Music

Music Diary / 何必惋惜永恒的阳光
  • 2019-08-16 你就要死了但我可以带你一起去那里

  • 2019-07-14 正在死去的美丽的会跳舞的天使和稻草人

  • 2019-07-12 切勿努力去忘记

  • 2019-03-06 今天本来不应该出门的

  • 2016-11-16 初犯
    • 荒城
      鲍鴻然
      稻粱亦盡人安在
      夜入秦川舊笛聲
      秋水不眠吞落月
      孤墳難入嘆荒城
    • 客夢
      鲍鴻然
      故雁回風驚客夢
      長川落日踏紛來
      秦中飛雪孤鴻寞
      嶺表玉階漫狂苔