[facebook digest] Paper submitted

1. 週末試著把積好久的 blog posts 出清吧⋯ 然後就可以繼續寫 reading course 的小論文了。    [2011-04-29 20:29:38 +0000]
2. Preparing to go to the legendary May Day.    [2011-05-01 02:37:56 +0000]
   • 王** ⇒ 是五月天嗎XDD    [2011-05-01 02:54:33 +0000]
3. 補眠到剛剛。八點多吃的 double sausage & egg McMuffin meal 應該是會當早午餐了。    [2011-05-01 11:27:10 +0000]
4. There are really two kinds of ornament composition: vertical and horizontal. The horizontal one is the one introduced in the paper; the vertical one seems to be less interesting. The implementation of projection & integration, however, relies on converting horizontal composition to vertical composition. That's more interesting...    [2011-05-02 19:05:28 +0000]
5. 「這不是正確與否的問題，而是規約問題。目前我們只能說，在一個規約下，就得到一個明確的答案。到底是採用那一種規約較方便、好用與合理呢？這就必須作進一步的考察與比較，從比較中作選擇。」 ↦ 先算乘除後算加減 - 數學解惑四則    [2011-05-04 13:34:36 +0000]
   • Josh Ko ⇒ 我也是這樣覺得呀。「相鄰」和「星號」是兩個不同的算符，語意上行為一樣，語法上前者優先度較高。（說不定學 lambda-calculus 的人都會這麼覺得？）真的怕歧義、不想加括號（確實有點醜）然後不嫌麻煩的話⋯ 有篇 functional pearl "Enumerating the Rationals" 裡面是特地把 1/2 的 1 打成上標、2 打成下標，可以考慮？    [2011-05-04 14:09:34 +0000]
   • S************ ⇒ 用上下標的想法不錯，等下試試看    [2011-05-04 14:19:49 +0000]
6. It seems that realisability is always talked about relative to a more complete notion, e.g., provability, and there is always an adequacy theorem (which is the realisability transformation in the paper) saying that, e.g., provability implies realisability.    [2011-05-04 15:19:48 +0000]
   • Josh Ko ⇒ When Kleene introduced realisability, proofs were still *mental* constructions and did not have a concrete form. He defined realisability to say that natural numbers, interpreted "recursively", can be considered concrete proofs which reflect the mental proofs.    [2011-05-04 15:46:37 +0000]
   • Josh Ko ⇒ So an adequacy theorem is needed, because the realisability view should faithfully reflect the proving view. However, the realisability view can be incomplete, so realisability does not imply provability.    [2011-05-04 15:50:27 +0000]
   • Josh Ko ⇒ For Kleene's original intention, he certainly wished the realisability view was incomplete, because he wished to talk about intuitionistic logic in classical logic.    [2011-05-04 15:51:24 +0000]
7. This should be the argument that realisability implies consistency: Let Γ denote some consistent axioms and φ a realisable proposition.
   
   Γ ∧ φ → ⊥ provable
   ⇒ { adequacy }
   Γ ∧ φ → ⊥ realisable
   ⇒ { Γ and φ realisable }
   ⊥ realisable
   ⇒ { which is not the case }
   contradiction.
   
   Hence from Γ ∧ φ we cannot derive ⊥, i.e., Γ ∧ φ is consistent. This can be developed into an induction on the number of axioms in Γ.    [2011-05-04 15:33:21 +0000]
8. Used \section*{Acknowled\smash gements} to squeeze the last reference entry into the last page.    [2011-05-04 18:57:26 +0000]
9. Paper now reached the closed-beta stage!    [2011-05-04 22:26:33 +0000]
   • Josh Ko ⇒ 翻譯：論文進入封測階段！    [2011-05-04 22:26:49 +0000]
   • Y********** ⇒ 瞄了一下, 好難好難好難 XD    [2011-05-05 13:38:20 +0000]
   • Josh Ko ⇒ 蛤，不會啦⋯    [2011-05-05 14:49:15 +0000]
