Some programs use their data cache extensively, while underusing their instruction cache. We embed constant data, typically stored in memory, into the immediate fields of instructions to balance to use of both caches. We illustrate the impacts of such optimizations on the performances of a target program, describing the key …| SYSTEMF @ EPFL
The JVM raw interpreter doesn't perform liveness analysis, so references sometimes persist much too long. Concretely in Scala, this leads to high memory consumption by lazy lists when a parent frame retains a reference to the root of the list. We added a mechanism to the Scala compiler to erase these references.| SYSTEMF @ EPFL
Rocq uses an algorithm with heuristics to test convertibility of terms. While these heuristics work fine for many problems, some simple convertibility problems can take forever. Usually, these problems are between convertible terms obtained using a reduction tactic. We propose to add a convertibility checker that takes a convertibility certificate to speed up convertibility checks in such cases.| SYSTEMF @ EPFL
An annotated guide to adding captureless lookbehinds to the Rust linear-time regex engine.| SYSTEMF @ EPFL
Computations with dependent types often get stuck on rewrites that use opaque lemmas. When the corresponding equality is decidable, these lemmas don't need to be made transparent to unblock computation.| SYSTEMF @ EPFL
