Publications
Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation
Qianchuan Ye and Benjamin Delaware
Proceedings of the ACM on Programming Languages, Volume 8 (OOPSLA1), 2024
[Open access] [Artifact]
A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata
Zhe Zhou, Qianchuan Ye, Benjamin Delaware, and Suresh Jagannathan
Proceedings of the ACM on Programming Languages, Volume 8 (PLDI), 2024
[Open access] [Artifact]Taype: A Policy-Agnostic Language for Oblivious Computation
Qianchuan Ye and Benjamin Delaware
Proceedings of the ACM on Programming Languages, Volume 7 (PLDI), 2023
[Open access] [Talk] [Artifact]RHLE: Modular Deductive Verification of Relational ∀∃ Properties
Robert Dickerson, Qianchuan Ye, Michael K. Zhang, and Benjamin Delaware
Programming Languages and Systems, Lecture Notes in Computer Science (APLAS), 2022
[Open access] [Artifact]
Oblivious Algebraic Data Types
Qianchuan Ye and Benjamin Delaware
Proceedings of the ACM on Programming Languages, Volume 6 (POPL), 2022
[Open access] [Talk] [Artifact]HACCLE: Metaprogramming for Secure Multi-Party Computation
Yuyan Bao, Kirshanthan Sundararajah, Raghav Malik, Qianchuan Ye, Christopher Wagner, Fei Wang, Mohammad Hassan Ameri, Donghang Lu, Alexander Seto, Benjamin Delaware, Roopsha Samanta, Aniket Kate, Christina Garman, Jeremiah Blocki, Pierre-David Letourneau, Benoit Meister, Jonathan Springer, Tiark Rompf, and Milind Kulkarni
Proceedings of the 20th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE), 2021
[Open access] [Artifact]Narcissus: Correct-by-Construction Derivation of Decoders and Encoders from Binary Formats
Benjamin Delaware, Sorawit Suriyakarn, Clément Pit-Claudel, Qianchuan Ye, and Adam Chlipala
Proceedings of the ACM on Programming Languages, Volume 3 (ICFP), 2019
[Open access] [Artifact]A Verified Protocol Buffer Compiler
Qianchuan Ye and Benjamin Delaware
Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), 2019
[URL] [Local copy]
Workshops
- Scrap your boilerplate definitions in 10 lines of Ltac!
Qianchuan Ye and Benjamin Delaware
The Eighth International Workshop on Coq for Programming Languages (CoqPL), 2022
[Open access] [Talk] [Artifact]
Dissertations
- Language-Based Techniques for Policy-Agnostic Oblivious Computation
Qianchuan Ye
PhD Dissertation, Purdue University, April 2024
[Open access]