Ed Westbrook, Higher-Order Encodings with Constructors

As programming languages become more complex, there is a growing call in the research community for machine-checked proofs about programming languages. A key obstacle to this goal is in formalizing name binding, where a new name is created in a limited scope. Name binding is used in almost every programming language to refer to the formal arguments to a function. For example, the function f(x) = x * 2, which doubles its argument, binds the name x for its formal argument. Though this concept is intuitively straightforward, it is complex to define precisely because of the intended properties of name binding. For example, the above function is considered "syntactically equivalent" to f(y) = y*2.

It is the goal of this dissertation to posit a new technique for encoding name binding, called Higher-Order Encodings with Constructors or HOEC. HOEC encodes name binding with a construct called the nu-abstraction, which binds new constructors in a limited scope. These constructors can then be used to encode names. nu-abstractions already have the required properties of name bindings, so name binding need only be formalized once, in the definition of the nu-abstraction. The user thus then gets name binding "for free" and need not define it explicitly.

To demonstrate the usefulness of HOEC, this dissertation gives a language, CNIC, with a limited form of nu-abstractions. CNIC is a form of Intensional Constructive Type Theory or ICTT, a formalism which is both a programming language and a logical theory whose proofs can be checked by machine. CNIC is the first form of ICTT with nominal features that has been proven consistent. The consistency proof for CNIC also has independent interest, as it demonstrates how limited nu-abstractions can be added to a wide variety of languages.