Reconstruction of Incomplete Polymorphic Programs
The ability to reconstruct the dependencies of incomplete programs to form complete and well-typed ones provides several benefits, including allowing static analysis tools to analyse incomplete programs where their surrounding dependencies are unavailable, and supporting stub generation and testing tools to work on snippets. However, earlier efforts to do so are unable to work with incomplete programs containing parametrically polymorphic types.
In this paper, we present a technique that receives an incomplete Java program that may contain parametrically polymorphic types, and reconstructs its surrounding dependencies to form a complete and well-typed program. We then present empirical results from our prototype implementation of this algorithm, JavaCIP, which outperforms prior works in this area.
Partial Evaluation of Rank-2 Polymorphic Functions
Rank-2 polymorphic functions are used in a variety of programs and libraries. However, such functions may be difficult to optimize by general-purpose optimizers, especially if they are recursive. General-purpose optimizers thus avoid optimizing these functions, leaving many missed opportunities for further program optimization.
Thus, we propose a new optimization pass, PEPSA, that performs a partial evaluation of partially static applications of rank-2 polymorphic functions to reveal further avenues of optimization. Preliminary benchmarks show that PEPSA, in conjunction with other standard optimization passes, achieves a 3 to 75 times speedup on generic programming systems.
A Fixed-Point-Oriented Programming Language with User-Specified Optimization Strategies
There are a wide range of problems that are easily solved using a fixed-point algorithm instead of the more common programming strategies of loops and recursions. Examples of these include parsing, static analysis, type-checking, graph algorithms, and automata manipulation. Existing language paradigms, such as the imperative and functional paradigms, support loops and recursions well but support fixed-point algorithms rather poorly.
In this project, we will develop a programming language providing such support. In addition, by specifying problems at the abstraction-level of fixed points, our language can include mechanisms for the programmer to influence and optimize the solution strategy used by the implementation without the programmer having to modify the problem specification. This will allow users of the language to rapidly prototype and test a problem specification and to later specify optimizations while making only minimal changes to existing code, a task particularly difficult for fixed-point problems in existing languages.
Optimization Tactics (Functional Pearl)
Program optimizations are frequently done by the compiler. These optimizations are general purpose, so as to extract the best performance out of as many programs as possible. However, general-purpose optimizations may not be well-suited for some specific programs.
Thus, we present optimization tactics, a new construct that allows users to define their own optimization strategies and to apply optimizations at specific program points. The library for supporting optimization tactics is implemented with Lean 4's powerful metaprogramming and theorem proving facilities, which allows users to:
- Easily define provably correctness-preserving optimization tactics as expression-to-expression transformation functions.
- Apply an optimization wherever a program term occurs
- Leverage Lean 4's interactive view to observe every step of the optimization
- Separate algorithm from optimization.
Optimization tactics thus allows library authors to define domain-specific optimizations, and for library users to incorporate, extend and adapt optimization tactics to their specific use-case. We also propose that the interactivity of optimization tactics in Lean 4 allows researchers to explore new optimization techniques that can be applied to other functional programming languages.
Improving the Bounds on Random-Access Lists
Accessing an arbitrary element of a traditional singly linked list or cons list requires traversing up to a linear number of pointers. A random-access list is a data structure that behaves like a cons list except that accessing an arbitrary element requires traversing only a logarithmic number of pointers. Specifically, in a list of length n, an arbitrary element can be accessed by traversing at most 3 * ceil(log(n)) - 5 pointers.
In this paper, we present a simple variation on Myers lists that improves this bound and requires traversing at most 2 * ceil(log(n + 1)) - 1 pointers. We then present a more complicated variation that improves this bound to (1 + 1 / s) * ceil(log(n)) + s + 9 for any s >= 2. This shows that it is possible to get asymptotically close to the information-theoretically optimal bound of ceil(log(n + 1)) - 1.
Motivating Mathematics Study in Prospective Computer Scientists with Interactive Theorem Provers
The Curry-Howard correspondence shows that terms, types, programs and program evaluation correspond to witnesses, propositions, proofs and proof normalization in (intuitionistic) logic. This has spawned a large body of work in the literature known as proof assistants or interactive theorem provers that exploit this correspondence via a programming language with a type system that supports proof checking.
On the other hand, the need to study mathematics may not be immediately apparent to budding software engineers, particularly those aiming to enter industry post-study. Our aim is motivate students to study mathematics by showing that the art of writing programs is the same as the art of writing a proof. We do so by writing both proofs and programs in Lean 4.