Problem: Library summarization is an effective way to accelerate the analysis of client code. However, information about the client is unknown at the time of library summarization, preventing complete summarization of the library. A state-of-the-art approach is Conditional Dyck-CFL Reachability Analysis (ConCRA), which targets graph-reachability-like static analyses and uses hypothetical summaries.

Proposal: Lal et al.⁷ proposed a tensor-product principle: Tensor products with an appropriate detensor operation allow computations to be rearranged in certain ways; for example, they can be used to delay a multiplication in a chain of multiplications. This principle may allow us to generalize, in the summarization framework, Dyck-CFL-reachability-based analyses to algebraic semiring-based analysis.

Follow-up: The library summarization problem can be generalized to partially solving an equation system for a static analysis. Any thoughts on partial evaluation?

Problem: Esparza et al.⁵ generalized Newton’s method to a method for finding fixed points of systems of equations over semirings, leading to a new algorithm to solve interprocedural dataflow analysis. Reps et al.⁸ developed NPA-TP, which extended Esparza’s framework with an improved algorithm for solving linear-context-free-language (LCFL) sub-problems. However, NPA-TP assumes the underlying abstract domain admits an idempotent semiring; such an assumption rules out interesting analysis domains, especially for numerical properties, e.g., the reaching probability.

Proposal: Esparza’s original framework does support non-idempotent semirings, so it would be a good starting point. The NPA-TP framework features tensor products to solve LCFL sub-problems, and from the perspective of algebras, the principle of tensor products does not require idempotence.

Follow-up: Some recent work shows that quantum computation also needs non-idempotent semirings. Can the idea of NPA-TP be generalized to analyze quantum programs?

Problem: In many programs, the manipulation of probability is very complicated and even manual analysis of their correctness is difficult. Consider the problem below:

x = p;
while (prob(0.5)) {
  x = 2 * x;
  if (x >= 1) {
    x = x - 1;
  }
}

We want to verify that at the end of the loop, the probability of the event is exactly .

Proposal: Probability-generating functions provide a succinct way to describe probability distributions of discrete random variables. We might try to derive the probability-generating function of a probabilistic program to reason about the resulting distribution of the program. A recent paper⁹ is in this direction.

Follow-up: There is a connection between derivatives of the probability-generating function of a random variable and the moments of . Can we use the fact to perform moment analysis?

Problem: Static analysis of heap-manipulation programs often involves heap sensitivity. In the simplest case, all memory allocations with the same program location are treated as a single allocation (thus in a context-insensitive way). Advanced techniques include three-valued logic for shape analysis, -CFA, -CFA¹⁰, etc. However, they seem insufficient when we want to analyze recursive programs. (Imagine that in functional programming, iterating over a list is usually implemented as a recursive function.)

Proposal: We can treat the set of all call-strings as a language, then different strategies for handling sensitivity are essentially different ways of defining equivalence classes on the language. A presumably good proposal is to use regular patterns to classify equivalence classes. For example, indicates calling a function an even number of times, an odd number.

Follow-up: In fact, this approach should generalize to all sensitivities that use call strings. Is it meaningful to develop a general framework with regular-pattern-sensitivity?

Problem: Nondeterminism-first means that we resolve nondeterminism prior to program inputs when defining denotational semantics. For example, suppose that a deterministic function has the signature , then a standard resolution of nondeterminism gives us , but nondeterminism-first suggests . Nondeterminism-first can be useful for e.g., compile-time nondeterminism. A recent study proposed a denotational semantics for probabilistic programs that combines discrete distributions (on a countable state space) and nondeterminism-first. However, it remains open if the semantics can be extended to support continuous distributions.

Proposal: In fact, I do not have any ideas yet.

Follow-up: What about a computational theory for such a combination?

Problem: The common treatment of a probabilistic flip in the semantics is to “split” the current program configuration into two, one for the “world” where the flip shows heads and the other for tails. When we need to deal with multiple concurrent processes, such a treatment means a local flip in a process results in duplicating all other processes. Such a non-local (thus non-compositional) behavior has been shown to be problematic for proving soundness of formal methods (e.g., type systems, which are usually compositional).

Proposal: The result of a probabilistic flip should remain as local as possible. We have recently developed an operational semantics with the desirable locality, but I feel that a more algebraic representation is better. For example, we might want to rearrange the operational semantics to reduction rules and congruence rules. Furthermore, we should prove an equivalence result to the ordinary probabilistic semantics (e.g., Markov chains).

Follow-up: I can always imagine that adding nondeterminism causes a lot of trouble.

