New Jersey
Programming Languages and Systems
Seminar

Nondeterminism makes parallel programs challenging to write and reason about. To avoid these challenges, researchers have developed techniques for internally deterministic parallel programming, in which the steps of a parallel computation proceed in a deterministic way. Internal determinism is useful because it lets a programmer reason about a program as if it executed in a sequential order. However, no verification framework exists to exploit this property and simplify formal reasoning.

To capture the essence of why internally deterministic programs should be easier to reason about, we define a property called schedule-independent safety. A program satisfies schedule-independent safety, if, to show that the program is safe across all interleavings, it suffices to show that one terminating execution of the program is safe. We then present Musketeer, a separation logic for proving that a program satisfies schedule-independent safety. Once schedule independence is guaranteed, correctness can be shown in Angelic, a companion logic in which the user may select interactively one sequential interleaving and reason about it alone.

Using Musketeer, we prove the soundness of MiniDet, an affine type system for enforcing internal determinism. All results are mechanized in Rocq on top of the Iris separation logic framework.

Identifying dependencies between parallel tasks on-the-fly, or parallel order maintenance, lies at the heart of dynamic race detection, disentanglement checks, and other runtime techniques for parallel programs. We present DePa*, a parallel order maintenance algorithm for structured futures. DePa* strictly supersedes the current algorithm used by the MaPLe (MPL) runtime for disentanglement checks in fork-join programs, adding support for futures without affecting the efficiency of fork-join programs.

DePa* labels tasks in a computation with unique, compact tags that contain enough information to perform reachability queries on. The vertex labeling approach grants two practical advantages to the algorithm: scheduler-agnosticism and extensibility. Firstly, DePa* makes no assumptions about the underlying scheduling strategy, and thus can be integrated into many runtimes. Furthermore, the unique vertex labels can be extended/repurposed for graph visualization or fine-grained profiling. DePa* is ongoing work; we have an initial algorithm and a proof sketch, and are working towards a proof of correctness and a formal analysis of efficiency. We seek the NJPLS community’s insights on concrete implementing DePa* and interesting use cases for unique vertex labeling.

Effect handlers and multishot continuations are powerful abstractions for managing control flow; together, they offer concise and modular ways to express and handle nondeterminism, randomness, and more. However, implementing multishot continuations in the presence of stack-allocated lexical resources—lexical effect handlers in particular—is challenging, since stack copying invalidates references to these resources.

In this talk, I will present a novel implementation strategy for lexical effect handlers that fully supports multishot continuations. The key idea is to virtualize the stack space used by continuations. Each stack-allocated handler instance is assigned a virtual address, and all effect invocations through these virtual addresses are mediated by an address translation mechanism. A software-based memory management unit in the runtime system performs these translations efficiently, exploiting the lexical scoping discipline of effect handlers.

We capture the essence of our approach via a new operational semantics for lexical effect handlers and prove it correct with respect to the standard semantics. We also implement it in a compiler and runtime system. Compared to prior languages with lexical effect handlers, our implementation increases expressivity by fully supporting multishot continuations—and, as a happy consequence, unlocks significant performance gains by enabling parallel execution of multishot continuations.

In this talk, we show how to retrofit purity onto an impure language with first-class mutable references using a modal type system. We introduce a pair of modal axes: statefulness and visibility. The former indicates whether a function depends on captured mutable state, while the latter controls how reference cells can be accessed. We support creating reference cells that remain local to pure functions, allowing for efficient imperative implementations.

