I submitted my diploma thesis titled Formalizing Semantic Bidirectionalization in Agda (source) to the University of Bonn in 2013. It was supervised by Janis Voigtländer and Andres Löh.
During my DFG-funded employment at the University of Bonn, that work was furthered (git) and I worked on the inductive program synthesis engine Igor2. Our changes to Igor2 are available at darcs clone http://subdivi.de/~helmut/academia/darcs/igor2.