|
Hongwei Xi
Facilitating program verification with dependent
types
In Proceedings of the International Conference on Software
Engineering and Formal Methods, pages 72-81, Brisbane, Australia, September
2003
The use of types in capturing program invariants is overwhelming in
practical programming. The type systems in languages such as ML and Java
scale convincingly to realistic programs but they are of relatively limited
expressive power. In this paper, we show that the use of a restricted form
of dependent types can enable us to capture many more program invariants
such as memory safety while retaining practical type-checking. The
programmer can encode program invariants with type annotations and then
verify these invariants through static type-checking. Also the type
annotations can serve as informative program documentation, which are
mechanically verified and can thus be fully trusted. We argue with
realistic examples that this restricted form of dependent types can
significantly facilitate program verification as well as program
documentation.
[ bib |
.ps |
.pdf ]
Back
This file has been generated by
bibtex2html 1.61
Copyright notice: The documents contained
in these pages are included by the contributing authors as a means to
ensure timely dissemination of scholarly and technical work on a
non-commercial basis. Copyright and all rights therein are maintained
by the authors or by other copyright holders, notwithstanding that
they have offered their works here electronically. It is understood that all persons copying this information will
adhere to the terms and constraints invoked by each author's
copyright. These works
may not be reposted without the explicit permission of the copyright
holder.
If you experience problems downloading any of the files above,
it is most likely because your browser does not handle compressed
files correctly.
In particular, Netscape might save the file in the compressed
gz-format with extension .ps or
.pdf (indicating postscript or PDF, resp.). You can work around this by saving the file,
renaming it to .ps.gz or .pdf.gz, and then
uncrompress it.
|
