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 artifacts

• Ph.D. Thesis

  • Yuting Wang. A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs. [arXiv | Pdf (with fixes after submission)]

• Conference Papers

  • Yuting Wang, Pierre Wilke, Zhong Shao. An Abstract Stack Based Approach to Verified Compositional Compilation to Machine Code. The 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2019. [DOI |PDF |Slides |Website]

  • Gopalan Nadathur, Yuting Wang. Schematic Polymorphism in the Abella Proof Assistant. Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming (PPDP), 2018. [DOI | arXiv | Slides | Website]

  • Yuting Wang, Gopalan Nadathur. A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs. The 25th European Symposium on Programming (ESOP), 2016. [DOI | arXiv | Slides | Website]

  • 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. [DOI | Slides | Website]

  • 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 (PPDP), 2013. [arXiv | DOI]

• Journal Papers

  • 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. [DOI]

• Workshop Papers

  • Yuting Wang and Gopalan Nadathur. Towards Extracting Explicit Proofs from Totality Checking in Twelf. The 8th ACM SIGPLAN International Workshop on Logical Frameworks (LFMTP), 2013. [arXiv | DOI]