PRL Seminars

I will present the Habilitation thesis of C. Kreitz.

In his thesis, he formalized existing approaches to program synthesis using NuPrl. He investigated the synthesis paradigms "proofs as programs," transformational synthesis, and algorithm schemata. Embedding these paradigms in a formal framework allows to compare them, to justify their application, and to prove the soundness of synthesis steps. The formal framework may be considered as a starting point to build up global programming knowledge; i.e., knowledge about the basic domains in programming, about program design strategies, and about program optimiziation.