The bedrock structured programming system: combining generative metaprogramming and hoare logic in an extensible program verifier

We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining character...

Full description

Bibliographic Details
Main Author: Chlipala, Adam (Contributor)
Other Authors: Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory (Contributor), Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science (Contributor)
Format: Article
Language:English
Published: Association for Computing Machinery (ACM), 2014-04-07T12:42:35Z.
Subjects:
Online Access:Get fulltext