Mechanized Reasoning for Binding Constructs in Typed Assembly Language Using Coq
Nadeem Abdul Hamid · 2006
Mechanized reasoning about programming languages and type sys-tems is becoming increasingly important for the development of certified code frameworks. For instance, in order to realize the safety and security potential of proof-carrying code (PCC) [3] the development of formal, machine-checkable proofs is a necessity. Much of the difficulty and research surrounding PCC involves the generation of large, complex proofs in a user-friendly, automated way. Several approaches in this respect [2, 1] rely on encoding a typed assembly language (TAL) and mechanically proving its safety properties. This work describes some aspects of the author’s experience with the mechanical encoding of TAL for several prototype sys-tems developed in the Yale FLINT group’s PCC project. In partic-ular, an approach to encoding TAL binding constructs is presented in which a first-order representation using de Bruijn indices is used