Qiyuan Xu
I am an Isabelle hacker and a PhD candidate at Nanyang Technological University, supervised by Conrad Watt. Aimming to diminish the gap between verification for functional correctness and broad industry applications, my research interest focuses on program logics, program verification, automated theorem proving, and neural theorem proving.
My current projects involve two directions:
Neural Theorem Proving for Real-world Proof Engineering
Isabelle infrastructures for machine learning:
- Isabelle REPL, a socket-based Isabelle REPL server for clusters.
- MiniLang, a minimal proof lanugage of Isabelle designed for LLM.
- MLML, a machine learning framework for NTP over Isabelle.
Sledgehammer wrapper / interfaces:
Associated papers:
- A Minimal Proof Language for Neural Theorem Proving over Isabelle/HOL. Qiyuan Xu, Renxi Wang, Haonan Li, David Sanan, Conrad Watt. online draft under review
An automated program verification platform over Isabelle
- Based on a first-order fictional separation logic
- Focusing on automation, equiped with our algebraic-based automation algorithms for generically reasoning about a wide amount of data structures.
- Certified programming that provides instant symbolic execution and a development environment intergrated within Isabelle/Isar.
- For sequential, terminating programs, but still capable for critical industrial applications like smart contracts.
- Github available
Associated papers:
- Generically Automating Separation Logic by Functors, Homomorphisms, and Modules. Qiyuan Xu, David Sanan, Zhe Hou, Xiaokun Luan, Conrad Watt, Yang Liu, POPL’25