GSS student report, Michaelmas Term 2010

This term I focused mainly on coursework but also started my survey on Type Theory and Intuitionism in general. First I list below some brief remarks about the three courses I take this term.

1. Lambda Calculus & Types: Since lambda-calculus is so fundamental to functional programming, I have heard of its various properties like Church-Rosser, strong normalisation of simply-typed lambda-calculus (and System F), but have never actually looked into their proofs. This course offered me a good opportunity to organise these topics and fill in the missing details.
2. Categories, Proofs & Processes: Category theory is also a frequently used tool whose essence I had never grasped except for the simplest ideas. Surprisingly, during this course I started to gain some intuition about universality and adjunctions, now being able to regard them as beautiful rather than incomprehensible. I will need to think more about these concepts, though, to understand them better and be able to use them reasonably intuitively.
3. Program Analysis: The keyword that attracted me was Galois connections, which is a specialised but highly useful form of adjunctions. Also I thought the mixture of theory and practice offered by this course may help me gain some concrete feelings about the application side which I am less familiar with. I find the course amusing but feel a bit awkward doing the practicals. It seems I am now more comfortable with writing proofs rather than hacking computer systems!

For the survey on Type Theory, I have basically finished reading [NPS90] on Martin-Löf's Type Theory and a few relevant papers like [ML87]. Perhaps as a bit of excursion, I have also skimmed through [Hey71] and [Dum77] on intuitionistic mathematics, whose details I am not in a hurry to go into. I am now in the middle of [Luo94] on the Extended Calculus of Constructions, which is based on Martin-Löf's Type Theory but proposes major modifications to it and adopts a different approach to presentation, and I find the book rather dry and considerably harder to comprehend. To make the survey more goal-oriented, I have started to think about how I might write the essay on Type Theory and dependently-typed programming which I am going to submit to Jeremy next term and work on a very early draft from time to time, hoping that could somehow guide my direction of surveying. What makes me slightly worried now is, though confident that I should be able to give a logically smooth summary, it seems more difficult to dig out all relevant previous works and include them in my writing. Hopefully it will look less difficult after I chase more references.

Finally, a comment on my work pattern. I did not do much planning this term, and, sadly, I do not think I have attained reasonable productivity, so a free style does not work very well for me. (Coursework may have taken a lot of my time, but I still think I could have been more productive.) Therefore, I intend to try to follow a timetable and work in a regular manner after this term ends. (It doesn't seem necessary to do the planning right now as the homework and coming exams will occupy most of my time.) Also I will try to set short-term goals for myself. Hopefully this strategy would enable me to complete the survey more quickly and spend more time thinking about some smaller research problems I have in hand.

* References

[Dum77] M. Dummett. Elements of Intuitionism. Clarendon Press, 1977.
[Hey71] A. Heyting. Intuitionism: An Introduction. Amsterdam: North-Holland Publishing, third revised version, 1971.
[Luo94] Z. Luo. Computation and Reasoning: A Type Theory for Computer Science. Clarendon Press, 1994.
[ML87] P. Martin-Löf. Truth of a proposition, evidence of a judgement, validity of a proof. Synthese, 73(3):407-420, December 1987.
[NPS90] B. Nordström, K. Peterson, and J. M. Smith. Programming in Martin-Löf's Type Theory: An Introduction. Oxford University Press, 1990.

--
譯成中文版我可能會被罵浪費時間⋯？XD