Recent Changes - Search:
FP /

Libraries You Can Trust: high-level specifications and correct implementations via dependent types

Work page for a project application sent to VR 2015-03-31.

Full application

Main applicant: Patrik Jansson, co-applicants Jean-Philippe Bernardy and Cezar Ionescu.

Introduction

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: the Algebra of Parallel Programming (inspired by the Algebra of Programming [Bird&de Moor, 1996]), Domain-specific Modelling, and Testing.

Note that what we call "software" or "program" in this proposal is not just a sequence of instructions, written to perform a specified task with a computer [Wikipedia, Computer Program]. In our terminology a "program" is a more high-level description of what a computer should compute (perhaps closer to the meaning of "algorithm") or even, in the case of Domain-specific Modelling, a high-level description of a problem or a solution in a particular application domain (be it financial contracts, partial differential equations or formal proofs). This means that the iterative process of coming up with a "program" matching a "specification" is not limited to traditional programming, but it is also a way of exploring and understanding a domain. A resulting library of specifications can be seen as a collection of building-blocks for describing (problems in) the domain and a library of implementations can be seen as computer aided methodologies for computing with, or solving problems within, that domain.

Related projects