10. A weakness that just came to my mind: The realisability interpretation cannot be straightforwardly extended to function types. Specifically, the adequacy theorem does not hold for functions, i.e., not all complete functions have a realiser. This does not undo the contribution of the paper, but in the worst case we would have to rename the realisability transformation to something else.    [2011-05-05 18:19:24 +0000]
11. Almost forgot that an even more fun & exciting part of writing a paper is responding to comments!    [2011-05-06 17:03:22 +0000]
12. Borrowed Jacobs' Categorical Logic and Type Theory. But as "[t]he reader is assumed to be familiar with the basic notions of category theory, such adjunctions, (co)limits and Catesian closed categories" and the chapter on **first-order** dependent type theory starts on page **581**, it's going to be a very tough read...    [2011-05-06 19:35:12 +0000]
13. 剛才和 Frank 一塊晨間散步時想到 Mazurka Op 59 No 1 的這一句，琢磨著前四個小節的顏色與鬆緊時，突然發現這種質地和那些極其精煉的古詩句是完全相通的。交響曲用完整的主線支線發展交織去鋪敘情感（如同小說一般），馬厝卡則是用精煉的句式、藉著細緻的音色與節奏變化在一瞬間表現一切。 ↦ http://www.facebook.com/photo.php?fbid=186698124716066&set=a.126799950705884.40277.100001276392360&type=1    [2011-05-08 08:05:27 +0000]
    • Josh Ko ⇒ 對啊 XD。    [2011-05-08 14:13:10 +0000]
    • S********** ⇒ 我喜歡chopin的nocturne :D    [2011-05-08 20:32:56 +0000]
14. Relational ornaments?    [2011-05-09 19:54:08 +0000]
    • Josh Ko ⇒ Gosh, can it be the realisability predicate for the ornamentation from Desc to Orn?!    [2011-05-09 20:01:11 +0000]
    • Josh Ko ⇒ It turns out to be the algebraic ornament of Orn using the algebra of its decoding function (basically)!    [2011-05-09 20:36:55 +0000]
15. "Interestingly, in Chinese philosophy yin symbolizes open and hence corresponds to the open world of coSQL, and yang symbolizes closed and hence corresponds to the closed world of SQL." Never heard of that...    [2011-05-11 08:48:58 +0000]
    • L************** ⇒ hahahaha.    [2011-05-11 09:18:50 +0000]
    • L********** ⇒ Do you also study semantics of database querying languages?    [2011-05-11 10:53:31 +0000]
    • Josh Ko ⇒ It's a paper we are going to read in a Haskell reading club.    [2011-05-11 11:14:16 +0000]
    • L********** ⇒ Interesting. What's the name of the paper?    [2011-05-11 11:15:19 +0000]
    • Josh Ko ⇒ A co-relational model of data for large shared data banks.
      http://portal.acm.org/citation.cfm?doid=1924421.1924436
      I find it rather too sketchy, though...    [2011-05-11 11:16:47 +0000]
16. General (horizontal) composition is working... XD    [2011-05-11 14:37:21 +0000]
17. This is the key to victory! (A tribute to GGG, of course.)
    
    -- fibre product
    data _⋏_ {A B C : Set} (e₁ : A → C) (e₂ : B → C) : Set where
    _,_ : ∀ {c} → e₁ ⁻¹ c → e₂ ⁻¹ c → e₁ ⋏ e₂    [2011-05-11 15:19:32 +0000]
18. Interesting... It is nontrivial to express the datatype of relational algebraic ornaments as an ornamentation of the datatype of the relational ornaments, if possible at all.    [2011-05-12 08:57:00 +0000]
19. Some candidate concerts.    [2011-05-12 19:23:39 +0000]
    • Josh Ko ⇒ Rachmaninoff: Piano Concerto No 3 + Tchaikovsky: Symphony No 6 (Pathétique)
      30 June - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/philharmonia-orchestra-53788
      Chopin: Piano Concerto No 1
      4 Dec - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/philharmonia-orchestra-56505
      Rachmaninoff: Piano Concerto No 2
      23 Oct - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/royal-philharmonic-orchestra-58985
      14 Feb 2012 - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/london-philharmonic-orchestra-56718
      Brahms: Violin Concerto
      25 Sep - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/philharmonia-orchestra-56421
      22 Feb 2012 - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/london-philharmonic-orchestra-56664
      12 June 2012 - http://ticketing.southbankcentre.co.uk/find/music/classical/tickets/royal-philharmonic-orchestra-58970    [2011-05-12 19:23:43 +0000]
    • Josh Ko ⇒ Tchaikovsky: Piano Concerto No 1
      4 Aug - http://www.oxfordplayhouse.com/ticketsoxford/?event=12255    [2011-05-12 19:26:03 +0000]
    • W********* ⇒ 通通去了阿    [2011-05-13 02:08:19 +0000]
