Xiaohong Chen

Welcome. I'm the CTO of Pi Squared Inc.

I built mathematical foundations for programming languages through logic and formal verification during my PhD.

At Pi Squared, applying this to web3 revealed that performance is what unlocks adoption. My work now spans consensus protocols and distributed systems — alongside technical strategy and partnerships.

Bio

2024–presentCTOPi Squared Inc.
2023–2024Research EngineerRuntime Verification Inc.
2016–2023PhDUniversity of Illinois Urbana-Champaign
2015–2016Research AssistantSingapore University of Technology and Design
2014–2015Assistant LecturerBirmingham City University
2010–2014BScPeking University

Selected Publications

Matching μ-logic.
Xiaohong Chen.
PhD Thesis, University of Illinois Urbana-Champaign, 2023.
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier.
Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu.
OOPSLA 2023. [DOI]
Towards a Trustworthy Semantics-Based Language Framework via Proof Generation.
Xiaohong Chen, Zhengyao Lin, Minh-Thai Trinh, Grigore Rosu.
CAV 2021. [DOI]
A General Approach to Define Binders Using Matching Logic.
Xiaohong Chen, Grigore Rosu.
ICFP 2020. [DOI]
Towards a Unified Proof Framework for Automated Fixpoint Reasoning Using Matching Logic.
Xiaohong Chen, Minh-Thai Trinh, Nishant Rodrigues, Lucas Peña, Grigore Rosu.
OOPSLA 2020. [DOI]
Matching μ-Logic.
Xiaohong Chen, Grigore Rosu.
LICS 2019. [DOI]

View all publications →