Wang, Yuting2017-03-142017-03-142016-12https://hdl.handle.net/11299/185114University of Minnesota Ph.D. dissertation.December 2016. Major: Computer Science. Advisor: Gopalan Nadathur. 1 computer file (PDF); xii, 246 pages.This thesis concerns the verified compilation of functional programming languages. Functional programming languages, or functional languages for short, provide a high degree of abstraction in programming and their mathematical foundation makes programs written in them easy to analyze and to be proved correct. Because of these features, functional languages are playing an increasingly important role in modern software development. However, there is a gap that must be closed before we can derive the full benefits of verifying programs written in functional languages. Programs are usually verified with regard to the computational models underlying the functional languages, while the execution of programs proceeds only after they are transformed by compilers into a form that is executable on real hardware. To get programs verified end-to-end, the compilers must also be proved correct. Significant strides have been taken in recent years towards the goal of verifying compilers. However, much of the attention in this context has been on imperative programming languages. The verification of compilers for functional languages poses some additional challenges. A defining characteristic of such languages is that they treat functions as first-class objects. In describing the compilation of programs written in functional languages and in reasoning about this compilation, it is therefore necessary to treat functions as data objects. In particular, we need to provide a logically correct treatment of the relationship between the arguments of a function and their use within its body, i.e., the binding structure of the function. Most existing proof systems for formal verification provide only very primitive support for reasoning about binding structure. As a result, significant effort needs to be expended to reason about substitutions and other aspects of binding structure and this complicates and sometimes overwhelms the task of verifying compilers for functional languages. We argue that the implementation and verification of compilers for functional languages are greatly simplified by employing a higher-order representation of syntax known as Higher-Order Abstract Syntax or HOAS. The underlying idea of HOAS is to use a meta-language that provides a built-in and logical treatment of binding related notions. By embedding the meta-language within a larger programming or reasoning framework, it is possible to absorb the treatment of binding structure in the object language into the meta-theory of the system, thereby greatly simplifying the overall implementation and reasoning processes. We develop the above argument in this thesis. In particular, we present and demonstrate the effectiveness of an approach to the verified implementation of compiler transformations for functional programs that exploits HOAS. In this approach, transformations on functional programs are first articulated in the form of rule-based relational specifications. These specifications are rendered into programs in lambda Prolog, a language that is well-suited to encoding rule-based relational specifications and that supports an HOAS-style treatment of formal objects such as programs. Programs in lambda Prolog serve both as specifications and as executable code. One consequence of this is that the encodings of compiler transformations serve directly as their implementations. Another consequence is that they can be input to the theorem proving system Abella that provides rich capabilities for reasoning about such specifications and thereby for proving their correctness as implementations. The Abella system also supports the use of the HOAS approach. Thus, the lambda Prolog language and the Abella system together constitute a framework that can be used to test out the benefits of the HOAS approach in verified compilation. We use them to implement and verify a compiler for a representative functional programming language that embodies the transformations that form the core of many compilers for such languages. In both the programming and the reasoning phases, we show how the use of the HOAS approach significantly simplifies the representation, manipulation, analysis and reasoning of binding structure. Carrying out the above exercise revealed some missing capabilities in the Abella system. At the outset, it was possible to reason about only a subset of lambda Prolog programs using the system. Some compiler transformations required the use of features not available in this subset. Another limitation was that it did not support the ability to reason about polymorphic specifications, thereby leading to a loss of modularity in programs and in reasoning. We have addressed these issues as well in this thesis. In particular, we have developed the theoretical underpinnings for introducing polymorphism into Abella and for treating the full range of lambda Prolog specifications. These ideas have also been implemented to yield a new version of Abella with the additional capabilities.enThesis or Dissertation