PhD Proposal: Typed Embeddings for Metaprogramming

https://umd.zoom.us/my/jprinz
Interactive theorem provers can check formal proofs written by a user, usually in dependent type theory. Inevitably formal proofs contain many tedious details, and so the most successful of these theorem provers supply the user with metaprogramming facilities which can be programmed to automatically perform common operations. In general, these metaprogramming tools are written in a separate language, and operate on an un-typed representation of the core type theory. Unfortunately, this lack of type checking for metaprograms makes the process of writing them bug-prone and difficult.
This problem could be solved if metaprograms could operate on a typed embedding. Embeddings are encodings of one formal language into another, in this case of the proof language into the metaprogramming language. In particular, programs over intrinsically typed embeddings produce well-typed outputs by construction. But so far despite several attempts, intrinsically typed embeddings of dependent type theory itself have been complex and prohibitively difficult to program with. This dissertation proposal describes a new paradigm for building an embedding of dependent type theory which is designed to facilitate convenient typed operation by metaprograms.
I also present my prior work in this area. The first work serves as an example of a metaprogram --- an algorithm for combining two inductive relations into one representing their conjunction, which is useful for generating data meeting a given specification. This work was carried out using a standard untyped embedding of Coq, and involved implementation difficulties characteristic of an untyped metaprogram which demonstrate the need for a typed embedding of dependent type theory. Next, I present a technique for organizing a deep embedding of dependent type theory using a shallow embedding, which simplifies the definition of term equivalence and results in an embedding which is convenient to program with, although with some limitations. Finally, I present a structure editor which provides structure preserving operations over programs, and makes use of an embedding of a simple type theory in its implementation. These works demonstrate the value of representing a type system using inductive relations, and the proposed work builds on their techniques.