Combining proofs and programs

Dependently typed languages allow us to develop programs and write proofs quickly and without errors, and the last decade has seen many success stories for verified programming with dependent types. Despite these successes, dependently typed languages are rarely used for day-to-day programming tasks. There are many reasons why these languages have not been more widely adopted. This thesis addresses two of them: First, existing dependently typed languages restrict recursion and require programmers to prove that every function terminates. Second, traditional representations of equality are inconvenient to work with because they require too much typing information and because their eliminations clutter terms. This thesis introduces PCC&thetas;, a new dependently typed core language that addresses these problems. To handle potentially non-terminating computations, PCC&thetas; is split into two fragments: a programmatic fragment with support for general recursion, and a logical fragment that is restricted for consistency. Crucially, while the logical fragment is consistent, it can reason about programs written in the inconsistent programmatic fragment. To make equality reasoning easier, PCC&thetas; includes a novel heterogeneous notion of equality whose eliminations are not marked in terms. The metatheory of PCC&thetas; is studied in detail, including a complete proof of normalization and consistency for its logical fragment. The normalization proof required the development of a novel technique, partially step-indexed logical relations, which is motivated and explained. Additionally, to demonstrate that PCC&thetas; addresses the problems described above, we have extended it to a complete core language Theta, adding features like user-defined datatypes and an infinite hierarchy of universes. Several examples are carried out in Theta, and an implementation is available