Abstract
One approach to Prof. Hoare's challenge is to view the development of verified software from the perspective of interactive theorem provers. This idea is not new and many medium-scale software systems have been developed and verified in this manner. Developments based on HOL, ACL2, or PVS have already been described and advocated and our position stands on the same line: most powerful (higher-order) theorem proving systems already contain a programming language, programs can be developed and the correctness of these programs can be specified and verified, they can then be compiled into traditional executable code. In this sense, we already have a small scale example of a verification aware programming language. © IFIP International Federation for Information Processing 2008.
Cite
CITATION STYLE
Bertot, Y., & Théry, L. (2008). Dependent types, theorem proving, and applications for a verifying compiler. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4171 LNCS, pp. 173–181). https://doi.org/10.1007/978-3-540-69149-5_19
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
