Problem: Library summarization is an effective way to accelerate the analysis of client code. However, information about the client is unknown at the 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 $x \ge \frac{1}{2}$ is exactly $p$.

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 on this direction.

Follow-up: There is a connection between derivatives of the probability-generating function of a random variable $X$ and the moments of $X$. 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-value-logic for shape analysis, $k$-CFA, $m$-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, $(ff)^*$ indicates calling a function $f$ for an even number of times, $f(ff)^*$ for 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 $A \to B$, then a standard resolution of nondeterminism gives us $A \to \wp(B)$, but nondeterminism-first suggests $\wp(A \to B)$. 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 troubles.

Problem: Nondeterminism is often referred to as the basis of abstraction and refinement in the setting of stepwise developement¹⁰. However, such a pattern has not been popular in modern programming languages. What is the main obstable 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: Consider 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 a 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, debugger, mixed paradigm, etc.

Problem: Array programming (or tensor programming) is pervasive nowadays because of machine learning. Many machine-learning frameworks lack the ability to statically check 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 separtion 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 refinemend 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 back 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 form 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 there are—to do this?

Proposal: So the system is basically a comination of liquid-style language design and an 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 of 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 $\frac{p}{1-p}$, where $p$ 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 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 carray 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 on incorrectness logic²¹ and coverage typing²² show the power of suhc 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: 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 feedbacks 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 (emm, 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 (emm, not really).

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

Problem: One central function of low-code programming platforms is to automatically generate 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 as a functor that takes a database-table module as its input and outputs an inference 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 synthesize the code of the customization functor.

Follow-up: Low-code programming involves many UI-related customization. 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^{26 27}. We also had published a related PLDI paper. Those approaches can be categorized into two sorts: one develops a complex type system of 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, an ICC research usually provides a non-standard programming language, in which every legal program is guaranteed to have certain complexity. Can we generalize the template-based approach to ICC-based approach?

Proposal: A starting point could be non-size-increasing computaion²⁸.

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 $O(n \log n)$ 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: Coq 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, so that improves readability. Is it possible to use a backward pattern in Coq proofs? If not, would it be possible to have a backward-proof DSL that can be translated to Coq?

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 a concrete implementation in a system programming language (e.g., C) refine 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?