编程语言
Non-Interactive Zero Knowledge (NIZK) proofs, such as zkSNARKS, let one prove knowledge of private data without revealing it or interacting with a verifier. While existing tooling focuses on specifying the predicate to be proven, real-world…
Modern deep learning compilers rely on layout abstractions to manage the complex mapping between logical tensor structures and physical memory arrangements. CuTe layouts and Triton linear layouts are widely adopted industry standards.…
We present Cyclotron, a framework and compiler for using recurrence equations to express streaming dataflow algorithms, which then get portably compiled to distributed topologies of interlinked processors. Our framework provides an input…
Galois slicing is a technique for program slicing for provenance, developed by Perera and collaborators. Galois slicing aims to explain program executions by demonstrating how to track approximations of the input and output forwards and…
Current evaluations of LLMs for code generation emphasize functional correctness, overlooking the fact that functionally correct solutions can differ significantly in algorithmic complexity. For instance, an $(O(n^2))$ versus $(O(n \log…
Compilers must check the legality of code transformations to guarantee the correctness of applying a sequence of code transformations to a given code. While such a legality check needs to be precisely computed in general, we can use an…
As the demand for computational power grows, optimizing code through compilers becomes increasingly crucial. In this context, we focus on fully automatic code optimization techniques that automate the process of selecting and applying code…
This paper studies the design of programming languages with handlers of higher-order effectful operations -- effectful operations that may take in computations as arguments or return computations as output. We present and analyse a core…
Hardware accelerators, especially those designed for tensor processing, have become ubiquitous in today's computing landscape. However, even with significant efforts in building compilers, programming these tensor accelerators remains…
In the domain of Programmable Logic Controller (PLC) programming, converting a Ladder Diagram (LD) into a Sequential Function Chart (SFC) is an inherently challenging problem, primarily due to the lack of domain-specific knowledge and the…
In the seminal paper Functional unparsing, Olivier Danvy used continuation passing to reanalyse printf-like format strings as combinators. In the intervening decades, the conversation shifted towards a concurrent line of work --…
We introduce a just-in-time runtime program transformation strategy based on repeated recursion unfolding. Our online program optimization generates several versions of a recursion differentiated by the minimal number of recursive steps…
Relational programming enables program synthesis through a verifier-to-solver approach. An earlier paper introduced a functional conversion that mitigated some of the inherent performance overhead. However, the conversion was inelegant: it…
Large Language Models (LLMs) have achieved remarkable progress in code-related tasks. Despite their advancement, empirical evidence reveals that they still struggle with \emph{deductive code reasoning}, the ability to reason about the…
One critical issue with large language models (LLMs) is their inability to guarantee correctness. Although this problem can be addressed by applying LLMs to formal rewrite systems, current LLMs are still far from adequate to generate sound…
WebAssembly (Wasm) programs may trigger bugs in their engine implementations. To aid debugging, program reduction techniques try to produce a smaller variant of the input program that still triggers the bug. However, existing…
Qubit Mapping is a critical task in Quantum Compilation, as modern Quantum Processing Units (QPUs) are constrained to nearest-neighbor interactions defined by a qubit coupling graph. This compiler pass repairs the connectivity of two-qubit…
miniKanren's key semantic advance over Prolog is to implement a complete yet efficient search strategy, fairly interleaving execution between disjuncts. This fairness is accomplished by bounding how much work is done exploring one disjunct…
This paper introduces a novel paradigm for the analysis and verification of concurrent programs -- the Singularity Theory. We model the execution space of a concurrent program as a branched topological space, where program states are points…
We present Walrus, a functional relational programming language embedded in Haskell that extends the miniKanren model with type-polymorphic unification, on-demand laziness, and a range of usability features aimed at practical development.…