Towards extracting explicit proofs from totality checking in twelf. - Yuting Wang 001; Gopalan Nadathur (LFMTP, 2013)

Reasoning about higher-order relational specifications. - Yuting Wang 001; Kaustuv Chaudhuri; Andrew Gacek; Gopalan Nadathur (PPDP, 2013)

Abella: A System for Reasoning about Relational Specifications. - David Baelde; Kaustuv Chaudhuri; Andrew Gacek; Dale Miller 001; Gopalan Nadathur; Alwen Tiu; Yuting Wang 001 (J. Formaliz. Reason., 2014)

A Proof-theoretic Characterization of Independence in Type Theory. - Yuting Wang 001; Kaustuv Chaudhuri (TLCA, 2015)

Verified Transformations on Functional Programs Using the Higher-Order Abstract Syntax Approach. - Yuting Wang 001; Gopalan Nadathur (CoRR, 2015)

A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs. - Yuting Wang 001; Gopalan Nadathur (ESOP, 2016)

A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs. - Yuting Wang 001 (CoRR, 2017)

Schematic Polymorphism in the Abella Proof Assistant. - Gopalan Nadathur; Yuting Wang 001 (PPDP, 2018)

An abstract stack based approach to verified compositional compilation to machine code. - Yuting Wang 001; Pierre Wilke; Zhong Shao 001 (Proc. ACM Program. Lang., 2019)

CompCertELF: verified separate compilation of C programs into ELF object files. - Yuting Wang 001; Xiangzhe Xu; Pierre Wilke; Zhong Shao 001 (Proc. ACM Program. Lang., 2020)

Automatic Generation and Validation of Instruction Encoders and Decoders. - Xiangzhe Xu; Jinhua Wu; Yuting Wang 001; Zhenguo Yin; Pengfei Li (CAV (2), 2021)

Verified Compilation of C Programs with a Nominal Memory Model (Artifact). - Yuting Wang 001; Ling Zhang; Zhong Shao 001; Jérémie Koenig (Zenodo, 2021)

Verified Compilation of C Programs with a Nominal Memory Model (Artifact). - Yuting Wang 001; Ling Zhang; Zhong Shao 001; Jérémie Koenig (Zenodo, 2021)

Verified compilation of C programs with a nominal memory model. - Yuting Wang 001; Ling Zhang; Zhong Shao 001; Jérémie Koenig (Proc. ACM Program. Lang., 2022)

Towards a Framework for Developing Verified Assemblers for the ELF Format. - Jinhua Wu; Yuting Wang 001; Meng Sun; Xiangzhe Xu; Yichen Song (APLAS, 2023)

Verified Transformation of Continuation-Passing Style into Static Single Assignment Form. - Siyu Liu; Yuting Wang 001 (TASE, 2023)

A Bottom-Up Approach to a Unified Semantic Interface for Verified Compositional Compilation. - Ling Zhang; Yuting Wang 001; Jérémie Koenig; Zhong Shao 001 (CoRR, 2023)

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. - Ling Zhang; Yuting Wang 001; Jinhua Wu; Jérémie Koenig; Zhong Shao 001 (Zenodo, 2023)

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. - Ling Zhang; Yuting Wang 001; Jinhua Wu; Jérémie Koenig; Zhong Shao 001 (Zenodo, 2023)

Generic Reasoning of the Locally Nameless Representation. - Yicheng Ni; Yuting Wang 001 (APLAS, 2024)

Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. - Ling Zhang; Yuting Wang 001; Jinhua Wu; Jérémie Koenig; Zhong Shao 001 (Proc. ACM Program. Lang., 2024)

Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). - Yu Zhang 086; Jérémie Koenig; Yuting Wang 001; Zhong Shao 001 (Zenodo, 2024)

Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). - Yu Zhang 086; Jérémie Koenig; Yuting Wang 001; Zhong Shao 001 (Zenodo, 2024)

Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). - Yu Zhang 086; Jérémie Koenig; Yuting Wang 001; Zhong Shao 001 (Zenodo, 2024)

Unifying compositional verification and certified compilation with a three-dimensional refinement algebra (artifact). - Yu Zhang 086; Jérémie Koenig; Yuting Wang 001; Zhong Shao 001 (Zenodo, 2024)

Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra. - Yu Zhang 086; Jérémie Koenig; Zhong Shao 001; Yuting Wang 001 (Proc. ACM Program. Lang., 2025)

CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks. - Ling Zhang; Yuting Wang 001; Yalun Liang; Zhong Shao 001 (Proc. ACM Program. Lang., 2025)

CompCertOC: Verified Compositional Compilation of Multi-Threaded Programs with Shared Stacks. - Ling Zhang; Yuting Wang 001; Yalun Liang; Zhong Shao 001 (Zenodo, 2025)