We demonstrate our approach in OxCaml (OCaml with Jane Street's extensions), building on the existing mode system. Our compiler extension has been deployed in production code and is available as open source.

Property-based testing (PBT) relies on generators for random test cases, often constructed using embedded domain specific languages, which provide expressive combinators for building and composing generators. The effectiveness of PBT depends critically on the speed of these generators. However, careful measurements show that the generator performance of widely used PBT libraries falls well short of what is possible, due principally to (1) the abstraction overhead of their combinator-heavy style and (2) suboptimal sources of randomness. We characterize, quantify, and address these bottlenecks. To eliminate abstraction overheads, we propose a technique based on multi-stage programming, dubbed Allegro. We apply this technique to leading generator libraries in OCaml and Scala 3, significantly improving performance. To quantify the performance impact of the randomness source, we carry out a controlled experiment, replacing the randomness in the OCaml PBT library with an optimized version. Both interventions exactly preserve the semantics of generators, enabling precise, pointwise comparisons. Together, these improvements find bugs up to 13X faster.

Monads can be used to simulate a programming language feature in a language lacking it. For example, the ‘Maybe’ or ‘option’ monad can simulate exceptions. Monads can also be used to recover axioms lacking in an axiomatic system. For example, it is well known that in a constructive type theory, double negation is a monad within which one can use the law of the excluded middle.

Extending prior work, we define a monad to recover another major feature missing from constructive type theory: a convenient representation of nonconstructive functions. Much of traditional mathematics makes use of noncomputable functions, but most dependent type theories don’t have a way to directly represent them. To solve this problem, our monad gives access to a definite description principle, allowing one to select a value by its unique description. By combining this monad with double negation, we are able to simulate nonconstructive features in a constructive type theory.

Using these monads, we formalize the classical real numbers, define maps out of a natural definition of quotient types as equivalence classes, and define functions by general recursion. Our monad can be defined in any dependent type theory with extensionality principles, and all of our results are formalized in the Rocq prover.

Pattern matching appeals to functional programmers for its expressiveness and good cost model, but it expresses certain computations quite verbosely. Verbosity can be reduced by using extended forms of pattern matching, but extensions are not standardized, and in a large-scale programming language, making certain extensions cooperate, like or-patterns and pattern guards, is a significant implementation challenge.

Alternatively, as has been shown in the Verse programming language, computations can be expressed succinctly by using equations. But computations expressed using equations have have time and space costs that can be hard to predict. As a potential sweet spot, we propose a new calculus, V-, which limits equations in a way that makes time and space costs easy to predict.

In comparative examples, V- expresses computations as succinctly as pattern matching with popular extensions (side conditions, or-patterns, and pattern guards). And just like a case expression with patterns, a set of V- equations can be compiled to an efficient decision tree. We support our claim about V-'s cost model by providing formal rules and a Standard ML implementation for a V- match compiler. We prove that our compiled decision-making code runs in time at most linear in the size of the equations, and we evaluate our implementation with micro-benchmarks.

Iris is a popular framework for mechanizing program logics which has seen a wide range of applications such as distributed protocols, compilers, and security. The canonical implementation of Iris is written inside the Rocq prover, however, there are ongoing efforts to re-imagine Iris inside of proof assistants that may be better suited to different verification tasks. Iris-Lean is one such project: we envision an implementation of Iris with access to Lean's suite of sophisticated mathematical models and metaprogramming tools.

In this talk I will discuss the past, present, and future of the Iris-Lean project. I will discuss the lessons we have learned through the porting effort so far, the current state of Iris-Lean (including a recent development building off of Iris-Lean in industry) and I will illustrate the paths forward for this project by showing some mathematical constructions unique to Iris-Lean.

I will talk about our ongoing effort to extract verified programs from the Rocq Prover into production-grade C++. While existing compilers and extractors from Rocq target high-level functional languages (OCaml, Haskell) or lower-level imperative ones (C, Rust), none were well-suited for Bloomberg’s requirements.

We introduce Crane, a new extraction method to generate idiomatic, functional, memory- and thread-safe C++ code aligned with Bloomberg’s coding practices. Our approach uses modern C++ features to represent Rocq’s functional constructs in a way that preserves readability and maintainability. Our tool can work with mappings of Rocq data types to C++ standard library types, or to Bloomberg’s core library types to facilitate integration with existing C++ code. Additionally, we provide concurrency primitives in Rocq which compile into software transactional memory (STM) constructs in C++, enabling safe concurrent execution.

My talk will sketch out the design, implementation challenges, and early lessons learned in our quest to integrate verified functional programs into complex concurrent C++ systems. This project is joint work with Joomy Korkut.

Levy’s call-by-push-value (CBPV) is a language that subsumes both call-by-name and call-by-value lambda calculi by syntactically distinguishing values from computations and explicitly specifying execution order. This low-level handling of computation suspension and resumption makes CBPV suitable as a compiler intermediate representation (IR), while its substitution evaluation semantics affords compositional reasoning about programs.

In particular, beta-eta -equivalences in CBPV have been used to justify compiler optimizations in low-level IRs. However, these equivalences do not validate commuting conversions, which are key transformations in compiler passes such as A-normalization. Such transformations syntactically rearrange computations without affecting evaluation order, and can reveal new opportunities for inlining.

In this work, we identify the commuting conversions of CBPV, define a commuting conversion normal form (CCNF) for CBPV, present a single-pass transformation into CCNF based on A-normalization, and prove that well-typed, translated programs evaluate to the same result. To avoid the usual code duplication issues that also arise with ANF, we adapt the explicit join point constructs by Maurer et al. [2017].

We extend the scope of context-free-language (CFL) reachability to a new class of infinite-state systems. Parikh’s Theorem is a useful tool for solving CFL-reachability problems for transition systems that consist of commuting transition relations. It implies that the image of a context-free language under a homomorphism into a commutative monoid is semi-linear, and that there is a linear-time algorithm for constructing a Presburger arithmetic formula that represents it. However, for many transition systems of interest, transitions do not commute.

In this paper, we introduce almost-commuting transition systems, which pair finite-state control with commutative components, but which are in general not commutative. We extend Parikh’s theorem to show that the image of a context-free language under a homomorphism into an almost-commuting monoid is semi-linear and that there is a polynomial-time algorithm for constructing a Presburger arithmetic formula that represents it. This result yields a general framework for solving CFL-reachability problems over almost-commuting transition systems. We describe several examples of systems within this class. Finally, we examine closure properties of almost-commuting monoids that can be used to modularly compose almost-commuting transition systems while remaining in the class.

Optimizing quantum circuits is critical: the number of quantum operations needs to be minimized for a successful evaluation of a circuit on a quantum processor. Production frameworks rely on heuristics or destructive algorithms to decide if rewrite rules should be applied and in which order.

However, we observe that existing production toolchains typically rely on heuristics or destructive passes to decide which rewrite to apply and when to apply it. These sequential strategies are order-sensitive and, in practice, traverse only a tiny slice of the exponentially large space of equivalent circuits. We present a novel technique for quantum circuit optimization that employs equality saturation to apply all possible substitutions at once. Our extensive evaluation demonstrates the ability of equality saturation to strongly outperform existing optimizers on a wide range of benchmarks.

Random testing is an effective method for finding bugs that cause compilers to crash or miscompile code. An unexplored area in random testing compiler optimization is testing recursion optimizations, including (mutual) recursion elimination. Such testing commonly requires input programs to be terminating. However, existing work on (1) testing loop optimizations and (2) recursive program synthesis does not adapt well to exploring the program space of recursive optimizations while ensuring termination.

My work adapts one method of termination checking, sized types, for program generation of recursive programs. This talk will explain sized typing by comparison to another common termination checking method used in Rocq (syntactic guardedness) and discuss the challenges of implementing and evaluating a program generator for recursive optimizations.

With separate compilation and foreign language interfaces, two programs interact at program boundaries through imports and exports. When analyzing a program in isolation, a sound analysis must account for all possible imported values and downstream program behaviors depending on them. For example, abstract interpretations typically introduce 'unknown' values; imports are unknown, and applying an unknown function produces another unknown value. Argument values provided to unknown functions *escape*. Unknown values precisely represent the values coming from the *external* context, as well as the internal values that have escaped.

But to precisely characterize the external context, we need a multi-language semantics that combines the two language semantics (which may be the same language for separate compilation) with appropriate boundary forms. The multi-language semantics enables us to distinguish values emerging from the different program contexts, and the boundary forms allow us to track values crossing the program boundary.

Oftentimes, abstract interpretations do more than just run the program; they collect additional information about the program trace while running. For example, whether two values are always the same (alias analysis), which calls can apply which functions (control flow analysis), and whether a contract is always satisfied (gradual typing). Soundness of the analysis is proven against the concrete collecting semantics, which also collects information about the program trace: the events that the analysis observes must be a superset of the events the concrete semantics observes. The multi-language semantics naturally allows us to partition the observable events into "external," "internal," and "boundary," which allows the analysis to be proven sound. In this talk, we will present this technique in detail and describe how we are using it to mechanize program analyses for flow-directed transformations in CertiCoq.