This project investigates the usage of interactive proof assistants for reasoning about the properties of programs written in functional programming languages, with the specific focus on code written in the Haskell programming language and verified using the Coq proof assistant. Results from this project will increase our understanding of mechanical reasoning and its role in the development of a wide variety of software systems through specification identification and bug detection. In other words, development teams should be able to use proof assistants to discover a formal description of the properties and invariants that should hold for a code base and to identify parts of the code base that violate those properties. Additionally, the project develops a corpus of translated libraries, their specifications, and properties that may be used in future developments.
The project centers around the development, extension and use of a verification tool, called hs-to-coq that semi-automatically translates unmodified Haskell source code to the language of the Coq proof assistant. This project extends hs-to-coq so that it may be applied to effectful code which express side effects like input/output and other stateful computations using monadic actions. The project considers Haskell code that makes use of concurrency, mutable state, exceptions, or operating system calls. To this end, project members investigate the use of monadic and algebraic structures, such as interaction trees, free monads and effect handlers, both in the original Haskell code and in support of modeling effectful code in Coq.
This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.
