Clara Schneidewind: Bachelor's Thesis

Saarland University Computer Science

Regularity and Linearization of Tail-recursive programs

Advisor: Gert Smolka


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.



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.

Clara Schneidewind, Sat Oct 31 15:30:16 2015