Problem: Nondeterminism is often referred to as the basis of abstraction and refinement in the setting of stepwise development¹¹. However, such a pattern has not been popular in modern programming languages. What is the main obstacle for developing such a framework? Also, people have developed many kinds of semantics for nondeterminism. Which semantics should be the most suitable one for refinement-based programming and reasoning?

Proposal: I guess this has something to do with relational Hoare Logics¹². At least they provide a way to use nondeterminism in a formal framework of proving program properties.

Follow-up: How to devise a language design for it?

Problem: Suppose we have a typed programming language that is suitable for developing embedded Domain Specific Languages (eDSLs). Every eDSL can directly use the base type system from the host language, but it can also have its own advanced domain-specific type system. Languages such as MetaOCaml have already supported such a mechanism, but the interaction between the host language and the eDSL, or maybe even between different eDSLs, is not very convenient yet. It would be nice to have a simple and safe interaction scheme among eDSLs on the same host language.

Proposal: In fact, I do not have any ideas yet.

Follow-up: What else should we have for such a flexible eDSL framework? For example, we might want to consider multi-stage compilation, debuggers, mixed paradigms, etc.

Problem: Array programming (or tensor programming) is pervasive nowadays because of machine learning. Many machine-learning frameworks lack the ability to statically check that tensor shapes are always consistent during program execution. Approaches based on dependent/refinement/indexed types all seem too heavy to become practical.

Proposal: In many (really?) cases, when the input of an array program is fixed, the shapes of all intermediate arrays are also fixed. So we can perform a static shape check after the input is given, but before we execute the program, by propagating the concrete shape information from the given input.

Follow-up: Is it possible to automatically learn the shape-related effects of library functions (e.g., broadcast_tensor)?

Problem: Recently, people have developed verification systems, e.g., CN¹³ and RefinedC¹⁴, which integrate refinement types and separation logic to reason about low-level programs. In those systems, refinements seem to still encode purely functional properties (really?). How about enabling type refinements to be separation-logic propositions? To that end, such refined types are not structural any more and we need to work with substructural refinement types. Does the integration make sense?

Proposal: It seems that we can start from linear refinement types.

Follow-up: Linear typing and separation logic share a lot of similarities. Are both rooted in linear logic? If not, what is the fundamental difference?

Problem: Dijkstra monads¹⁵ were originally proposed to automate the verification-condition-generation (VCG) routine for analyzing effectful higher-order programs. They later formed the basis of F*, a proof-oriented programming language¹⁶. One feature of F* is that it supports proof-irrelevant refinement types. Liquid types¹⁷ provide another method of balancing between automatic type inference and dependent typing. One main idea of liquid types is to separately design a language for specification. Can we combine Dijkstra monads and liquid types? What are the benefits—if any—of doing this?

Proposal: So the system is basically a combination of liquid-style language design and F*-style type inference.

Follow-up: Dijkstra monads support multi-monadic effects in a systematic way. This means we might have a method to extend our ICFP paper to include the value interpretation as in the language itself.

Problem: Most current resource-analysis techniques derive linear, polynomial, or exponential bounds. However, when analyzing probabilistic programs, we often encounter bounds that involve fractions. For example, the simple loop while (prob(p)) tick(1); has an expected cost of , where is a program variable that denotes a non-trivial probability.

Proposal: In many cases, a fraction bound can be expressed as a polynomial over another polynomial. So it should be possible to extend current template-based resource-analysis techniques (e.g., AARA) that derive polynomial bounds, by using a template for the denominator to reduce fraction-bound inference to polynomial-bound inference.

Follow-up: A random thought: how can we apply such a resource-analysis technique to Bayesian inference (like a recent paper by Beutner et al.¹⁸)?

Problem: Our ICFP paper presents an extension of AARA that infers upper bounds on the expected cost of probabilistic functional programs with monotone resources (such as time). In general, combining probability and non-monotone resources (such as memory) is unreasonably complex¹⁹. Applying optional stopping theorems, people have successfully developed techniques for analyzing arithmetic programs. It would be interesting to see if the whole methodology applies to functional programming, where we have inductive data structures (that can hold potential) instead of numbers.

Proposal: One version of optional stopping theorems states that the expected change in one evaluation step should be “bounded.” This should intuitively hold for functional programming (I mean, in most cases) because one step should change the size of a data structure by at most one (consider the case of cons). By constructing a suitable Markov chain, we might be able to reason about probabilistic functional programs with non-monotone resources.

Follow-up: Optional stopping theorems always talk about “expected change” and “expected termination time.” Why them?!

