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||18|
|Publication status||Published - 2007|
|Event||8th Symposium on Trends in Functional Programming 2007 - New York City, United States|
Duration: 2 Apr 2007 → 4 Apr 2007
|Conference||8th Symposium on Trends in Functional Programming 2007|
|Abbreviated title||TFP 2007|
|City||New York City|
|Period||2/04/07 → 4/04/07|
Brady, E., McKinna, J., & Hammond, K. (2007). Constructing Correct Circuits: Verification of Functional Aspects of Hardware Specifications with Dependent Types. 159-176. Paper presented at 8th Symposium on Trends in Functional Programming 2007, New York City, United States.