Michael Hicks
where else to find them
bluesky:did:plc:ar3iq5andgbyif4ce75f6ydj
linkedin:michaeljhicks
what they talk about
all 8 in the filters
where they keep going back
all 6 in the filters
on a stage with
all 34 in the filters
who talks about the same things
- Derek Dreyer35 talks
- Michael Carbin14 talks
- Shriram Krishnamurthi12 talks
- Ranjit Jhala19 talks
- Bryan Parno22 talks
- Peter Sewell14 talks
| title | conference | date |
|---|---|---|
| Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization | OOPSLA 2024 | 2024-10-20 |
Cedar defines a concise DSL, a Rust evaluation engine, and a Lean formal model that proves key properties; policies compile into SMT in the sound and complete… | ||
| Improving the Stability of Type Safety Proofs in Dafny | Dafny 2024 | 2024-01-14 |
Presents a concrete method for stabilizing Dafny type-soundness proofs by making the safety predicate and then the typechecker opaque, proving small safety… | ||
| Fat Pointers for Temporal Memory Safety of C | OOPSLA 2023 | 2023-10-23 |
Extends Checked C with four new fat pointers that store a key and an offset and enforces temporal safety via dynamic key-lock checks; implements… | ||
| Qunity: A Unified Language for Quantum and Classical Computing | POPL 2023 | 2023-01-15 |
Qunity defines a unified syntax where sum types → direct sum implements operator sums, exception-handling → projective measurement expresses measurements, and… | ||
| C to checked C by 3c | OOPSLA 2022 | 2022-12-05 |
3C is a static-analysis annotation tool that uses two novel algorithms, typ3c and boun3c, to infer Checked C pointer kinds and array bounds; it converts about… | ||
| Verified Compilation of Quantum Oracles | OOPSLA 2022 | 2022-12-05 |
Verified compilation proves an imperative oracle language OQIMP compiles to OQASM and then to SQIR via Coq, preserving semantics and keeping simulation cost… | ||
| Better Learning through Programming Languages | POPL 2022 | 2022-01-16 |
Argues that combining program synthesis with ML lets search scale and tolerate noise by directing search with a network rather than exhaustive enumeration… | ||
| Benefits and Drawbacks of Adopting a Secure Programming Language: Rust as a Case Study | SOUPS 2021 | 2021-08-08 |
Study interviews 16 professional developers and surveys 178 Rust community members n = 16 n = 178 and reports concrete tradeoffs: Rust delivers good compiler… | ||
| From Verified Compilation to Shor's Algorithm | PLanQC 2021 | 2021-06-22 |
A verified compiler stack implements a small IR called Squire and a proven optimizer Vox that preserves denotational semantics across rewrites. The project… | ||
| A Verified Optimizer for Quantum Circuits | POPL 2021 | 2021-01-17 |
VOQC is a fully verified optimizer for quantum circuits implemented in the Coq proof assistant over the SQIR intermediate language; all transformations are… | ||
| Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell | OOPSLA 2020 | 2020-11-15 |
Extension to Liquid Haskell adds refined typeclasses in Liquid Haskell so class laws become checkable at Core; the implementation verifies laws for 34… | ||
| Ask Me Anything with Kathryn McKinley | PLDI 2020 | 2020-06-15 |
Live Q&A explains why the DaCapo suite was born from an NSF review, the DaCapo 20-author process and strict criteria (no user interaction, commercial… | ||
| nothing matches | ||