A-Translation - From Theory to Practice and Back

Diana Ratiu

(LMU Munich)

We overview the refined A-Translation method for uncovering the
computational content in the classical proofs, thus enabling the extraction of
algorithms from them. We will briefly present the successful application of
A-Translation on the base case proof for Dickson's Lemma and then suggest a
generalisation of the lemma. This later part refers to work in progress, since
we aim at extensions of the conditions which the refined A-Translation imposes,
such that the method becomes applicable to a larger scale of proofs.
Thursday 16th November 2006, 14:00
Board Room
Department of Computer Science