编程语言
Strong call-by-need combines full normalization with the sharing discipline of lazy evaluation, yet no prior implementation achieved both simplicity and efficiency. We introduce RKNL, an abstract machine that realizes strong call-by-need…
In service-oriented architecture, services coordinate in one of two ways: directly, using point-to-point communication, or indirectly, through an intermediary called the orchestrator. Orchestrators tend to be more popular because their…
How do LLMs compare with symbolic tools on program synthesis tasks? We investigate this question on several synthesis domains: LTL reactive synthesis, syntax-guided synthesis, distributed protocol synthesis, and recursive function…
We extend the semantics and type system of a lambda calculus equipped with common constructs to be "resource-aware". That is, the semantics keeps track of the usage of resources, and is stuck, besides in case of type errors, if either a…
Accattoli, Dal Lago, and Vanoni have recently proved that the space used by the Space KAM, a variant of the Krivine abstract machine, is a reasonable space cost model for the lambda-calculus accounting for logarithmic space, solving a…
Quantum error correction (QEC) enables reliable computation on noisy hardware by encoding logical information across many physical qubits and periodically measuring parities to detect errors. A decoder is the classical algorithm that uses…
Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that the IVL program is correct. Soundness of such translational…
When the MLIR project was first introduced, it promised to address the issues that the HLS community had with the LLVM project. But is this really the case, and is MLIR the "right"/"best" compiler infrastructure for HLS? We here share our…
Live programming systems aim to quickly show programmers the dynamic impacts of program edits. To do so, they re-execute the program whenever it is edited, which poses a computational challenge when programs become large or complex. This…
Symbolic execution is a powerful program analysis technique, but its effectiveness is fundamentally limited by solver-hostile program fragments, complex numerical reasoning, and unbounded heap structures. Recent work proposed replacing…
Peephole optimizations are a core component of modern optimizing compilers. It rewrites specific instruction into semantically equivalent but more efficient forms. In practice, creating a new peephole optimization often starts from a…
Sparse Tensor Compilers (STCs) have emerged as critical infrastructure for optimizing high-dimensional data analytics and machine learning workloads. The STCs must synthesize complex, irregular control flow for various compressed storage…
As the ECMAScript specification evolves, industrial-scale JavaScript compilers face the challenge of supporting modern language syntax while maintaining compatibility for diverse execution environments. Traditionally, compilers solve this…
Hierarchical graph rewriting is a highly expressive computational formalism that manipulates graphs enhanced with box structures for representing hierarchies. It has provided the foundations of various graph-based modeling tools, but the…
Large Language Models (LLMs) can solve previously intractable tasks given only natural-language instructions and a few examples, but they remain difficult to steer precisely and lack a key capability for building reliable software at scale:…
The rise of large language models (LLMs) has introduced a new type of programming: natural language programming. Users write prompts, which are instructions in natural language, to direct LLMs to perform tasks such as natural language…
The languages of mathematical physics and modelling are endowed with a rich ``grammar of dimensions'' that common abstractions of programming languages fail to represent. We propose a dependently typed domain-specific language (embedded in…
In computer science, students are encouraged to learn various programming languages such as Python, C++, and Java, equipping them with a broad range of technical skills and problem-solving capabilities. Nevertheless, the design of objective…
Hash-based maps, particularly java.util.HashMap, are pervasive in Java applications and the JVM, making their performance critical. Evaluating optimizations is challenging because performance depends on factors such as operation patterns,…
This thesis develops a system for automatically analyzing and improving dynamic programs, such as those that have driven progress in natural language processing and computer science, more generally, for decades. Finding a correct program…