Using Dependent Types to Certify the Safety of Assembly Code
Abstract elided by the publisher.
Related papers
- A type system for certified binaries POPL 2002
- The Design and Implementation of a Certifying Compiler PLDI 1998
- Inferable object-oriented typed assembly language PLDI 2010
- Principled Scavenging PLDI 2001
- A certified type-preserving compiler from lambda calculus to assembly language PLDI 2007
- A type system for certified binaries TOPLAS 2005
- From system F to typed assembly language TOPLAS 1999
- Modular verification of concurrent assembly code with dynamic thread creation and termination ICFP 2005