Programming Languages
Recent deep learning workloads increasingly push computational demand beyond what current memory systems can sustain, with many kernels stalling on data movement rather than computation. While modern dataflow accelerators incorporate…
Stream-based monitoring is a real-time safety assurance mechanism for complex cyber-physical systems such as unmanned aerial vehicles. In this context, a monitor aggregates streams of input data from sensors and other sources to give…
The theory of sequences, supported by many SMT solvers, can model program data types including bounded arrays and lists. Sequences are parameterized by the element data type and provide operations such as accessing elements, concatenation,…
We report on our tool, Pulse Infinite, that uses proof techniques to show non-termination (divergence) in large programs. Pulse Infinite works compositionally and under-approximately: the former supports scale, and the latter ensures…
AI-assisted programming greatly increases software development performance. We enhance this potential by integrating transparency through domain-specific modeling techniques and providing instantaneous, graphical visualizations that…
Code generation, symbolic math reasoning, and other tasks require LLMs to produce outputs that are both syntactically and semantically correct. Constrained LLM generation is a promising direction to enforce adherence to formal grammar, but…
Image editing is a common task across a wide range of domains, from personal use to professional applications. Despite advances in computer vision, current tools still demand significant manual effort for editing tasks that require…
Operating system kernels employ virtual memory subsystems, which use a CPU's memory management units (MMUs) to virtualize the addresses of memory regions Operating systems manipulate these virtualized memory mappings to isolate untrusted…
Many natural program correctness properties can be stated in terms of symmetries, but existing formal methods have little support for reasoning about such properties. We consider how to formally verify a broad class of symmetry properties…
Algorithmic type checking and inference of reachability types present a particular challenge with regards to subtyping. As a restricted form of dependent types, reachability types are subject to the avoidance problem: a variable mentioned…
We present a type-theoretic framework for reasoning about incorrectness in functional programs that interact with effectful, opaque library APIs. Our approach centers on traces -- temporally-ordered sequences of library API invocations --…
A coverage type generalizes refinement types found in many functional languages with support for must-style underapproximate reasoning. Property-based testing frameworks are one particularly useful domain where such capabilities are useful…
The computational fabrication pipeline for 3D printing is much like a compiler - users design models in Computer Aided Design (CAD) tools that are lowered to polygon meshes to be ultimately compiled to machine code by 3D slicers. For…
Esoteric programming languages are challenging to learn, but their unusual features and constraints may serve to improve programming ability. From languages designed to be intentionally obtuse (e.g. INTERCAL) to others targeting artistic…
In this paper, we investigate the fundamental laws of quantum programming. We extend a comprehensive set of Hoare et al.'s basic laws of classical programming to the quantum setting. These laws characterise the algebraic properties of…
This paper describes a new abstract interpretation-based approach to verify temporal safety properties of recursive, higher-order programs. While prior works have provided theoretical impact and some automation, they have had limited…
We present CrossTL, a universal programming language translator enabling bidirectional translation between multiple languages through a unified intermediate representation called CrossGL. Traditional approaches require separate translators…
The goal of active learning for program synthesis is to synthesize the desired program by asking targeted questions that minimize user interaction. While prior work has explored active learning in the purely symbolic setting, such…
Local reasoning about programs that combine aliasing and mutable state is a longstanding challenge. Existing approaches -- ownership systems, linear and affine types, uniqueness types, and lexical effect tracking -- impose global…
It is commonly known that any Bayesian network can be implemented as a probabilistic program, but the reverse direction is not so clear. In this work, we address the open question to what extent a probabilistic program with user-labelled…