Emina Torlak
where else to find them
what they talk about
where they keep going back
- OOPSLA2 editions2023–2024
all 5 in the filters
on a stage with
all 19 in the filters
who talks about the same things
- Sorawee Porncharoenwase4 talks
- Rastislav Bodík8 talks
- Işıl Dillig21 talks
- Amal Ahmed25 talks
- Loris D'Antoni17 talks
- Adam Chlipala23 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… | ||
| A Pretty Expressive Printer | OOPSLA 2023 | 2023-10-23 |
Claims a new printer Πe that is strictly more expressive than prior pretty printers, provably minimizes a user-chosen optimality objective via a Cost Factory… | ||
| A Formal Foundation for Symbolic Evaluation with Merging | POPL 2022 | 2022-01-16 |
New formal symbolic semantics incorporates state merging and a parameterized symbolic factory and is mechanized in Lean, proving soundness, completeness… | ||
| Ask Me Anything with Işıl Dillig | PLDI 2020 | 2020-06-15 |
Covers practical advising tips — co-design problems with students, balance hands-off and hands-on mentorship, and foster group social time — plus concrete… | ||
| Synthesis and Verification for All | Clojure/west 2017 | 2017-03-30 |
Rosette is a Racket-based language that compiles interpreters to solver constraints via a symbolic virtual machine, exposing six solver-aware constructs so a… | ||
| nothing matches | ||