Automatic Differentiation (AD) is at the core of all machine learning frameworks and has applications in scientific computing as well. Theoretical research on reverse-mode AD focuses on functional, higher-order languages, enabling AD to be formulated as a series of local, concise program rewrites. These theoretical approaches focus on correctness but disregard efficiency. Practical implementations, however, employ mutation and taping techniques to enhance efficiency. This approach, however, necessitates intricate, low-level, and non-local program transformations. In this work, we introduce MimIrADe, a functionally inspired AD technique implemented within a higher-order, graph-based ("sea of nodes") intermediate representation (IR). Our method consists of a streamlined implementation and incorporates standard optimizations, resulting in an efficient AD system. The higher-order nature of the IR enables us to utilize concise functional AD methods, expressing AD through local rewrites. This locality facilitates modular high-level extensions, such as matrix operations, in a straightforward manner. Additionally, the graph-based structure of the IR ensures that critical implementation aspects---particularly the handling of shared pullback invocations---are managed naturally and efficiently. Our AD pass supports a comprehensive set of features, including non-scalar types, pointers, and higher-order recursive functions. We demonstrate through standard benchmarks that a suite of common optimizations effectively eliminates the overhead typically associated with functional AD approaches, producing differentiated code that performs on par with leading mutation and taping techniques. At the same time, MimIrADe's implementation is an order of magnitude less complex compared to its contenders.

Recently, AlphaDev has shown significant advances in the synthesis of branchless sorting kernels for arrays of lengths 3 to 5. In this paper, we propose an enumerative search technique based on A* search and present novel optimality-pre­serving heuristics and non-optimality-preserving cuts for sorting kernel synthesis. Our algorithm outperforms AlphaDev in synthesis time by two orders of magnitude ran on a standard notebook instead of a TPU cluster. Because our algorithm can explore the solution space, we are able to enumerate all correct sorting kernels for length 3 and simply select the best-performing one. For larger array lengths, we intelligently sample the solution space and find a sorting kernel that outperforms the state-of-the-art. Furthermore, we establish a new tight lower bound for the shortest sorting kernel for length 4. Finally, we provide a comprehensive comparison against several other existing synthesis techniques and show that none of them is able to synthesize sorting kernels for arrays longer than 3.

Traditional compilers, designed for optimizing low-level code, fall short when dealing with modern, computation-heavy applications like image processing, machine learning, or numerical simulations. Optimizations should understand the primitive operations of the specific application domain and thus happen on that level. Domain-specific languages (DSLs) fulfill these requirements. However, DSL compilers reinvent the wheel over and over again as standard optimizations, code generators, and general infrastructure & boilerplate code must be reimplemented for each DSL compiler. This paper presents MImIR, an extensible, higher-order intermediate representation. At its core, MImIR is a pure type system and, hence, a form of a typed lambda calculus. Developers can declare the signatures of new (domain-specific) operations, called axioms . An axiom can be the declaration of a function, a type constructor, or any other entity with a possibly polymorphic, polytypic, and/or dependent type. This way, developers can extend MImIR at any low or high level and bundle them in a plugin . Plugins extend the compiler and take care of optimizing and lowering the plugins' axioms. We show the expressiveness and effectiveness of MImIR in three case studies: Low-level plugins that operate at the same level of abstraction as LLVM, a regular-expression matching plugin, and plugins for linear algebra and automatic differentiation. We show that in all three studies, MImIR produces code that has state-of-the-art performance.

Electrical impedance tomography (EIT) uses current-voltage measurements on the surface of an imaging subject to detect conductivity changes or anomalies. EIT is a promising new technique with great potential in medical imaging and non-destructive testing. However, in many applications, EIT suffers from inconsistent reliability due to its enormous sensitivity to modeling and measurement errors. In this work, we show that it is principally possible to give rigorous resolution guarantees in EIT even in the presence of systematic and random measurement errors. We derive a constructive criterion to decide whether a desired resolution can be achieved in a given measurement setup. Our results cover the case where anomalies of a known minimal contrast in a subject with imprecisely known background conductivity are to be detected from noisy measurements on a number of electrodes with imprecisely known contact impedances. The considered settings are still idealized in the sense that the shape of the imaging subject has to be known and the allowable amount of uncertainty is rather low. Nevertheless, we believe that this may be a starting point to identify new applications and to design and optimize measurement setups in EIT.