Advisor: Gert Smolka
Abstract:
We study equivalence transformations for tail-recursive context-free programs. Context-free programs generalize regular programs and can be seen as an abstract model for imperative programs. We take the view that the execution of a context-free program generates a trace of actions and employ a notion of program equivalence based on traces. We discuss equivalence preserving translations from tail-recursive context-free programs to regular programs and from regular programs to linear tail-recursive programs (regular and linear tail-recursive programs are both tail-recursive). We also verify a direct transformation from tail-recursive to linear tail-recursive programs.
To make the relation between tail-recursive context-free programs and imperative programs more explicit, we show how abstract IMP programs can be encoded using context-free programs. We show that program equivalence with respect to the big-step semantics of two abstract IMP programs is implied by the equivalence of their context-free encodings.
References:
I gave my initial Bachelor's seminar talk on May 22nd, 2015.
My second Bachelor's seminar talk was given on July 17th, 2015.
I submitted my thesis on October 21st, 2015.
The thesis is accompanied by a Coq development.
I gave my final talk on October 30th, 2015.