Edinburgh Research Archive >
Informatics, School of >
Informatics thesis and dissertation collection >
Please use this identifier to cite or link to this item:
|Title: ||Supporting dependently typed functional programming with proof automation and testing|
|Authors: ||Wilson, Sean|
|Supervisor(s): ||Fleuriot, Jacques|
|Issue Date: ||30-Jun-2011|
|Publisher: ||The University of Edinburgh|
|Abstract: ||Dependent types can be used to capture useful properties about programs at compile time. However, developing dependently typed programs can be difficult in current
systems. Capturing interesting program properties usually requires the user to write
proofs, where constructing the latter can be both a difficult and tedious process. Additionally, finding and fixing errors in program scripts can be challenging.
This thesis concerns ways in which functional programming with dependent types
can be made easier. In particular, we focus on providing help for developing programs
that incorporate user-defined types and user-defined functions. For the purpose of supporting dependently typed programming, we have designed a framework that provides
improved proof automation and error feedback.
Proof automation is provided with the use of heuristic based tactics that automate
common patterns of proofs that arise when programming with dependent types. In
particular, we use heuristics for generalising goals and employ the rippling heuristic
for guiding inductive and non-inductive proofs. The automation we describe includes
features for caching and reusing lemmas proven during proof search and, whenever
proof search fails, the user can assist the prover by providing high-level hints.
We concentrate on providing improved feedback for the errors that occur when
there is a mismatch between the specification of a program, described with the use of
dependent types, and the behaviour of the program. We employ a QuickCheck-like
testing tool for automatically identifying these forms of errors, where the counter examples generated are used as error messages.
To demonstrate the effectiveness of our framework for supporting dependently
typed programming, we have developed a prototype based around the Coq theorem
prover. We demonstrate that the framework as a whole makes program development
easier by conducting a series of case studies. In these case studies, which involved
verifying properties of tail recursive functions, sorting functions and a binary adder, a
significant number of the proofs required were automated.|
|Sponsor(s): ||Engineering and Physical Sciences Research Council (EPSRC)|
|Keywords: ||dependent types|
|Appears in Collections:||Informatics thesis and dissertation collection|
Items in ERA are protected by copyright, with all rights reserved, unless otherwise indicated.