SHF: Medium: Collaborative Research: Principled Optimizing Compilation of Dependently Typed Languages

Cornell University, Ithaca NY

Investigators

Abstract

Title: SHF: Medium: Collaborative Research: Principled Optimizing Compilation of Dependently Typed Languages The project focuses on a form of software engineering with program verification: writing programs with logical, machine-checkable proofs of correctness, reliability, or security. Such proofs can be done for programs written in conventional programming languages, but the "proof theory" of these languages is complex and difficult, which makes verification time-consuming and expensive. New, "dependently typed" programming languages use principles of functional programming and advanced type systems to achieve a smoother and cleaner proof theory, so that verifying the correctness and safety of software (written in these new languages) is much easier. In this project, the research is to build compilers for these new languages that are efficient and are verified correct. The intellectual merits are in the challenges and opportunities that occur in dependently typed, purely functional contexts, such as the Coq proof assistant. The exciting opportunities that arise only in this context are the ability to choose evaluation order for any sub-term (since Coq's language is pure and total), the ability to open a compiler to user-specified (and certified) rewrite rules that support application-specific optimization, and the ability of programmers to use the Calculus of Inductive Constructions (CiC) proof theory of Coq to verify their programs. The challenges we face, unique to this setting, include the need to determine and erase those terms that are computationally irrelevant. A major foundational challenge is attempting to preserve types (and hence proofs) as we perform lowering transformations, such as conversion to continuation-passing style (CPS) or static single assignment (SSA). Our strategy is to use type and proof-preserving compilation where possible, and where not, to prove a simulation-based notion of correctness. The broader impacts will include (1) pedagogical materials on verified functional programming in Coq; (2) training of graduate students; and (3) improvements in software engineering practice, in enabling practical verified functional programming.