Qianchuan Ye

About

I am currently a PhD Candidate of Computer Science at Purdue University, advised by Benjamin Delaware.

My research interests lie in proof assistants, type theory and programming languages, program verification and synthesis, and broadly anything about proofs.

CV

Publications

• Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation
  Qianchuan Ye and Benjamin Delaware
  Accepted to OOPSLA 2024
  Draft  Artifact

• A HAT Trick: Automatically Verifying Representation Invariants Using Symbolic Finite Automata
  Zhe Zhou, Qianchuan Ye, Benjamin Delaware, and Suresh Jagannathan
  Conditionally Accepted to PLDI 2024

• Taype: A Policy-Agnostic Language for Oblivious Computation
  Qianchuan Ye and Benjamin Delaware
  Proceedings of the 44th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2023)
  Open access  Talk  Artifact

• RHLE: Modular Deductive Verification of Relational ∀∃ Properties
  Robert Dickerson, Qianchuan Ye, Michael K. Zhang, and Benjamin Delaware
  Proceedings of the 20th Asian Symposium on Programming Languages and Systems (APLAS 2022)
  Open access  Artifact

• Oblivious Algebraic Data Types
  Qianchuan Ye and Benjamin Delaware
  Proceedings of the 49th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (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 24th ACM SIGPLAN International Conference on Functional Programming (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