low-level imperative languages

JAR
2008

124views more JAR 2008»

Formal Verification of a C-like Memory Model and Its Uses for Verifying Program Transformations

13 years 11 months ago

This article presents the formal verification, using the Coq proof assistant, of a memory model for low-level imperative languages such as C and compiler intermediate languages. Be...

Xavier Leroy, Sandrine Blazy

claim paper

Read More »

click to vote

ESOP
2007
Springer

123views Programming Languages» more ESOP 2007»

Dependent Types for Low-Level Programming

14 years 5 months ago

Download www.eecs.berkeley.edu

In this paper, we describe the key principles of a dependent type system for low-level imperative languages. The major contributions of this work are (1) a sound type system that c...

Jeremy Condit, Matthew Harren, Zachary R. Anderson...

claim paper

Read More »

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers