PLDI 2020
2020-06-15..2020-06-20
-- online --
[PLDI 2020, PLDI 2022, PLDI 2023, PLDI 2024, PLDI 2024 Workshop Honoring Andreas Podelski, PLDI 2025, PLDI 2026, PLDI 2026 Student Research Competition]
who it's for
programming language researchers, formal verification engineers, compiler engineers, language tool developers, systems and embedded engineers, engineering managers, program synthesis researchers
topics
incremental compilation and MIR optimizations; unsafe code guidelines for Rust; Miri dynamic checker for undefined behavior; stochastic superoptimization (Stoke); decoupled search and verification; s2 verified TLS stack and Daphne proofs; seL4 microkernel partitioning; Zelkova and Access Analyzer for IAM; Inspector-Executor Generator for sparse tensors; Sparse Polyhedral Framework for auto-tuning; C++20 concepts and modules; Infer compositional static analysis
| title | author | length |
|---|---|---|
| Ask Me Anything with Işıl Dillig | Işıl Dillig, Emina Torlak | 24m |
Covers practical advising tips — co-design problems with students, balance hands-off and hands-on mentorship, and foster group social time — plus concrete… | ||
| Ask Me Anything with Alex Aiken | Alex Aiken, Kathleen Fisher | 39m |
Argues that program synthesis and superoptimization work in practice for small codelets — early Stoke enumerates all 3-line x86 programs and later moves to… | ||
| Ask Me Anything with Byron Cook | Byron Cook, Peter Mueller | 40m |
Amazon shows how formal methods move from prototype to production: teams prove the KMS protocol, verify an in‑house TLS stack called s2 and ship a service that… | ||
| Ask Me Anything with Kathleen Fisher | Kathleen Fisher, Michelle Strout | 48m |
A DARPA program builds vehicles with formally specified components and runs red-team wireless attacks every 18 months; after replacing ad-hoc code with… | ||
| Ask Me Anything with Chris Lattner | Chris Lattner, Cristian Cadar | 34m |
A wide-ranging Q&A covers practical takeaways: tradeoffs between publication and building robust prototypes, why LLVM/Clang/Swift/MLIR grew (modularity… | ||
| Ask Me Anything with Michelle Strout | Michelle Strout, Emery D. Berger | 48m |
Explains why runtime inspectors live in libraries for sparse matrices rather than LLVM/GCC: storage formats vary (index arrays, pointer-based sparse tensors)… | ||
| Ask Me Anything with Bjarne Stroustrup | Bjarne Stroustrup, John Regehr | 56m |
Recommends using C++ for new embedded systems because of performance, ecosystem and evolving safety features; argues that concepts finally give templates… | ||
| Ask Me Anything with Richard Gabriel | Richard Gabriel, Stephen Kell | 53m |
Computational poetry system Inkwell generates programs that then generate poems, using Lisp reflection plus some machine learning so the program can “know” it… | ||
| Ask Me Anything with Felix Klock | Felix Klock, Derek Dreyer | 57m |
A live Q&A at PLDI 2020 explains concrete Rust work: ongoing unsafe code guidelines to write down rules, a dynamic checker implemented in the Miri interpreter… | ||
| Ask Me Anything with Margaret Martonosi | Margaret Martonosi, Adrian Sampson | 27m |
Leads the US computing directorate as assistant director for CISE, stewarding roughly a billion-dollar budget while keeping Princeton tenure and advising… | ||
| Ask Me Anything with Peter O'Hearn | Peter W. O'Hearn, John Wickerson | 48m |
Answers claim a shift from heavy upfront specs to a pay-as-you-go model where small specs give incremental value, and point to concrete tools: Infer team work… | ||
| Ask Me Anything with Kathryn McKinley | Kathryn McKinley, Michael Hicks | 33m |
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… | ||
| Ask Me Anything with Doug Lea | Doug Lea, Laurence Tratt | 38m |
Answers about practical concurrency trade-offs and concrete Java work: advocates divide-and-conquer parallelism and non-blocking synchronization, explains why… | ||
| Ask Me Anything with Simon Peyton Jones | Simon Peyton Jones, Benjamin Pierce | 52m |
A wide-ranging AMA covers Haskell tradeoffs and real projects: GHC uses a GHC Core typed intermediate language to keep transformations type-safe, experiments… | ||
| Ask Me Anything with Guy Steele | Guy Steele, Jan Vitek | 45m |
Long Q&A that hits concrete projects and lessons: explains the telnet song as a real exponential-escape-character example, evaluates persistent memory vs… | ||
| nothing matches | ||