编程语言

Program verification is vital for ensuring software reliability, especially in the context of increasingly complex systems. Loop invariants, remaining true before and after each iteration of loops, are crucial for this verification process.…

Domain-specific languages (DSLs) are integral to various software workflows. Such languages offer domain-specific optimizations and abstractions that improve code readability and maintainability. However, leveraging these languages requires…

This paper explores the potential of communicating information gained by static analysis from compilers to Out-of-Order (OoO) machines, focusing on the memory dependence predictor (MDP). The MDP enables loads to issue without all in-flight…

Traditionally, designs are written in Verilog hardware description language (HDL) and debugged by hardware engineers. While this approach is effective, it is time-consuming and error-prone for complex designs. Large language models (LLMs)…

Despite an abundance of proposed systems, the verification of units-of-measure within programs remains rare in scientific computing. We attempt to address this issue by providing a lightweight static verification system for units-of-measure…

Semantics-Guided Synthesis (SemGuS) is a programmable framework for defining synthesis problems in a domain- and solver-agnostic way. This paper presents the standardized SemGuS format, together with an open-source toolkit that provides a…

Automatically creating a computer program using input-output examples can be a challenging task, especially when trying to synthesize computer programs that require loops or recursion. Even though the use of recursion can make the…

Functional choreographic programming suggests a new propositions-as-types paradigm might be possible. In this new paradigm, communication is not modeled linearly; instead, ownership of a piece of data is modeled as a modality, and…

We present ExpIris, a separation logic framework for the (amortized) expected cost analysis of probabilistic programs. ExpIris is based on Iris, parametric in the language and the cost model, and supports both imperative and functional…

We explore the use of Large Language Models (LLMs) to generate high-quality Register-Transfer Level (RTL) code with minimal human interference. The traditional RTL design workflow requires human experts to manually write high-quality RTL…

We introduce the third major version of Metatheory.jl, a Julia library for general-purpose metaprogramming and symbolic computation. Metatheory.jl provides a flexible and performant implementation of e-graphs and Equality Saturation (EqSat)…

Memory persistency models provide a foundation for persistent programming by specifying which (and when) writes to non-volatile memory (NVM) become persistent. Memory persistency models for the Intel-x86 and Arm architectures have been…

Currently, there is a gap between the tools used by probability theorists and those used in formal reasoning about probabilistic programs. On the one hand, a probability theorist decomposes probabilistic state along the simple and natural…

Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and recursion, arrays in linear algebra demand constant-time…

State-of-the-art sequential reasoning in Large Language Models (LLMs) has expanded the capabilities of Copilots beyond conversational tasks to complex function calling, managing thousands of API calls. However, the tendency of compositional…

The naive combination of polymorphic effects and polymorphic type assignment has been well known to break type safety. Existing approaches to this problem are classified into two groups: one for restricting how effects are triggered and the…

Handling bound identifiers correctly and efficiently is critical in implementations of compilers, proof assistants, and theorem provers. When choosing a representation for abstract syntax with binders, implementors face a trade-off between…

Machine learning has become an effective tool for automatically annotating unstructured data (e.g., images) with structured labels (e.g., object detections). As a result, a new programming paradigm called neurosymbolic programming has…

This paper introduces a model theory for resolution on Higher Order Hereditarily Harrop formulae (HOHH), the logic underlying the Lambda-Prolog programming language, and proves soundness and completeness of resolution. The semantics and the…

Most automated program verifiers for separation logic use either symbolic execution or verification condition generation to extract proof obligations, which are then handed over to an SMT solver. Existing verification algorithms are…