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*.

[ PS | PDF ]