Yuting Wang

22 papers A 1B 2C 2Misc 1Journal 13Unranked 3
YearRankTypeTitle / Venue / Authors
2025 J jnl
CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared Stacks.
Proc. ACM Program. Lang.
Ling Zhang, Yuting Wang, Yalun Liang, Zhong Shao
2025 J jnl
Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra.
Proc. ACM Program. Lang.
Yu Zhang, Jérémie Koenig, Zhong Shao, Yuting Wang
2024 J jnl
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules.
Proc. ACM Program. Lang.
Ling Zhang, Yuting Wang, Jinhua Wu, Jérémie Koenig, Zhong Shao
2024 B conf
Generic Reasoning of the Locally Nameless Representation.
APLAS
Yicheng Ni, Yuting Wang
2023 J jnl
A Bottom-Up Approach to a Unified Semantic Interface for Verified Compositional Compilation.
CoRR
Ling Zhang, Yuting Wang, Jérémie Koenig, Zhong Shao
2023 B conf
Towards a Framework for Developing Verified Assemblers for the ELF Format.
APLAS
Jinhua Wu, Yuting Wang, Meng Sun, Xiangzhe Xu, Yichen Song
2023 Misc conf
Verified Transformation of Continuation-Passing Style into Static Single Assignment Form.
TASE
Siyu Liu, Yuting Wang
2022 J jnl
Verified compilation of C programs with a nominal memory model.
Proc. ACM Program. Lang.
Yuting Wang, Ling Zhang, Zhong Shao, Jérémie Koenig
2021 — conf
Automatic Generation and Validation of Instruction Encoders and Decoders.
CAV (2)
Xiangzhe Xu, Jinhua Wu, Yuting Wang, Zhenguo Yin, Pengfei Li
2020 J jnl
CompCertELF: verified separate compilation of C programs into ELF object files.
Proc. ACM Program. Lang.
Yuting Wang, Xiangzhe Xu, Pierre Wilke, Zhong Shao
2019 J jnl
An abstract stack based approach to verified compositional compilation to machine code.
Proc. ACM Program. Lang.
Yuting Wang, Pierre Wilke, Zhong Shao
2018 C conf
Schematic Polymorphism in the Abella Proof Assistant.
PPDP
Gopalan Nadathur, Yuting Wang
2018 J jnl
Schematic Polymorphism in the Abella Proof Assistant.
CoRR
Gopalan Nadathur, Yuting Wang
2017 J jnl
A Higher-Order Abstract Syntax Approach to the Verified Compilation of Functional Programs.
CoRR
Yuting Wang
2016 A conf
A Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs.
ESOP
Yuting Wang, Gopalan Nadathur
2015 — conf
A Proof-theoretic Characterization of Independence in Type Theory.
TLCA
Yuting Wang, Kaustuv Chaudhuri
2015 J jnl
Verified Transformations on Functional Programs Using the Higher-Order Abstract Syntax Approach.
CoRR
Yuting Wang, Gopalan Nadathur
2014 J jnl
Abella: A System for Reasoning about Relational Specifications.
J. Formaliz. Reason.
David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, Yuting Wang
2013 J jnl
Reasoning About Higher-Order Relational Specifications
CoRR
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur
2013 C conf
Reasoning about higher-order relational specifications.
PPDP
Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur
2013 J jnl
Towards Extracting Explicit Proofs from Totality Checking in Twelf.
CoRR
Yuting Wang, Gopalan Nadathur
2013 — conf
Towards extracting explicit proofs from totality checking in twelf.
LFMTP
Yuting Wang, Gopalan Nadathur