20. Conclusions: 1. I am offered more freedom regarding the research direction than I had expected. 2. Let's keep developing stories based on universe encodings, and also start learning about fibred categories, about which Jeremy can provide more help.    [2011-05-13 22:17:08 +0000]
    • Josh Ko ⇒ I won't put particular emphasis on the categorical approach, though, at least in the near future, because it can take quite some time for my categorical maturity to catch up with my dependently typed programming skills.    [2011-05-13 22:17:11 +0000]
21. Stuck on a special case of the adjoint functor theorem for a while (but got through eventually): For a partial order, prove that "every subset has a least upper bound" implies "every subset has a greatest lower bound".    [2011-05-14 22:44:39 +0000]
    • Josh Ko ⇒ Suddenly not very confident whether it is a special case of the adjoint functor theorem. Is it?    [2011-05-14 22:56:50 +0000]
    • L************** ⇒ A monotone function (functor) preserves greatest upper bounds (colimits) if and only if it has a right adjoint. The solution set condition is automatically satisfied since poset is a set.    [2011-05-14 23:23:32 +0000]
    • Josh Ko ⇒ Yes, but it says nothing about the existence of (co)limits...    [2011-05-15 07:40:23 +0000]
    • L************** ⇒ in (meet-)complete lattice ...    [2011-05-15 13:37:02 +0000]
22. 退役快一年才打上役政署發的領帶（和領帶夾）XD。    [2011-05-15 20:41:29 +0000]
23. Impressed by how much can be achieved by using fibre products.    [2011-05-15 23:25:08 +0000]
    • T************** ⇒ 纖維積是啥    [2011-05-16 01:04:27 +0000]
    • Josh Ko ⇒ 給兩個 functions f : A -> C and g : B -> C, 它們的 fibre product 是 { (a, b) \in A * B | f(a) = g(b) }.
      http://en.wikipedia.org/wiki/Pullback_(category_theory)    [2011-05-16 07:07:48 +0000]
24. When Delta and nabla clash — Δ S O' ⊙ ∇ s O = O' s ⊙ O.    [2011-05-16 08:08:41 +0000]
    • T************** ⇒ While Ita and alpha clash -- +.+ @@ = T^T QQ    [2011-05-16 14:50:49 +0000]
25. "Martin Campbell-Kelly is emeritus professor in the Department of Computer Science at the University of Warwick, where he specializes in the history of computing." 有人專門研究計算史耶！香香可以考慮一下 XD。    [2011-05-16 15:30:06 +0000]
    • W********* ⇒ 真的有唷XD    [2011-05-17 02:28:14 +0000]
26. 「寫於 1845 年的作品 59 向來是諸多鋼琴名家最愛的一組馬厝卡，三曲旋律出色又有蕭邦晚期獨到的轉調手法；特別是第一曲，其轉調之繁複巧妙讓人嘆為觀止，幾乎每一拍都可有所變化，聽者卻不覺其勉強古怪，只能感受無窮無盡的色調光影與心理層次。而搭配如此和聲的，卻是旋律線條相當明確，在庫加維亞克與馬厝爾兩者間徘徊的舞曲，更可見蕭邦的巧思。」（焦元溥《聽見蕭邦》p 297。）    [2011-05-16 17:25:44 +0000]
    • Josh Ko ⇒ 唉，重聽四首即興曲也覺得好想練啊。    [2011-05-16 18:01:31 +0000]
27. "èe-téks ding~~" XDD ↦ Don Knuth - An Earthshaking Announcement - Transcription    [2011-05-16 21:16:29 +0000]
28. 7 am - Morning walk with Frank
    8 am - Breakfast
    9 am - Essay
    12 pm - Lunch
    2 pm - Piano playing
    4.30 pm - Departmental seminar
    6 pm - Dinner
    7 pm - Essay
    10 pm - Bedtime reading
    
    Wonderful schedule! ↦ SpongeBob SquarePants - The Best Day Ever    [2011-05-17 05:16:54 +0000]
    • J********** ⇒ Are you saying that you'll play piano for nearly 2 hours?!    [2011-05-17 08:42:46 +0000]
    • Josh Ko ⇒ I am!    [2011-05-17 08:51:14 +0000]
29. I suspect the reason that the inverse realisability transformation is not available in, say, the Calculus of Constructions is simply that we are not allowed to inspect the realisability proof and accordingly produce a complete object because the former resides in Prop and the latter in Set...    [2011-05-17 08:53:54 +0000]
30. Interesting — trying to explain dependently typed programming to an audience who I cannot even assume to know what first-order logic is.    [2011-05-17 21:36:30 +0000]
    • Josh Ko ⇒ and what types are!    [2011-05-17 21:37:03 +0000]
    • Josh Ko ⇒ strictly speaking, not even what proofs are...    [2011-05-17 21:40:33 +0000]
    • L************** ⇒ ............ tell me if you can make it. If it is possible, there is no reason why we can't teach category theory to the same audience (via Curry-Howard-Lambek isomorphism).    [2011-05-17 21:59:28 +0000]
31. Abstract submitted to Oxbridge Taiwan Science and Technology Symposium.    [2011-05-17 22:50:43 +0000]
    • Josh Ko ⇒ Introduction to dependently typed programming
      
      It is desirable to be able to check whether the dynamic behaviour of a program satisfies a certain property just by examining the static structure of the program, without actually executing it. To state what property a program should satisfy, we assign an appropriate type to the program. Type checking — the process of finding a proof that a program has a certain type — can then be done mechanically, because the structure of such proofs are designed in such a way that they can be synthesised by following the structure of the program being checked. Modern programming languages thus employ type systems to help programmers to check properties of programs. The more sophisticated a type system is, the more properties can be expressed and checked. Since the last decade of the last century, dependent types have come into play — they are a family of type systems that are strong enough to specify exact behaviour of programs. Programming language researchers are still actively finding ways to fit this powerful type system for practical programming. In this talk I will attempt to sketch how dependently typed programming might change the way we program fundamentally.    [2011-05-17 22:50:51 +0000]
    • S************ ⇒ Oh, is that an event organised by the Taiwanese student society? Must be fun, good luck!    [2011-05-18 05:39:23 +0000]
    • S************ ⇒ You should come and give a talk in my lecture. :)    [2011-05-18 05:41:21 +0000]
    • Josh Ko ⇒ Then I can assume much more background! On the other hand, I do not think I can do better than you... (Yesterday I just reviewed your correspondence with Conor on observational equality back in March 2009!)    [2011-05-18 05:49:29 +0000]
    • S************ ⇒ Was there such a conversation? It must be asking Conor lots of questions and still feel puzzled...    [2011-05-18 05:52:07 +0000]
    • S************ ⇒ BTW, I believe that the OTSTS series was initiated by Duen-Wei, and I was one of the 1st generation speakers. :) Arrr.. sweet memories~    [2011-05-18 05:53:17 +0000]
    • Josh Ko ⇒ And you talked about... relational derivations?!    [2011-05-18 07:39:36 +0000]
    • S************ ⇒ Something more general --- about 1. how programs could go wrong and why we need to prove the correctness of programs (and that by correctness we mean being correct w.r.t a specification), and 2. in proofs we work purely symbolically. I am not sure how many of them understood 2.    [2011-05-18 09:53:17 +0000]
    • Josh Ko ⇒ They sound like reusable ideas for my talk.. XD    [2011-05-18 10:11:56 +0000]
    • S************ ⇒ Haha... I will send you my old slides. :)    [2011-05-18 10:13:45 +0000]
    • Josh Ko ⇒ Thanks a lot!    [2011-05-18 10:16:18 +0000]
32. About time to get a haircut...    [2011-05-18 13:29:59 +0000]
33. My head becomes considerably lighter after having a long awaited haircut. Now I can stuff more things about equalities in my head.    [2011-05-18 15:56:49 +0000]
34. After listening to the recording, I found that my Mazurkas Op 50 were not as awful as I thought.    [2011-05-18 17:47:00 +0000]
35. I shall focus on these pieces in the near future:
    
    Mazurkas Op 50
    Mazurka Op 59 No 1
    Mazurkas Op 63 No 2 & 3
    Ballade No 4, Op 52
    Impromptu No 1, Op 29
    Nocturne No 15 in F minor, Op 55 No 1
    
    Only Op 59 No 1 and Op 63 No 3 are completely new to me.    [2011-05-18 17:54:03 +0000]
    • Josh Ko ⇒ At the current rate, however, I expect that Ballade No 4 would take at least another year...    [2011-05-18 17:55:52 +0000]
    • J********** ⇒ Seriously, any intent of switching your dphil to musicology? Or at least, a double major of cs and music? ^^    [2011-05-18 18:11:54 +0000]
    • Josh Ko ⇒ I think music will always be more like an excursion rather than a destination to me. Earning a DPhil in that is too much for an excursion...    [2011-05-18 19:54:31 +0000]
    • J************* ⇒ Besides, it's good to hang on to at least one passion that's not also a job...    [2011-05-19 11:36:40 +0000]
36. Streicher's habilitation thesis is very helpful for understanding the equality issue in type theory.    [2011-05-18 19:53:07 +0000]
    • L************** ⇒ Thomas Streicher?    [2011-05-18 20:00:21 +0000]
    • Josh Ko ⇒ That's him.    [2011-05-18 20:05:31 +0000]
37. Reluctant to write about equality...    [2011-05-19 21:18:37 +0000]
38. "Your Graduate Review will be with the Master, Dean of Graduates and your College Advisor and last 5 minutes." ... So it's like "hello/how're you doing/good/keep up with it/bye"?    [2011-05-20 12:53:03 +0000]
39. Got my first rejection: My abstract submitted to the Taiwanese Oxbridge Symposium wasn't selected. (Hope my next submission — which is more important — won't have the same fate.)    [2011-05-20 13:10:04 +0000]
    • J********** ⇒ 厚, 那個 committee 是看到鬼ㄡ><    [2011-05-20 13:36:26 +0000]
    • Josh Ko ⇒ I posted the abstract here, in case you didn't notice:
      
      https://www.facebook.com/Josh.HS.Ko/posts/189165994469279
      
      I do not know which part went wrong. Too trivial? Too hard? Too abstract? Too boring?    [2011-05-20 13:49:56 +0000]
    • J********** ⇒ actually, i just noticed that the deadline for that was May 12. Or it's been extended?    [2011-05-20 13:51:28 +0000]
    • S************ ⇒ Hmm.. my guess is that they have a limited number of slots and have to give priority to those who about to graduate soon. After all, it's not a serious peer review!    [2011-05-20 14:12:13 +0000]
    • F********* ⇒ Hi Josh: You are doing very well actually. Sometime referees don't understand how important of our research are. We still love our research and will definitely have great impact on Science and human society. That's for sure!    [2011-05-20 14:12:53 +0000]
    • J********** ⇒ Target for the upcoming comlab student conference in November!
      
      Might you be interested in volunteering a softeng talk? (They're not holding it regularly anymore, used to be on Fridays, but it's worth asking!)    [2011-05-20 14:15:09 +0000]
    • P************* ⇒ Getting used to rejections is a part of PhD training. cheers.    [2011-05-20 14:30:06 +0000]
    • S************ ⇒ Well, don't take this too seriously. It's just a social event and a rejection has nothing to do with the quality of your work.    [2011-05-20 14:56:29 +0000]
    • Josh Ko ⇒ Indeed, and it's not really my work after all. XD For the comlab student conference, I can just talk about my real work! (No longer need to presume no one knows what types are.) Max and Oege seemed to hint that they intend to hold the Programming Languages Seminar regularly from now on. In any case, I think I will surely get lots of chance to give talks.    [2011-05-20 15:04:52 +0000]
40. Received the second comment, which is long and nice. Feeling thrilled to answer it!    [2011-05-20 16:51:14 +0000]
    • Josh Ko ⇒ Spent three hours replying.    [2011-05-20 20:16:15 +0000]
41. If we do not need to avoid confusion, realisability is actually a good term...    [2011-05-21 07:55:08 +0000]
42. Helicopter taking off again.    [2011-05-23 19:08:10 +0000]
43. This excerpt from "The Humble Programmer" by Dijkstra, which I am rereading, forcibly reminds me of C++.    [2011-05-24 07:41:46 +0000]
    • Josh Ko ⇒ And if I have to describe the influence PL/I can have on its users, the closest metaphor that comes to my mind is that of a drug. I remember from a symposium on higher level programming languages a lecture given in defence of PL/I by a man who described himself as one of its devoted users. But within a one-hour lecture in praise of PL/I, he managed to ask for the addition of about 50 new "features," little supposing that the main source of his problems could very well be that it contained already far too many "features." The speaker displayed all the depressing symptoms of addiction, reduced as he was to the state of mental stagnation in which he could only ask for more, more, more....    [2011-05-24 07:41:53 +0000]
44. Got my copies of Categorical Logic and Type Theory, Categories for the Working Mathematician, Purely Functional Data Structures, and Computation and Reasoning from Amazon.co.uk. It is about time to embrace more category theory...    [2011-05-26 14:14:53 +0000]
    • W********* ⇒ 在英國也要疊滿床嗎    [2011-05-26 16:23:16 +0000]
    • Josh Ko ⇒ 一時之間湊不起來吧 XD。    [2011-05-26 16:51:45 +0000]
45. Now that the descriptions and ornaments form a proper category, the construction of horizontal ornament composition looks very much like a pushout...    [2011-05-26 14:28:57 +0000]
46. Came across the proceedings of SIGCSE in the basement communal area. ↦ SIGCSE    [2011-05-27 21:20:41 +0000]
47. Very tricky, this whole business about equality.    [2011-05-28 08:33:30 +0000]
48. Revising the paper again, watching the reference entries happily crossing the page limit...    [2011-05-29 09:20:50 +0000]
49. Nice... Not only the 15 references but also the last four lines of Acknowledgements have gone into page 13, and I've just started revision...    [2011-05-29 14:33:19 +0000]
50. Perhaps I should study a bit of music composition so I can learn to write beautiful papers!    [2011-05-30 18:41:29 +0000]
51. Everything was good before a sentence was inserted in page 5. Keep squeezing...    [2011-05-30 21:12:39 +0000]
    • Josh Ko ⇒ Successful after transforming a displayed definition to an inlined one.    [2011-05-30 21:18:18 +0000]
52. The title of the paper is reduced to only three words now, having to de-emphasise the connection with realisability.    [2011-05-30 21:45:06 +0000]
    • W************ ⇒ Only three words ... XD    [2011-05-31 01:36:14 +0000]
53. I think I am very close to the first release candidate, but I should go to bed now...    [2011-05-30 23:20:07 +0000]
54. I was wrong: I am still making quite a few revisions here and there...    [2011-05-31 14:49:32 +0000]
55. Submission deadline of WGP has been extended by two days, indicating there may not be enough submissions...?    [2011-06-01 09:20:08 +0000]
    • J******************* ⇒ 不管submission夠不夠再延個幾天是很多個conference的傳統阿    [2011-06-01 09:24:30 +0000]
    • Josh Ko ⇒ WGP 這種小眾 workshop 特別令人擔心 XD。    [2011-06-01 09:56:44 +0000]
    • J******************* ⇒ 小眾work shop吃個best paper拿來用阿XD    [2011-06-01 10:03:56 +0000]
    • S************ ⇒ 呵呵，現在還不知道 submission 有多少（雖然通常不多啦），是因為有人問，往年也都會延，所以就延了。延期通常不可以是 deadline 之前最後一刻，不然拼死趕進了 deadline 的人會不高興...    [2011-06-01 12:25:37 +0000]
    • Josh Ko ⇒ 有點像「lecture/seminar 的開始時間照慣例比公告慢五分鐘」的感覺⋯    [2011-06-01 13:21:10 +0000]
56. Paper submitted! But it is shown as Paper 1... (Please do let the workshop have other papers!)    [2011-06-01 18:28:51 +0000]
    • Josh Ko ⇒ Resubmitted, correcting "signaling" to "signalling."    [2011-06-01 21:42:24 +0000]
    • W************ ⇒ Could you submit your paper until the conference's deadline ?    [2011-06-02 01:32:18 +0000]
    • Josh Ko ⇒ Yes, we can always resubmit before the deadline.    [2011-06-02 05:38:28 +0000]
57. Finally gained access to the webpage database (after writing to the IT staff) and can update my own page. ↦ Department of Computer Science: Hsiang-Shang Ko    [2011-06-03 14:53:45 +0000]
    • J************* ⇒ Weren't you given access automatically?    [2011-06-03 19:58:03 +0000]
    • Josh Ko ⇒ No! My SSO account was not linked to the database account until today.    [2011-06-03 19:59:04 +0000]
58. Undergrads happily chatting on Merton Street, presumably having just finished their exams.    [2011-06-03 16:34:38 +0000]
    • Josh Ko ⇒ With occasional "Whoo~~~!!!" sounds.    [2011-06-03 16:35:21 +0000]
    • Josh Ko ⇒ Now "happy birthday to you"...    [2011-06-03 16:38:15 +0000]
    • Josh Ko ⇒ Peace has returned.    [2011-06-03 16:58:48 +0000]
59. Err... The word "laboratory" in "Ideas that were first developed in the laboratory environment of functional programming have proved their values in wider settings" was wrongly replaced by "Department of Computer Science"... XD ↦ Department of Computer Science, University of Oxford: Publication    [2011-06-03 21:37:49 +0000]
60. Bought a £40 book on Chopin for £3.99 at Oxfam. ↦ The Music of Chopin (Clarendon Paperbacks)    [2011-06-04 09:41:10 +0000]

--
現在已經累積五篇 blog posts 等著出清了⋯