[facebook digest] Slides

1. 床前明月光，疑是地上霜；舉頭望明月，低頭思故鄉。    [2011-07-13 23:20:28 +0100]  [ 4 人說讚！]
   • W************ ⇒ You can listen to "登彼岸"    [2011-07-18 15:38:17 +0100]
2. Dare I not raise the big question at the beginning of my talk?    [2011-07-14 23:18:54 +0100]
   • Josh Ko ⇒ I have to do so for WGP, I think; but for DTP it might be possible just to tell a story. Will do some experiments.    [2011-07-14 23:23:33 +0100]
   • Josh Ko ⇒ (Because not asking a question at the beginning can make the talk disorienting. The audience at DTP can be assumed to have more relevant backgrounds, though, so this might work for them.)    [2011-07-14 23:42:08 +0100]
3. Not sure if internalist dependently typed programming will succeed. If programs and proofs are to be composed simultaneously, wouldn't that violate the principle of separation of concerns? Is there some way to defend internalism (against the principle)?    [2011-07-15 21:46:44 +0100]
   • Josh Ko ⇒ Perhaps we just need both internalism and externalism. Program in the internalist way to show that the program is constructed with some sort of correctness in mind; prove afterwards in the externalist way that the program has other properties.    [2011-07-15 22:01:53 +0100]
   • Josh Ko ⇒ This is not entirely convincing, though.. I hope I won't have to make the conclusion in my thesis that internalism should be abandoned.    [2011-07-15 22:18:39 +0100]
   • J************* ⇒ Best of both worlds?    [2011-07-16 18:21:15 +0100]
   • Josh Ko ⇒ Yeah.. I guess that's the way to go.    [2011-07-16 19:36:05 +0100]
4. 《悲愴》的震撼至今尚未消散。    [2011-07-15 23:37:08 +0100]
   • W************ ⇒ 為何？    [2011-07-18 15:36:42 +0100]
   • Josh Ko ⇒ 可看我 blog.    [2011-07-18 15:37:51 +0100]
5. Gattai - sorted vectors!    [2011-07-16 15:28:27 +0100]
6. Killer effect of Keynote. ↦ Sorted vectors = sorted lists + vectors [HQ]    [2011-07-16 19:43:02 +0100]  [ 3 人說讚！]
   • 曾** ⇒ Magic Move!    [2011-07-16 20:07:51 +0100]
   • L************** ⇒ Cool!    [2011-07-16 21:00:12 +0100]
7. Kant's justification of faith (or the lack thereof) is comparable to the introduction of extensional substitution in observational type theory..    [2011-07-17 21:27:48 +0100]
8. 谷歌翻譯可以正確翻譯「傑瑞米長臂猿」耶 XD。    [2011-07-18 16:52:53 +0100]  [ 2 人說讚！]
9. "Haskell Curry (1900-1982): He worked in combinatory logic. There is a programming logic named after his first name! (see here). Sane!"
   
   ... "programming logic?" Interesting choice of term.. ↦ Computational Complexity: Disproving the Myth that many early logicians were a few axioms short of a    [2011-07-18 19:58:56 +0100]  [ 1 人說讚！]
10. The word "reify" does not appear in LDOCE (and spell checker)! Oxford dictionary includes it, though, and says it originated in mid 19th century — no wonder!    [2011-07-19 09:33:35 +0100]
11. Hmm.. Ornament composition is not yet a pushout in the present ornament language. Permutations of fields need to be taken into consideration. That can be messy...    [2011-07-19 19:37:58 +0100]
12. I dare not use the title "One more thing"...    [2011-07-19 21:36:49 +0100]
    • Josh Ko ⇒ But it's tempting!    [2011-07-19 21:38:44 +0100]
