You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Authors: "Clément Allain (Inria), Basile Clément (OCamlPro), Alexandre Moine (Inria), Gabriel Scherer (Université Paris Cité, Inria, CNRS, IRIF)"
26
+
Venue: ICFP 2024
27
+
NominationStatement: |
28
+
Backtracking is a common technique in type checkers, theorem provers, and
29
+
constraint solvers, yet adding it to an existing imperative data structure
30
+
typically means either a full copy on each snapshot (expensive when
31
+
snapshots are frequent) or switching to persistent maps (a logarithmic
32
+
overhead on every access, paid even when no backtracking occurs). This paper
33
+
presents a snapshottable store---a bag of mutable references whose state can
34
+
be efficiently captured and restored---that avoids both pitfalls. The key
35
+
idea, extending a 1978 technique by Baker, is a journaled version tree where
36
+
the current state lives in ordinary references and past states are recovered
37
+
by replaying a log. A "record elision" optimisation ensures that reads and
38
+
writes cost essentially the same as plain references when snapshots are
39
+
infrequent, making the library a safe default even when backtracking is
40
+
rare. The implementation is short, subtle, and mechanically verified in Rocq
41
+
using Iris. The paper takes a simple, useful idea, works out the engineering
42
+
and correctness details thoroughly, and presents the result with clarity and
43
+
good taste.
44
+
45
+
46
+
- Title: "_[Implementation and Synthesis of Math Library Functions](https://dl.acm.org/doi/10.1145/3632874)_"
47
+
Authors: "Ian Briggs (University Of Utah), Yash Lad (University Of Utah), Pavel Panchekha (University Of Utah)"
48
+
Venue: POPL 2024
49
+
NominationStatement: |
50
+
Math library functions like `exp`, `sin`, and `log` are critical
51
+
infrastructure, yet implementing them well requires rare expertise. This
52
+
paper introduces MegaLibm, a domain-specific language whose type system
53
+
catches mathematical mistakes at compile time, whose compositional design
54
+
allows complex algorithms to be built from simple, verifiable pieces, and
55
+
whose tuning parameters separate high-level design from low-level precision
56
+
choices. Its type-directed synthesis algorithm using e-graphs can generate
57
+
complete implementations from scratch. MegaLibm replicates 8
58
+
state-of-the-art implementations in far less code, produces improved
59
+
variations, and even uncovers a bug in VDT's cosine. The paper is a nice
60
+
example of applying Programming Lanugage ideas, such as typing,
61
+
compositionality, and synthesis, opening up a domain that has long been
62
+
inaccessible to non-specialists.
63
+
1
64
Selected February 2025:
2
65
3
66
- Title: "_[A Grounded Conceptual Model for Ownership Types in Rust](https://dl.acm.org/doi/10.1145/3622841)_"
@@ -17,7 +80,7 @@ Selected February 2025:
17
80
Overall, the paper follows scientific principles and introduces
18
81
the PL community to an original and effective way to study a
19
82
language usability problem.
20
-
83
+
CACMSelection: true
21
84
22
85
- Title: "_[Dynamic Race Detection with O(1) Samples](https://dl.acm.org/doi/10.1145/3571238)_"
23
86
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)"
@@ -43,6 +106,7 @@ Selected February 2025:
43
106
The use of sampling to improve the performance of a data race
44
107
detector has been previously explored, but this work extends and
45
108
analyzes that idea.
109
+
CACMSelection: true
46
110
47
111
- Title: "_[Catala: a Programming Language for the Law](https://dl.acm.org/doi/10.1145/3473582)_"
48
112
Authors: "Denis Merigoux (INRIA), Nicolas Chataing (ENS Paris), Jonathan Protzenko (Microsoft Research)"
@@ -71,6 +135,7 @@ Selected February 2025:
71
135
paper is extremely well written and accessible. Egg has already
72
136
been quite influential, which numerous follow-on papers,
73
137
industrial adoption, an annual workshop, and a growing community.
138
+
CACMSelection: true
74
139
75
140
Selected September 2021:
76
141
@@ -88,7 +153,15 @@ Selected September 2021:
88
153
reuse properly for the first time. As a result we can enjoy elegance, and
89
154
state-of-the-art performance, both at the same time. Sometimes we can have
90
155
our cake and eat it too.
91
-
CACMSelection: true
156
+
CACMHighlight:
157
+
Date: March 2023
158
+
Title: "Achieving High Performance the Functional Way: Expressing High-Performance Optimizations as Rewrite Strategies"
159
+
Link: https://dl.acm.org/doi/abs/10.1145/3580371
160
+
TechnicalPerspective:
161
+
Title: 'Reconsidering the Design of User-Schedulable Languages'
162
+
Link: https://dl.acm.org/doi/10.1145/3580370
163
+
Author: Jonathan Ragan-Kelley
164
+
92
165
93
166
- Title: "_[Learning-based Memory Allocation for C++ Server Workloads](https://dl.acm.org/doi/10.1145/3373376.3378525)_"
94
167
Authors: "Martin Maas (Google), David Andersen (CMU), Michael Isard (Google), Mohammad Mahdi (Facebook), Kathryn S McKinley (Google), Colin Raffel (University of North Carolina)"
@@ -149,7 +222,14 @@ Selected September 2021:
149
222
interest, which demonstrates for the first time that one can obtain
150
223
deterministic certificates on properties of the training phase of
151
224
realistic machine learning models.
152
-
CACMSelection: true
225
+
CACMHighlight:
226
+
Date: January 2023
227
+
Title: "Proving Data-Poisoning Robustness in Decision Trees"
228
+
Link: https://dl.acm.org/doi/abs/10.1145/3576894
229
+
TechnicalPerspective:
230
+
Title: 'Beautiful Symbolic Abstractions for Safe and Secure Machine Learning'
0 commit comments