• View
• Edit
• History
• Print

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:

Full application

A follow-up project: Libraries You Can Trust.

Main applicant: Patrik Jansson, co-applicant Jean-Philippe Bernardy.

Abstract

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:

• "Parallel Parsing and Matrix Algebra"
  • ValiantAgda
  • including MSc thesis work on the Algebra of Parallel Programming in Agda
  • A paper on "Efficient Divide-and-Conquer Parsing of Practical Context-Free Languages" was presented at ICFP 2013
  • Phil Wadler praising the ICFP session were the paper was presented
• Functional Enumeration of Algebraic Types
• Testing Type Class Laws, published in the ACM SIGPLAN Haskell symposium 2012
• Testing versus proving in climate impact research
• Dependently-typed programming in scientific computing --- examples from economic modelling

Links:

• Algebra of Programming in Agda: original project page, on the Agda wiki
• Related events (some potential venues for research results within this project):
  • Mathematically Structured Functional Programming
  • Mathematics of Programme Construction
  • International Conference on Functional Programming
  • Workshop on Generic Programming
  • Haskell Symposium
  • Programming Languages meets Program Verification (PLPV)
  • Typed Lambda Calculi and Applications

Main objectives

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:

• KST: 3725
• PNr: 3720398
• PName: VR Starkt typade bibliotek PJ

In 2014 the project pays for Bernardy (50%), Ionescu (40%) and Jansson (15%).