13. Fitting the third paragraph of the discussion section as the special slides for DTP. (For WGP it would be... datatype-generic implementation details?! Er.. will think about that later.)    [2011-07-19 22:34:58 +0100]
14. Great! I believe I have an adequate set of slides now. The remaining work is to make sure I can give a good performance. (The control of timing and expressions is less demanding than that required for performing a piano piece, but the principles are similar, I think.)    [2011-07-19 23:55:24 +0100]
15. Title page. ↦ Wall Photos    [2011-07-20 00:18:31 +0100]  [ 4 人說讚！]
    • Y********** ⇒ 右上角那個好俏皮呀 XDD    [2011-07-20 08:27:51 +0100]
    • Josh Ko ⇒ 旋轉 10 度，效果就不一樣 XD。
      （另外，擺那個是要提示聽眾有 paper 可以看。）    [2011-07-20 08:42:51 +0100]
16. Read a bit more fibred category theory, waiting for the installation of Lion to complete.    [2011-07-20 14:17:42 +0100]  [ 2 人說讚！]
    • Josh Ko ⇒ It was estimated to take 33 minutes.    [2011-07-20 14:20:52 +0100]
    • Josh Ko ⇒ In Lion!    [2011-07-20 14:38:08 +0100]
    • Josh Ko ⇒ It can take some time to get used to the opposite scrolling direction and different gestures.    [2011-07-20 14:50:29 +0100]
17. The UI design of the new OS X is not (yet) perfect this time... (Leopard was a success.)    [2011-07-20 18:47:24 +0100]
    • Josh Ko ⇒ Integration of the UI of Keynote into Lion is particularly crappy.    [2011-07-20 18:56:29 +0100]
18. TeXShop for Lion, supporting Resume, Auto Saving (and Versioning), and Full Screen Mode! ↦ TeXShop    [2011-07-21 14:42:04 +0100]  [ 1 人說讚！]
    • L********* ⇒ How's OpenVanilla? Will it work in Lion?    [2011-07-21 15:02:21 +0100]
    • Josh Ko ⇒ I use the built-in input method. XD    [2011-07-21 15:03:26 +0100]
    • L********* ⇒ But, I don't like it! XD
      I still remember that I trying to use simplified chinese IM on Lion DP2 version few month ago...    [2011-07-21 15:11:07 +0100]
19. 這隻 King J-Der 也太夢幻！要是可以變型就真的是極品了啊。（轉自 ptt BraveSaga 板 #1E86XoUK） ↦ http://www.amiami.jp/blog/2011/07/fes_01cgk/11.jpg    [2011-07-21 21:01:52 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ 不過網上有人指出如果為了變型而照原比例做的話看起來滿慘的⋯    [2011-07-21 21:04:27 +0100]
    • Josh Ko ⇒ http://tieba.baidu.com/f?kz=325206746    [2011-07-21 21:07:14 +0100]
20. Developing my "interpretation" of the slides.    [2011-07-21 23:03:25 +0100]
21. 30 + 4 slides for a 25-minute talk, the additional four slides being special slides for DTP, which might not fit into the talk due to the time limit, however. 30 slides, then, which seems to be a reasonable number, taking into account that a few of them are transitional. Will know more exactly how much time is needed after I rehearse the presentation.    [2011-07-22 00:06:58 +0100]
22. I will go to this one. ↦ Stephen Hough and Oxford Philomusica | Oxford Philomusica    [2011-07-23 23:00:59 +0100]  [ 1 人說讚！]
23. I think I did better than I had expected as a demonstrator for the first time (for the UNIQ summer school). (Three days to go.) ↦ UNIQ summer schools at Oxford - University of Oxford    [2011-07-25 18:59:30 +0100]  [ 3 人說讚！]
24. ICFP is expensive...    [2011-07-25 19:12:35 +0100]
    • Josh Ko ⇒ About £360 for ICFP, WGP, and Haskell Symposium (student price).    [2011-07-25 19:13:28 +0100]
    • J********** ⇒ ㄑ, 還好啦 我去 QSIC ㄉ註冊費要 £485 ㄉ說    [2011-07-25 19:14:44 +0100]
    • J********** ⇒ 當然 沒 funding 就另一個故事ㄌ    [2011-07-25 19:15:29 +0100]
    • L************** ⇒ CALCO costs over £500 ...    [2011-07-25 19:16:48 +0100]
    • Josh Ko ⇒ I had better keep all the receipts very carefully..    [2011-07-25 19:18:30 +0100]
    • L************** ⇒ I think the school can pay them directly...    [2011-07-25 19:19:42 +0100]
    • Josh Ko ⇒ It doesn't seem to be easier, though.    [2011-07-25 19:27:22 +0100]
