Publications
High-Assurance Software: LDRD Report
This report summarizes our work on methods for developing high-assurance digital systems. We present an approach for understanding and evaluating trust issues in digital systems, and for us- ing computer-checked proofs as a means for realizing this approach. We describe the theoretical background for programming with proofs based on the Curry-Howard correspondence, connect- ing the field of logic and proof theory to programs. We then describe a series of case studies, intended to demonstrate how this approach might be adopted in practice. In particular, our stud- ies elucidate some of the challenges that arise with this style of certified programming, including induction principles, generic programming, termination requirements, and reasoning over infinite state spaces.