|
| 1 | +Selected February 2025: |
| 2 | + |
| 3 | +- Title: "_[A Grounded Conceptual Model for Ownership Types in Rust](https://dl.acm.org/doi/10.1145/3622841)_" |
| 4 | + Authors: "Will Crichton (Brown University), Gavin Gray (ETH Zurich), Shriram Krishnamurthi (Brown University)" |
| 5 | + Venue: OOPSLA 2023 |
| 6 | + NominationStatement: | |
| 7 | + Programmers learning Rust struggle to understand ownership types, |
| 8 | + Rust’s core mechanism for ensuring memory safety without garbage |
| 9 | + collection. This paper describes an attempt to systematically |
| 10 | + design a pedagogy for ownership types. The paper applies |
| 11 | + techniques from cognitive science to describing and teaching |
| 12 | + programming languages, focusing on one of the “hottest” languages |
| 13 | + to date: Rust. The work contains multiple aspects, such as |
| 14 | + analysing common misconceptions of the programmers, building the |
| 15 | + conceptual model of Rust ownership, designing a teaching |
| 16 | + methodology around it, and even evaluating it in a user study. |
| 17 | + Overall, the paper follows scientific principles and introduces |
| 18 | + the PL community to an original and effective way to study a |
| 19 | + language usability problem. |
| 20 | +
|
| 21 | +
|
| 22 | +- Title: "_[Dynamic Race Detection with O(1) Samples](https://dl.acm.org/doi/10.1145/3571238)_" |
| 23 | + Authors: "Mosaad Al Thokair (University of Illinois at Urbana-Champaign), Minjian Zhang (University of Illinois at Urbana-Champaign), Umang Mathur (National University of Singapore), Mahesh Viswanathan (University of Illinois at Urbana-Champaign)" |
| 24 | + Venue: POPL 2023 |
| 25 | + NominationStatement: | |
| 26 | + This paper proposes to use the property testing paradigm to design |
| 27 | + and analyze a randomized race detector. The detector samples |
| 28 | + subtracts and looks for races in them in the regular way, but will |
| 29 | + only find races that are included in these sub-traces. The |
| 30 | + motivation to consider subtracts is to improve performance and |
| 31 | + possibly allow using this checker in a production environment. |
| 32 | + When a date race is found, the execution surely contains a race, |
| 33 | + and when the full trace is "epsilon-far" from a trace with no data |
| 34 | + races, then the test is shown to find a race with a good |
| 35 | + probability. The authors implement such a tester and show that it |
| 36 | + does well within its promise and also does well even beyond what |
| 37 | + can be shown formally. |
| 38 | +
|
| 39 | + This paper appears very strong for the parallel computing |
| 40 | + community and intriguing for the property testing community as an |
| 41 | + application of property testing in a practical setting. Its |
| 42 | + primary contribution lies in connecting these two domains. The use |
| 43 | + of sampling to improve the performance of a data race detector has |
| 44 | + been previously explored, but this work extends and analyzes that |
| 45 | + idea. |
| 46 | +
|
| 47 | +- Title: "_[Catala: a Programming Language for the Law](https://dl.acm.org/doi/10.1145/3473582)_" |
| 48 | + Authors: "Denis Merigoux (INRIA), Nicolas Chataing (ENS Paris), Jonathan Protzenko (Microsoft Research)" |
| 49 | + Venue: ICFP 2021 |
| 50 | + NominationStatement: | |
| 51 | + Catala is a new programming language designed to formalize |
| 52 | + statutory law into executable code. The paper presents a novel and |
| 53 | + compelling application of so-called prioritized default logic to |
| 54 | + legal interpretation. The work is particularly impressive for its |
| 55 | + significant engineering effort and its close collaboration with |
| 56 | + legal professionals, demonstrating both feasibility and real-world |
| 57 | + applicability. |
| 58 | +
|
| 59 | +
|
| 60 | +- Title: "_[egg: Fast and extensible equality saturation](https://dl.acm.org/doi/10.1145/3434304)_" |
| 61 | + Authors: "Max Willsey (University of Washington), Chandrakana Nandi (University of Washington), Yisu Remy Wang (University of Washington), Oliver Flatt (University of Utah), Zachary Tatlock (University of Washington), Pavel Panchekha (University of Utah)" |
| 62 | + Venue: POPL 2021 |
| 63 | + NominationStatement: | |
| 64 | + Egg is a framework for optimizing term representations based on |
| 65 | + e-graphs and equality saturation. It has numerous applications in |
| 66 | + compiler optimization, program synthesis, term rewriting, and |
| 67 | + more. While the ideas and even their combination were known, this |
| 68 | + paper developed three key innovations: algorithmic improvements |
| 69 | + based on rebuilding, a framework for performing lattice-based |
| 70 | + analyses using e-graphs, and a standalone implementation. The |
| 71 | + paper is extremely well written and accessible. Egg has already |
| 72 | + been quite influential, which numerous follow-on papers, |
| 73 | + industrial adoption, an annual workshop, and a growing community. |
| 74 | +
|
1 | 75 | Selected September 2021: |
2 | 76 |
|
3 | 77 | - Title: "_[Achieving high-performance the functional way: a functional pearl on expressing high-performance optimizations as rewrite strategies](https://dl.acm.org/doi/10.1145/3408974)_" |
|
0 commit comments