25. Visa exemption! It's great to be a citizen of Taiwan.    [2011-07-25 19:31:48 +0100]
26. Second day. The part in my brain that handles English didn't work quite well in the morning, but it became normal in the afternoon. Dealt with a lot of parsing errors - teaching syntax *is* important..    [2011-07-26 18:11:49 +0100]
27. Fire alarm at 6 in the morning. Whoever forgot about his/her toast didn't (dare to?) show up.    [2011-07-27 06:19:03 +0100]
28. Jeremy is now Professor Gibbons!!!    [2011-07-27 16:39:33 +0100]  [ 3 人說讚！]
    • T************** ⇒ 手很長    [2011-07-28 07:02:33 +0100]
    • Josh Ko ⇒ 很好。    [2011-07-28 08:16:31 +0100]
29. Practised the presentation again. Cannot believe I could do it so badly..    [2011-07-27 21:55:39 +0100]  [ 1 人說讚！]
    • J********** ⇒ Wanna present it to me tmw?    [2011-07-27 22:36:42 +0100]
    • Josh Ko ⇒ Thanks, but tomorrow is definitely too soon - I need more practice!    [2011-07-27 22:47:36 +0100]
    • J********** ⇒ That's exactly the point though, cuz if you keep practicing in the same manner, the same shortcomings, if any, would stay... but certainly no pressure, let me know if feel like~~    [2011-07-27 22:49:40 +0100]
    • Josh Ko ⇒ You're right, but now I cannot satisfy even myself - it might be said that the presentation is still in an early draft form, so it's just premature to ask for comments from others.    [2011-07-27 23:02:49 +0100]
    • Josh Ko ⇒ More precisely: I am still thinking about what to say and how to say them..    [2011-07-27 23:05:24 +0100]
    • J********** ⇒ cool... my offer is upon your request~    [2011-07-27 23:18:26 +0100]
30. Managed to see one kid cracking the Caesar cipher and another cracking RSA.    [2011-07-28 18:36:26 +0100]
    • Josh Ko ⇒ However, I think some of them suffered from my non-proficient English..    [2011-07-28 18:41:39 +0100]
31. MS (Research) now does dependent types. ↦ Fstar: Secure Distributed Programming with Value-Dependent Types - Microsoft Research    [2011-07-28 21:56:21 +0100]
32. 那時候做白色版社會司中辦團體服的設計理念是不要太顯眼，結果到牛津這裡已經被問好多次那塊 QR code 的內容是啥⋯（用英文寫「社會司中辦」到這裡也變成很自然看得懂的字⋯）    [2011-07-29 19:34:08 +0100]  [ 1 人說讚！]
33. The phenomenon Jackie is experiencing. ↦ PHD Comic: The Repulsor Field Explained    [2011-07-29 20:09:20 +0100]  [ 2 人說讚！]
    • J********** ⇒ What the hell is wrong with Jackie?    [2011-07-29 20:10:11 +0100]
    • Josh Ko ⇒ Nothing: It's a natural phenomenon, as explained by the comics!    [2011-07-29 20:12:34 +0100]
    • J********** ⇒ 傑瑞米, 千萬不能跟吉姆講這件事ㄡ!!    [2011-07-29 22:31:02 +0100]
34. Oxford has appeared on the screening list! ↦ The PHD Movie!    [2011-07-29 20:50:16 +0100]
35. Wow, this is very democratic... "all participants are given 5 minutes for a quick “advertisement” of their proposed talk in the morning of 14th Sep. Participants then vote for talks they would like to listen to, and the programme is scheduled accordingly." ↦ Dependently Typed Programming    [2011-07-29 22:41:31 +0100]  [ 1 人說讚！]
    • Josh Ko ⇒ And there are lots of familiar names.. I suppose they will stay for ICFP too? (Thrilling.)    [2011-07-29 22:46:20 +0100]
    • Josh Ko ⇒ Shonan 是湘南；湘北比較有名吧？XD    [2011-07-29 22:57:46 +0100]

--
Updated the extraction program so the "like" counts are restored.