Department of Computer Science and Engineering
University of Minnesota
6-204 EE/CS Building, 200 Union Street SE
Minneapolis, MN 55455
I am a Ph.D. student at the University of Minnesota, Twin Cities. My
advisor is Gopalan
I am one of the developers of
the Abella theorem prover.
My research interests are broadly in the area of formal verification
of software systems. Within this context, I am interested in
developing specification and reasoning formalisms, in constructing
systems that implement these formalisms and in applying the formalisms
using the systems that implement them to verify software
In general, I enjoy doing research in the following fields:
programming languages, proof theory, type theory, automated and
interactive theorem proving, and program analysis.
Yuting Wang. A Higher-Order Abstract Syntax Approach to
Verified Compilation of Functional Programs. Ph.D. Thesis Proposal.
Yuting Wang, Gopalan Nadathur. A Higher-Order Abstract Syntax Approach
to Verified Transformations on Functional Programs.
The 25th European Symposium on Programming (ESOP), 2016.
Yuting Wang, Kaustuv Chaudhuri. A Proof-theoretic Characterization of
Independence in Type Theory. The 13th International
Conference on Typed Lambda Calculi and Applications (TLCA), 2015.
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, and Gopalan Nadathur.
Reasoning about Higher-Order Relational Specifications.
The 15th Symposium on Principles and Practice of Declarative Programming
David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller,
Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Abella: A System
for Reasoning about Relational Specifications. Journal of
Formalized Reasoning 7(2), 2014.
Yuting Wang and Gopalan Nadathur.
Towards Extracting Explicit Proofs from Totality Checking in Twelf.
The 8th ACM SIGPLAN International Workshop on Logical Frameworks