My interests in the intersection between interactive theorem-proving, formal and natural languages, and mechanised mathematics (mainly in probability theory and stochastic processes): 

• Interactive Theorem-Proving: The related tools are also called "proof assistants". I mainly use the Higher-Order Logic (HOL4) system and is an active contributor of it. I can also read some proofs written in HOL Light, Isabelle/HOL, Coq and Lean. 
• Mechanised Mathematics: Also called "Formal Mathematics", with the idea of representing mathematics definitions and theorems (with proofs) in ITP systems. I mainly work in the area of Probability Theory and Stochastic Processes.
• (Formal) Natural Language Processing: I'm one of the people who is trying to formalize/mechanise the Panini grammar of Sanskrit (ancient Indian language). I will use HOL4 in this work.

I received my PhD (Assumption-Based Runtime Verification of Finite- and Infinite-State Systems) in 2022 from the University of Trento (Italy) and my MSc (A Formalization of Unique Solutions of Equations in Process Algebra) in 2017 from the University of Bologna (Italy), and was an undergraduate at Zhejiang University (China) from 2001 to 2005.