Problem: Apply the Newtonian Program Analysis (NPA) framework⁵ and its extension⁸ to carry out resource analysis. Existing work has shown the possibility to perform recurrence-based analysis²⁰. How about other kinds of resource analysis, like AARA?

Proposal: Because amortized analysis is naturally two-vocabulary, it seems possible to recast AARA as a two-vocabulary abstract domain. The gap is that AARA is constraint-based, which differs from the general NPA framework.

Follow-up: NPA basically provides a framework for analyzing non-linear-recursive programs by iteratively analyzing linear-recursive programs. Can we combine this idea to iteratively use AARA to solve linear recursion?

Problem: Most work on resource analysis focuses on worst-case upper bounds, but in practice people also want to know worst-case lower bounds, i.e., whether there exists a realizable execution path leading to the bound. This could usually be done by testing techniques for worst-case analysis, e.g., fuzzing²¹. Recent advances in incorrectness logic²² and coverage typing²³ show the power of such realizability analysis. We want to follow those lines of work to build type systems or program logics to reason about worst-case lower bounds.

Proposal: From the perspective of incorrectness logic, one can extend separation logic with time credits. From the perspective of coverage typing, one can extend liquid resource types.

Follow-up: Is it possible to integrate such deductive analysis with fuzzing-based worst-case analysis?

Problem: AARA is a mathematically elegant approach, but it is still far from analyzing real-world programs to identify performance bottlenecks. With the evolution of LLMs, it seems promising to apply them in real-world program analysis. An interesting approach is HoarePrompt²⁴, which drives the LLM to perform Hoare-style strongest postcondition reasoning to detect bugs. I wonder if this approach could generalize to resource analysis, in the sense that the LLM uses its reasoning capability to analyze the potential functions in natural language.

Proposal: Maybe go from Hoare logic to quantitative Hoare logic²⁵? Or for performance bottleneck analysis, incorrectness-logic-style approaches could be better, e.g., our ESOP paper.

Follow-up: There is some possibility to develop a finer-grained integration. Hybrid Resource Analysis^{26 27} presents a theoretical framework to integrate different resource analyses in AARA, so, for example, it is interesting to see if one can use an LLM to analyze unsafe Rust code, derive the boundary information, and then integrate it back into an AARA analysis to analyze safe Rust code.

Problem: Daniel Ritchie suggested generative probabilistic programming for procedural modeling and design (the use of random programs to generate visual content with respect to aesthetic or functional constraints). Such an approach has been rediscovered in several individual developments, such as Scenic²⁸ and Picture²⁹. So instead of separate developments, we want to develop a framework to ease such domain-specific procedural design.

Proposal: This has something to do with the eDSL framework.

Follow-up: It might be interesting to see how such static procedural design evolves to dynamic procedural design (e.g., synthesis of an environment). Another direction is interactive refinement (e.g., incorporating feedback from users) of the generated designs.

Problem: A recent paper by Cusumano-Towner et al.³⁰ studies how to ease the burden of implementing involutive MCMC by combining probabilistic programming and differentiable programming. It still remains a challenge (um, you have to double-check) to statically verify the correctness of a concrete implementation in their framework.

Proposal: I would try to combine type systems for sound programmable inference and sound differentiable programming.

Follow-up: I am thinking of The Next XXX MCMC Algorithms.

Problem: Quantum physics uses a form of complex probability. People have been thinking of it as a serious probability theory (see this and this). There are even quantum analogs of Bayesian inference (one and the other). Does it make sense to incorporate some of those ideas in current probabilistic programming systems?

Proposal: I still have to learn quantum physics (um, not really).

Follow-up: Some people are trying to add quantum features to standard Bayesian models (check out this).

Problem: At the time of writing this page, system-one models (like Jev and Laya) are under active discussion. These models have the instruction understanding capability of LLMs, but they are designed to make probabilistic decisions from a given answer space, i.e., the support of a probability distribution. Such models may be more suitable to integrate with probabilistic programming than generative LLMs (e.g., as done in LLaMPPL³¹), especially in the programmable inference setting, where the system-one models could either provide model or guide samples.

Proposal: Currently, system-one models support discrete distributions with a finite support. So, they might be suitable for Bayesian inference with discrete latent variables.

Follow-up: How to extend from discrete distributions to continuous distributions?

Problem: One central function of low-code programming platforms is to automatically generate a usable interface for manipulating database tables. In an application, the developers might want to customize a specific way to organize the interface, and they want to reuse the customization across the application.

Proposal: The customization can be thought of as a functor that takes a database-table module as its input and outputs an interface module for that table. For low-code programming, it would be useful to have a mechanism where the developers customize a table interactively and the platform automatically synthesizes the code of the customization functor.

