Typed Lambda-Calculi with Sharing and Unsharing

This project aims to develop a new approach to efficient evaluation in the lambda-calculus, based on deep-inference proof theory.

The lambda-calculus is a minimal but fully expressive, theoretical programming language. It forms the basis of functional programming languages such as Haskell, and efficiency improvements in the lambda-calculus can be applied to create compilers that produce faster programs. Such improvements can be efficient computation strategies, or changes to the syntax, or both.

The lambda-calculus is linked to proof theory by the Curry-Howard correspondence: types are logical formulas, programs are proofs, and computation is proof normalization (reduction to a well-behaved form). Conversely, for a given proof system we can ask what its computational interpretation is.

Deep inference is a modern branch of proof theory characterized by its flexibility in composing proofs. This allows it to capture logics not expressible in other proof systems, and to yield surprisingly good complexity results. Key to these results is the medial rule scheme, a core innovation of deep inference that sets it apart from related formalisms. The basis of the project is the discovery that the medial enables computation steps associated with optimal efficiency.

Sharing graphs are a graphical formalism for lambda-calculus computation using sharing and unsharing. Sharing is the multiple use of a single expression, which then needs to be evaluated only once, improving efficiency. Unsharing is a counterpart that enables the shared use of partial expressions. In theory, sharing graphs are optimally efficient for lambda-calculus. However, in a real-world setting, the control mechanism that manages duplication, the oracle, incurs too much overhead cost, and they are not used in practice.

The discovery on which the project is based is that the medial rule scheme enables computation with sharing and unsharing, as in sharing graphs, but without the need for a control mechanism other than the structure of the proof itself.

The project will develop a computational interpretation of the medial. An initial investigation led to the atomic lambda-calculus, the first typed lambda-calculus with sharing and unsharing, and the first lambda-calculus to capture full laziness, a standard notion of efficiency, as a natural strategy. The project will build on this on three levels: structure, control, and measurement.

Structure: The project will develop a theory of proof normalization in deep inference for intuitionistic logic (associated with the lambda-calculus), where the medial replaces the need for a control mechanism. Based on the experience with the atomic lambda-calculus, the hypothesis is that the proof system adapts naturally to different levels of efficiency by varying the choice of proof rules.

Control: New control mechanisms will be derived from the structure of deep inference proofs. These will be used to implement various efficient strategies with sharing and unsharing in typed lambda-calculi and abstract machines.

Measurement: The project will use normalization in deep inference to construct a range of semantic tools to measure the efficiency of these calculi and control mechanisms. Here, the availability of a single underlying proof system provides a new and unique opportunity to compare strategies on an equal footing.

On the theoretical side, the project addresses several open questions in the literature: How to measure the efficiency of lambda-calculi with sharing? What is a global type system for sharing graphs? What is the computational meaning of deep inference? On the practical side, the typed lambda-calculi and abstract machines of the project are a basis for new and efficient ways of implementing functional programming languages.

The impact of the project will be both academic and, in the longer term, economic. Academic impact areas are deep-inference proof theory and the lambda-calculus; economic impact will be through the efficient implementation of functional programming languages, benefitting industrial and individual end-users.

Academic impact: deep-inference

The Curry-Howard correspondence relates proofs to programs, creating a bridge between proof theory and functional programming. It is a cornerstone of modern proof theory, to the extent that an essential question for any proof system has become: what is its computational meaning? For deep inference, this question has remained open, and the project will provide an answer. This represents a major breakthrough in the understanding of deep-inference proof theory.

The direct impact on deep inference in particular, and proof theory in general, will extend in two dimensions. One, the results will apply to other logics, represented in deep inference, yielding new approaches to their computational interpretation. Two, the approach of the project may be interpreted or encoded in other proof systems, yielding new approaches to normalisation in a wider range of proof systems.

Academic impact: the lambda-calculus

The lambda-calculus is a main tool in theoretical computer science. Its efficient evaluation has been studied through a wide array of disparate means: strategies, explicit substitutions, labelled calculi, sharing graphs, and many more. The project will have a significant impact on this research area, by three avenues. One, the project will develop a new approach to efficient lambda-calculus evaluation, in the form of typed lambda-calculi with sharing and unsharing. Two, the project has a unified approach anchored in a single proof system (intuitionistic deep inference) flexible enough to accommodate many strategies and control mechanisms. This will provide a new, common perspective on methods for efficient evaluation, both existing ones and those developed in the project. Three, the project leverages its unified approach to provide semantic tools for the measurement and comparison of evaluation mechanisms. Taken together, these three innovations will strongly influence the way efficiency in the lambda-calculus is pursued.

Economic impact: functional programming

The ultimate aim of the project, in the medium and longer term, is to contribute to the efficient implementation of functional programming languages. With strong type systems and high abstraction, these languages emphasize safety, programmer productivity, and modularity, while scaling well to parallel architectures. These features are becoming increasingly relevant. Trends are towards larger programs and systems, requiring modular programming paradigms and parallelism, and in general towards greater dependence on information technology, placing greater emphasis on safety.

At present, efficiency is a main weakness of pure functional programming languages: their demand for computational resources such as time and memory can be high, and unpredictable. Currently, their use is focused in high-end, quality-sensitive software. Industrial users include the financial industry (for safe development on high-end parallel architectures), developers of safety-critical systems, and large tech companies (for the rapid development of reliable in-house tools).

The project will provide a novel approach, and new momentum, to a wider effort to improve the efficiency of functional programming languages, removing one of their main drawbacks. This will make functional languages viable for a larger range of programming efforts, to which their benefits of safety and productivity will accrue. This will directly benefit society by preventing damage from program failures, and by reducing both the cost and the risk of large-scale programming efforts.