The Chalmers FP wiki is part of the CSE dept. wiki. |
FP /
Strongly Typed Libraries for Programs and ProofsWork page for a project submitted to VR 2013 (on 2013-04-11) as a continuation of a project with the same name funded by VR with 2.4 M SEK (2011-2013). Main applicant: Patrik Jansson, co-applicant Jean-Philippe Bernardy. AbstractOur 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:
Links:
Admin details for the 2011-2013 project instance:
|