Loading...
Please wait, while we are loading the content...
Similar Documents
A Higher-Order Abstract Syntax Approach to Verified Compilation of Functional Programs Thesis Proposal
| Content Provider | Semantic Scholar |
|---|---|
| Author | Wang, Yuting |
| Copyright Year | 2016 |
| Abstract | We propose to develop a dissertation in the broad area of verified compilation of programming languages. Our specific focus will actually be on a narrower class of languages called the functional programming languages or, more simply, the functional languages. Compilation in this context is generally visualized as the application of a series of transformations to input programs, resulting eventually in low-level instructions that can be executed directly on existing hardware. Our goal, then, is to show how such transformations can be encoded in programs and how it can be demonstrated that these programs modify or simplify the original code while preserving its meaning. A central thesis underlying our work is that the tasks of implementing and verifying the mentioned transformations is significantly assisted by the use of a particular approach, called the higher-order abstract syntax or HOAS approach, to representing, manipulating, and reasoning about programs in a functional language. The work that we will undertake in this dissertation is aimed at validating this thesis: in particular, we will further develop an existing framework that supports the HOAS approach and we will demonstrate how this framework can be used effectively in the verified compilation of functional programming languages. In the rest of this introductory section, we provide a more detailed background to the work we propose. We begin with a motivation for verified compilation in general and for functional languages in particular. In Section 1.3, we explain briefly the relevance of the HOAS approach to the task of describing and verifying transformations on functional programs. In Section 1.4, we outline the framework that supports the HOAS approach that we intend to use in this dissertation and we sketch the specific work that we will carry out in its context. Section 1.5 summarizes the expected contributions of our work. The rest of the thesis proposal is devoted to providing more details regarding the |
| File Format | PDF HTM / HTML |
| Alternate Webpage(s) | https://www-users.cs.umn.edu/~wang1740/files/yuting_thesis_proposal.pdf |
| Language | English |
| Access Restriction | Open |
| Content Type | Text |
| Resource Type | Article |
