Dependent types, theorem proving, and applications for a verifying compiler

2Citations
Citations of this article
8Readers
Mendeley users who have this article in their library.

This article is free to access.

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

APA

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.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free