Strongly Typed Libraries for Programs and Proofs
Work page for a project funded by VR with 2.4 M SEK (2011-2014).
A continuation proposal which was submitted to VR 2013 was rejected but describes the ongoing work well:
Main applicant: Patrik Jansson, co-applicant Jean-Philippe Bernardy.
Our long-term goal is to create systems (theories, programming languages, libraries and tools) which make it easy to develop reusable software components with matching specifications. In this research project, the main focus is on libraries.
Strongly-typed programming languages allow to express functional specifications as types. Checking the types of a program then means checking it against its specification.
Within such powerful programming languages, libraries are not only building blocks of programs, but also of proofs. We believe that such libraries will eventually become the main means of developing programs, and because they come with strong types, the programs built using the library will come with strong properties that will make the whole easy to prove correct.
The production of such libraries will also inform the design of future strongly-typed programming languages. In the recent years, strongly-typed programming languages have started to become usable, but remain confined to a small niche. Our libraries will make them a viable solution for a broader range of applications, bringing higher guarantees of correctness to a wider user base.
To check the applicability of our libraries, we will apply them to classical problems of computer programming, such as certain divide-and-conquer algorithms or optimisation problems, as well as to the construction of tools supporting dependently-typed programming themselves.
Case-studies, papers and libraries:
Our long term goal is to create systems (theories, programming languages, libraries and tools) which make it easy to develop software components and matching specifications. In this research project, we aim to leverage the power of languages with strong types to create libraries of components which can express functional specifications in a natural way, and, simultaneously, implementations which satisfy those specifications. The ideal we aim for is not merely correct programs, nor even proven correct programs; we want proof done against a specification that is naturally expressed for a domain expert.
Concretely, we aim to identify common patterns in the specification of programs, and capture those in libraries. At the same time, the patterns of implementations of these specifications will also be captured in the library, such that the development of software will go hand-in-hand with proofs of its functional correctness. As case-studies we will work in three areas: simple divide-and-conquer algorithms, optimisation problems (inspired by the Algebra of Programming), and testing.
Admin details for the 2011-2014 project instance:
In 2014 the project pays for Bernardy (50%), Ionescu (40%) and Jansson (15%).