I present two case studies supporting the assertion that type-based methods enable effective certified programming. By certified programming, I mean the development of software with formal, machine-checked total correctness proofs. While the classical formal methods domain is most commonly concerned with after-the-fact verification of programs written in a traditional way, I explore an alternative technique, based on using dependent types to integrate correctness proving with programming. I have chosen the Coq proof assistant as the vehicle for these experiments. Throughout this dissertation, I draw attention to features of formal theorem proving tools based on dependent type theory that make such tools superior choices for certified programming, compared to their competition.
In the first case study, I present techniques for constructing certified program verifiers. I present a Coq toolkit for building foundational memory safety verifiers for x86 machine code. The implementation uses rich specification types to mix behavioral requirements with the traditional types of functions, and I mix standard programming practice with tactic-based interactive theorem proving to implement programs of these types. I decompose verifier implementations into libraries of components, where each component is implemented as a functor that transforms a verifier at one level of abstraction into a verifier at a lower level. I use the toolkit to assemble a verifier for programs that use algebraic datatypes using only several hundred lines of code specific to its type system.
The second case study presents work in certified compilers. I focus in particular on type-preserving compilation, where source-level type information is preserved through several statically-typed intermediate languages and used at runtime for such purposes as guiding a garbage collector. I suggest a novel approach to mechanizing the semantics of programming languages, based on dependently-typed abstract syntax and denotational semantics. I use this approach to certify a compiler from simply-typed lambda calculus to an idealized assembly language that interfaces with a garbage collector through tables listing the appropriate root registers for different program points. Significant parts of the proof effort are automated using type-driven heuristics. I also present a generic programming system for automating construction of syntactic helper functions and their correctness proofs, based on an implementation technique called proof by reflection.