Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
424047 | Electronic Notes in Theoretical Computer Science | 2007 | 19 Pages |
Abstract
Recent developments in the area of expressive types have the prospect to supply the ordinary programmer with a programming language rich enough to verify complex program properties. Program verification is made possible via tractable type checking. We explore this possibility by considering two specific examples; verifying sortedness and resource usage verification. We show that advanced type error diagnosis methods become essential to assist the user in case of type checking failure. Our results point out new research directions for the development of programming environments in which users can write and verify their programs.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics