Josh Ko

Hsiang-Shang Ko

Doctoral Student

Student, University College

Hsiang-Shang.Ko@cs.ox.ac.uk

39a St Giles, Oxford, OX1 3LW

Interests

I am interested in revealing structures of programs so the discipline of programming can be better understood and explained. Currently I believe that intuitionistic type theory, which brings harmony to programming and logic, and category theory, which abstracts algebraic constructions in a surprisingly succinct and elegant manner, are two promising ways to such a goal. More specifically, I am now keen to explore the potential of dependently typed programming for writing precisely typed programs such that their correctness is manifest in themselves. (I call this style internalism and tried to advertise the name in my WGP'11 paper jointly written with Jeremy.) My DPhil thesis is about improving composability of high-precision dependently typed programs by developing techniques based on Conor McBride's ornaments, which is part of the EPSRC-funded project Reusability and Dependent Types. The latest development is hosted on GitHub.

I am an enthusiast for classical music, especially the works of Chopin. I am also impressed by particular works of Tchaikovsky, Rachmaninoff, Brahms, and Bach. I play the piano and practise mainly Chopin (for an acceptable recording: Mazurka Op 50 No 3 in C-sharp minor, recorded on 6 Sep 2010). Shortly after I moved from college accommodation to a share house in August 2011, I rented a Knight K10 piano for two years and can now practise regularly, thanks to the support of my dear housemates.

I have maintained a general blog since 2005, i.e., the year I started my undergraduate studies. The posts are mostly in Chinese except the facebook digests I dump to the blog from time to time.

Biography

I graduated from National Taiwan University (NTU) in June 2009 with a BSc in Computer Science and Information Engineering and a minor in Mathematics. During my third and fourth year at NTU, I worked as a part-time research assistant to Shin-Cheng Mu at the Institute of Information Science, Academia Sinica, Taiwan, to which I returned as a full-time research assistant for 3 months from June to September 2010 after I finished my 11-month compulsory substitute service at the Ministry of the Interior, Taiwan. I started my DPhil studies at Oxford in October 2010.

More specifically: I delved into the paradigms and idiosyncrasies of C++ in high school and turned to mathematics after I entered NTU, seeking cleaner and more systematic approaches to structuring and understanding programs. Between my second and third year, I attended the first Formosan Summer School on Logic, Language, and Computation (FLOLAC’07) and was exposed to the basic programming language theories for the first time. Shortly after that I was recruited by Shin, a former Algebra of Programming research group member, under whose guidance I acquainted myself with functional programming, gained experience in dependently typed programming (in Agda), and tackled the Algebra of Programming, laying the foundations for my DPhil studies.

My Chinese name 向上 (Hsiang-Shang) means "upwards" and is an unusual one. (For an indication of how unusual the name is, you can google for my full Chinese name 柯向上 — all the sensible results are about me.) It's impossible to approximate its pronunciation acceptably accurately in English, however. On the other hand, Josh is a name I've used for years (since 1996, to be precise), so I am perfectly happy (in fact happier) to be called by the name in English.