$\newcommand{\defeq}{\mathrel{\mathop:}=}$

## 2011/11/20

### GSS student report, Michaelmas Term 2011

I have mainly been concluding my first year's work since last report: I gave two talks at the DTP workshop in August and WGP (after which I also stayed for ICFP and the Haskell Symposium) in September, both receiving positive feedback; I polished up a dependently typed solution to the Dutch National Flag problem, used that as the motivating example for my transfer dissertation, and passed the transfer viva; a poster was made for the DNF development, which received the best poster award in this year's student conference and will be presented in APLAS in December. For the next stage of my research, I have been making steady progress, albeit slowly at the moment (with no significant output yet). I have set myself some reading tasks (including Jacobs' categorical logic and type theory book and Okasaki's purely functional data structures book as planned in the transfer dissertation), and identified a few concrete examples to play with (including the functional derivation of maximum segment sum and internalist de Bruijn indices used in typed representation of lambda terms), which hopefully can lead to interesting generalisations later. At a higher level, I believe I am having a better idea about how I will formulate the arguments for my thesis, while I estimate that it's possible but not easy to get all the technical results I need in time - hard work is therefore no doubt required!

--

Labels: