He was a logic-major bachelor student of Peking University (2009~2013) and he was a Ph.D student of Princeton University (2013~2018). His research includes a series of program-logic-related topics: interactive theorem proving, Hoare logic for concurrent programs, program verification for randomized programs etc. In 2017, he unifies all different semantics of separation logics, some of which were thought to be incompatible with each other for a long time.