This paper focuses on the important, but tricky, problem of determiningprovably correct program properties automatically from program source. Wedescribe a novel approach to constructing correct low-level programs. By usingmodern, full-spectrum dependent types, we are able to give an explicit and checkablelink between the low-level program and its high-level meaning. Our approachclosely links programming and theorem proving in that a type correct program is aconstructive proof that the program meets its specification. It goes beyond typicalmodel-checking approaches, that are commonly used to check formal propertiesof low-level programs, by building proofs over abstractions of properties. In thisway, we avoid the state-space explosion problem that bedevils model-checkingsolutions. We are also able to consider properties over potentially infinite domainsand determine properties for potentially infinite programs. We illustrateour approach by implementing a carry-ripple adder for binary numbers.
|Number of pages
|Published - 2007
|8th Symposium on Trends in Functional Programming 2007 - New York City, United States
Duration: 2 Apr 2007 → 4 Apr 2007
|8th Symposium on Trends in Functional Programming 2007
|New York City
|2/04/07 → 4/04/07