Joshua Gancher
where else to find them
what they talk about
all 5 in the filters
where they keep going back
no series more than once — all 5 in the filters
on a stage with
all 15 in the filters
who talks about the same things
- Zhengyao Lin4 talks
- Adam Chlipala23 talks
- Bryan Parno22 talks
- Benjamin Delaware18 talks
- Jonathan Aldrich17 talks
- Yizhou Zhang13 talks
| title | conference | date |
|---|---|---|
| OwlC: Compiling Security Protocols to Verified, Secure... | USENIX Security '25 | 2025-08-13 |
OwlC compiles Owl protocol specifications into side‑channel‑resistant Rust libraries and mechanically verifies their fidelity to an itrees specification using… | ||
| Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust | USENIX Security '25 | 2025-08-13 |
Vest generates Rust zero-copy parsers and in-place serializers from an RFC-like DSL, proves memory safety plus soundness, completeness, non-malleability and… | ||
| ILA: Correctness via Type Checking for Fully Homomorphic Encryption | PriSC 2025 (with POPL 2025) | 2025-01-20 |
ILA is an intermediate language that attaches quantitative bounds (plaintext range and ciphertext noise) as types and proves that well-typed ILA circuits… | ||
| FlowCert: Translation Validation for Asynchronous Dataflow Programs via Dynamic(…) | OOPSLA 2024 | 2024-10-20 |
FlowCert implements translation validation from LLVM to asynchronous dataflow graphs for the RipTide CGRA by constructing a deterministic canonical schedule… | ||
| Universally Composable Security for Program Partitioning | PriSC 2023 | 2023-01-21 |
An implemented compiler called Viaduct compiler takes a single-threaded program with tuple information-flow labels (confidentiality, integrity) and… | ||
| A Core Calculus for Equational Proofs of Cryptographic Protocols | POPL 2023 | 2023-01-15 |
Introduces a tiny process calculus and an equation-of-logic that proves observational equivalence for distributed crypto by rewriting networks of probabilistic… | ||
| nothing matches | ||