Follow-up: Low-code programming involves many UI-related customizations. Is there a more general principle? For example, it might be interesting to investigate Natural Programming.

Problem: Recently, resource-guided synthesis and algorithm synthesis have received considerable attention^{32 33}. We have also published a related PLDI paper. Those approaches can be categorized into two sorts: one develops a complex type system or program logic to enforce resource guarantees; the other proposes algorithmic templates that ensure resource guarantees. The latter is somewhat related to Implicit Computational Complexity (ICC), which characterizes algorithms by constraints on the way in which they are constructed. In other words, ICC research usually provides a non-standard programming language, in which every legal program is guaranteed to have a certain complexity. Can we generalize the template-based approach to an ICC-based approach?

Proposal: A starting point could be non-size-increasing computation³⁴.

Follow-up: ICC seems to be not so fine-grained, e.g., usually researchers focus on whether the complexity is polynomial or not. How to make them finer-grained? For example, would it be possible to develop an ICC class for algorithms?

Problem: Verified Software Toolchain (VST) is a set of verified tools that formally verify the functional correctness of C programs using Hoare logic and separation logic. I wonder if it is also convenient to verify resource-usage properties of C programs, like their time or memory complexities.

Proposal: It has been shown that separation logic naturally supports resource verification based on time credits³⁵. So conceptually it should be possible to have that in VST.

Follow-up: Can we develop some general reasoning libraries for resource verification?

Problem: Rocq proofs are organized in a forward, tactic-based manner, which is not very readable. In contrast, Isabelle (and some other theorem provers) provides a backward mode, where the intermediate goals are stated explicitly, which improves readability. Is it possible to use a backward pattern in Rocq proofs? If not, would it be possible to have a backward-proof DSL that can be translated to Rocq?

Proposal: Isabelle’s Isar might be a good starting point.

Follow-up: What is the best proof interface for system programmers?

Problem: Many verification projects (e.g., seL4) start from a high-level specification implemented in a functional language (e.g., Haskell) and then prove that a concrete implementation in a system programming language (e.g., C) refines the specification. From the perspective of software engineering, this suggests another way of system programming: first implement a functional specification and then (iteratively) refine it to build a concrete low-level implementation.

Proposal: Build a language where the high-level and low-level languages can interoperate seamlessly, e.g., Haskell and C. Existing solutions are somehow quite complex, in the sense that they want to interoperate with a realistic C compiler directly. However, it would be nice enough for the development process if the C part is just supported partially, but with better support, e.g., to be equipped with an interpreter.

Follow-up: What is the best practice for multi-language (i.e., multilingual) software engineering?

Problem: I had an LMPL paper about applying algebraic effects to engineer LLM-integrated scripts. (There is a parallel LMPL paper in the same direction: Programming Large Language Models with Algebraic Effect Handlers and the Selection Monad.) Since then, LLM engineering practice has shifted from workflows to agents, and to harnesses. Some people also call harnesses “AgentOS”, operating systems designed around LLMs. The idea is rather simple: algebraic effects provide a clean way to separate semantics from syntax, achieving good abstraction for building effectful software; on the other hand, LLM-integrated scripts need to handle many different kinds of effects, e.g., remote calls, bash executions, async schedules, multi-agent coordination, branch selections, and so on. DeepSeek Harness also employs an effect-and-coeffect plugin system, aiming at modularity and extensibility. Currently, the popular languages for implementing harnesses are Python and TypeScript, which lack good support for algebraic effects, from the perspective of either the runtime or the type system.

Proposal: Design a new programming language with the following features: (i) multi-shot effect handlers with a high-performance runtime (e.g., as a sandbox), (ii) support for hot code updates (like Erlang), so as to support dynamic plugin management, (iii) a type system to track resources, capabilities, and effects.

Follow-up: It is also interesting to see if choreographic programming can be applied here, in the sense of multi-agent systems or even distributed-agent systems.

Problem: In the current LLM workflows, tool calls are essential to grant agents powerful capabilities to do many kinds of work. Interestingly, from the perspective of LLM calls, tool calls are fully syntactic: an LLM request only carries the description and schema for each available tool. However, current agents/harnesses usually couple tools with their concrete implementations. Some frameworks may support tool customization, but the semantics is still tightly coupled.

Proposal: Suppose we have a harness that treats tools as effectful operations without semantics. Their semantics should be determined dynamically by effect handlers. So the harness should be able to write code to implement handlers, as well as push handlers onto and pop handlers off the runtime effect stack. This seems an interesting generalization of the code-action paradigm.

Follow-up: This seems quite interesting and powerful, but is it really useful?