Proof Theoretic Approach to Specification Languages
Jawahar Lal Chirimar
A Dissertation in Computer and Information Science
In this thesis I study FORUM as a
specification language. FORUM is a higher-order logic based on the
logical connectives of Linear Logic. As an initial example, I
demonstrate that FORUM is well suited for specifying concurrent
computations by specifying the higher-order pi-calculus. Next, I
focus on the problem of specifying programming languages with
higher-order functions, and imperative features such as assignable
variables, exceptions and first-class continuations. I provide a
modular and declarative specification of an untyped programming
language, UML, which contains the above mentioned features. Further, I
use the proof theory of FORUM to study program equivalence for the
functional core of UML augmented with assignable variables. Using my
compositional specifications in FORUM, I prove equivalence of programs
that have been challenging for other specification languages. Finally
I study the operation semantics of DLX, a prototypical RISC machine. I
specify the sequential and pipelined operational semantics of DLX with
important optimizations such as call-forwarding and early branch
resolution, and prove them to be equivalent. Furthermore, I study the
problem of code equivalence via the FORUM specification, and, in
particular, analyze the problem of code rescheduling for DLX.
(Postscript)