Higher-order encodings with constructors
Robert B. Pless, Edwin M. Westbrook · 2008
As programming languages become more complex, there is a growing call in the research community 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 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 encoding name binding, called Higher-Order Encodings with Constructors or HOEC. HOEC encodes name binding with a construct called the ν-abstraction, which binds new constructors in a limited scope. These constructors can then be used to encode names. ν-abstractions already have the required properties of name bindings, so name binding need only be formalized once, in the definition of the ν-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, CPTT, with ν-abstractions. CPTT is a form of Intensional Constructive Type Theory, a formalism which is both a programming language and a logical theory whose proofs can be checked by machine. The key novelty that enables CPTT is the constructor predicates, which limits the constructors that may appear in a term, allowing pattern-matching to be defined. The consistency proof CPTT also has independent interest, as it demonstrates how a simpler form of name binding can be added to a wide variety of theories.