Applications of Languages with Self-Interpreters to Partial Terms and Functional Programming

Abstract —Those programming languages that contain self-interpreters have the added power of reflection, and allow dynam-ically controlling execution. In a logical language a complete self-interpreter is necessarily inconsistent. However, we demonstrate a logical language with a reasonably complete self-interpreter. We argue for its use as a simple formalism for reasoning about partial terms, and functional languages that allow both general recursion and dependent types. Since refinements of programming specifications often include partial terms, they need to be handled using formal rules. Likewise, we show formal rules for handling general recursion consistently in a simple language. Moreover, we demonstrate how to use an interpreter to reason about lazy evaluation. We argue that the interpreter can be integrated within theorem provers