Qianchuan Ye
where else to find them
what they talk about
all 6 in the filters
where they keep going back
- PLDI Workshop Honoring Andreas Podelski2 editions2023–2024
all 5 in the filters
on a stage with
all 21 in the filters
who talks about the same things
- Benjamin Delaware18 talks
- Michael Carbin14 talks
- Yanning Chen2 talks
- Adam Chlipala23 talks
- Steve Zdancewic19 talks
- Justin Hsu13 talks
| title | conference | date |
|---|---|---|
| Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation | OOPSLA 2024 | 2024-10-20 |
A new MPC language called Taypsi compiles ordinary functional programs with recursive ADTs into policy-respecting oblivious implementations using a lifting… | ||
| A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…) | PLDI 2024 | 2024-06-24 |
Describes a toolchain that uses symbolic finite automata to encode data-dependent, temporal representation invariants and integrates them into a refinement… | ||
| Taype: A Policy-Agnostic Language for Oblivious Computation | PLDI 2023 | 2023-06-17 |
Taype provides a policy-agnostic language and a compiler that implements oblivious algebraic data types and tape semantics, translating λOADT+ concepts into a… | ||
| Scrap your boilerplate definitions in 10 lines of Ltac! | CoqPL 2022 | 2022-01-22 |
Library IDT generates new inductive definitions from existing ones by running Template-Coq code driven by small Ltac constructor-transformer tactics, so dozens… | ||
| Oblivious Algebraic Data Types | POPL 2022 | 2022-01-16 |
Presents Lambda OADT, a dependently typed calculus that encodes recursive private data by tagging each type with a public view (e.g. max tree depth) and… | ||
| HACCLE: Metaprogramming for Secure Multi-Party Computation | GPCE 2021 | 2021-10-17 |
HACCLE is a compiler toolchain that embeds a DSL (Harpoon) in Scala, uses LMS metaprogramming to lower code to a protocol‑independent acyclic circuit IR (HIR)… | ||
| nothing matches | ||