2011/04/28

[facebook digest] Writing the first first-author paper

  1. Should perhaps explicitly introduce a notation of realisability transformation for functions.    [2011-04-09 18:12:09 +0000]
  2. Arrived at the boarding gate, where the destination shown is still Hong Kong (07:25).    [2011-04-09 23:27:27 +0000]
  3. It is reported that Oxford will be wonderfully warm and sunny - nice!    [2011-04-09 23:31:53 +0000]
  4. 拚死在登機前吃了一客 NT$180 的紅燒牛腩飯套餐。其實不錯，除了牛腩飯以外，附三種小菜、貢丸湯（兩顆）、和一小塊巧克力蛋糕。有到讓我不敢照相的水準（免得日後望圖興嘆）。    [2011-04-10 00:22:31 +0000]
    • 柯** ⇒ 哈！這次回台媽媽叫你練習煮飯你就不要…    [2011-04-10 12:59:32 +0000]
  5. 今天機場比上次熱鬧很多，好幾個航班擠在同一個櫃台報到。    [2011-04-10 00:23:50 +0000]
    • 翁** ⇒ good luck~    [2011-04-10 00:32:07 +0000]
    • W************ ⇒ 一帆風順~    [2011-04-10 13:59:43 +0000]
  6. 登機嘍！    [2011-04-10 00:58:25 +0000]
    • S************ ⇒ Farewell~    [2011-04-10 04:34:35 +0000]
  7. Finally got on the coach, after helping a Taiwanese girl get on a coach to Cambridge. (She's attending a language school and does not speak English very well.)    [2011-04-10 18:25:07 +0000]
  8. Arrived at Oxford. 從海角又飛回天涯。    [2011-04-10 20:03:15 +0000]
  9. Good morning! Spring really has come to Oxford, as the trees are now vibrantly green. (In Taiwan there's no such contrast.)    [2011-04-11 07:39:49 +0000]
    • M*********** ⇒ 沒圖沒真相,照片~~照片~~~~    [2011-04-13 16:24:51 +0000]
    • Josh Ko ⇒ 真相已貼！XD    [2011-04-13 16:37:19 +0000]
  10. The immigration officer really asked for my CAS letter, even when I was entering the UK as a student for the second time. When she said "CAS letter, please", I replied "CAS letter?" and she said "acceptance letter" instead. But I was merely surprised to hear that a CAS letter was still needed. And of course I easily produced the letter, having brought it back to Taiwan.    [2011-04-11 08:11:48 +0000]
    • L********** ⇒ Useful information    [2011-04-11 08:54:31 +0000]
    • L************** ⇒ I have never been asked this ...    [2011-04-11 20:26:50 +0000]
  11. Finally discovered that option + '-' produces an en-dash and shift + option + '-' produces an em-dash. No need to search through the character map anymore!    [2011-04-11 14:34:25 +0000]
  12. The sun hesitating to fall, it is so easy to assume that it is still well in the afternoon while in fact the evening has come!    [2011-04-11 17:15:13 +0000]
  13. Classic FM: 101.3 MHz or www.classicfm.co.uk    [2011-04-12 09:02:54 +0000]
  14. What happened to the kitchen?! Leaving things in this horrible state, it's simply... illogical! And I guess the logical thing to do is to spend some time clean it all up, say tomorrow (allow myself some time to convince myself emotionally)... ↦ http://www.facebook.com/photo.php?fbid=180388995346979&set=a.126799950705884.40277.100001276392360&type=1    [2011-04-12 18:04:12 +0000]
    • J******** ⇒ Dishwasher is your best friend!!    [2011-04-12 22:07:08 +0000]
    • Josh Ko ⇒ No such thing in our kitchen...    [2011-04-13 05:42:41 +0000]
  15. Suddenly realised why it is strange and inconvenient to publish a result heavily based on something which hasn't been published.    [2011-04-13 15:47:16 +0000]
  16. "Silver white winters that melt into springs" - now I know why it's one of her favourite things. ↦ http://www.facebook.com/photo.php?fbid=180612515324627&set=a.126799950705884.40277.100001276392360&type=1    [2011-04-13 16:36:30 +0000]
  17. Hmm... I'd say it's really a paper from the AoP group, with lists, folds, and fold fusion!    [2011-04-14 17:56:16 +0000]
  18. The paper is definitely going to exceed the page limit...    [2011-04-14 19:01:59 +0000]
    • Josh Ko ⇒ Let's forget about fusion?    [2011-04-14 19:02:43 +0000]
    • J********** ⇒ Let's forget about submitting it?    [2011-04-14 19:34:37 +0000]
    • Josh Ko ⇒ No way! ICFP is too tempting!    [2011-04-14 19:38:26 +0000]
    • J************* ⇒ C'est la vie, I'm afraid. Short version for submission, long version with the full story in to go online. TeX conditionals are your friend!    [2011-04-15 00:09:58 +0000]
  19. When can we publish animated papers...?    [2011-04-14 20:01:20 +0000]
    • C*********** ⇒ We graphics guys really need that.    [2011-04-18 00:46:49 +0000]
  20. "The contribution of the realisability transformation, then, is pointing out the connection between the two different ways of expressing constraints --- realisability predicates for externalism and ornaments for internalism.    [2011-04-17 18:43:48 +0000]
    • Josh Ko ⇒ An ornament induces a realisability predicate, which is the manifestation of the ornament in the world of decoded datatypes, and moreover, composition of realisability predicates mirrors composition of ornaments. A bridge is formed between externalism and interalism, and subsequently, externalist modularity is brought into internalist datatypes."    [2011-04-17 18:43:52 +0000]
    • Josh Ko ⇒ A problem I encountered four years ago, now finally having an initial solution.
      http://joshkos.blogspot.com/2007/11/qsort-in-agda-round-4.html    [2011-04-17 18:52:29 +0000]
    • Josh Ko ⇒ It was actually mentioned by Shin in his fifth email to me (in Chinese):「有沒有可能模組化地證明程式的性質。例如我們能設計一個 type 證出 mergesort 之中的那個 merge 函數傳回的 list 長度是對的，也可以設計另一個 type 證出 merge 傳回的 list 是 sort 好的。但如果要同時證兩個性質，又要設計另一個 type. 有沒有可能模組化一點。」    [2011-04-19 20:17:59 +0000]
  21. Writing up and revision of the paper in active progress. It reminds me vividly of how much hard work was required to produce the two AoPA papers, even though I had been just watching and didn't actually do the writing then.    [2011-04-19 20:12:46 +0000]
  22. Tulips or...? ↦ http://www.facebook.com/photo.php?fbid=182721041780441&set=a.126799950705884.40277.100001276392360&type=1    [2011-04-22 10:16:44 +0000]
    • T************** ⇒ 這樣拍看不出來    [2011-04-22 12:37:58 +0000]
  23. The Introduction will be finished tomorrow, which tells a specialised story about finite numbers with parity. (And the maximum page number is expected to reach 12.)    [2011-04-22 22:04:17 +0000]
  24. Just realised that paper writing is really comparable to music composing! (The example of finite numbers with parity appearing in the Introduction and never again reminds me of the first theme in the first movement of Tchaikovsky's first piano concerto.)    [2011-04-23 10:10:42 +0000]
    • Josh Ko ⇒ Cf. Remy: "Compose the salad like you were painting a picture!"    [2011-04-23 10:17:35 +0000]
  25. Making some very subtle points. The points are already hard by themselves, and naturally it is even harder to put them in words clearly!    [2011-04-24 14:23:01 +0000]
    • Josh Ko ⇒ On the other hand, that's what's so interesting about a paper. I hope the reader will find the discussion worth reading.    [2011-04-24 14:24:11 +0000]
  26. "Thus the use of realisability predicates, which is central to externalist compositionality, can in fact be regarded as an application of an internalist technique to solve the compositionality problem of internalist datatypes."    [2011-04-24 15:38:44 +0000]
  27. See if I can have the first complete draft of the paper before May starts.    [2011-04-24 19:39:20 +0000]
  28. $ detex OAOAOO.tex | wc
    1009 9327 56566
    (No, the paper has not been finished...)    [2011-04-25 19:33:47 +0000]
  29. 人事物都在變，很快中興新村就要變得陌生了。 ↦ 中興新村將風華再現開發計畫有條件通過｜地方新聞｜中時電子報    [2011-04-25 21:17:26 +0000]
    • W************ ⇒ 彰中的教室都有冷氣了 ...    [2011-04-26 02:49:40 +0000]
  30. New address from August: 45 Marlborough Road, Oxford, OX1 4LW.    [2011-04-26 15:04:23 +0000]
  31. So nice to be able to reach the Acknowledgements.    [2011-04-26 21:49:59 +0000]
  32. Finally arrived at a draft that counts basically as complete. XD    [2011-04-27 21:23:20 +0000]
    • Josh Ko ⇒ Err... I forgot the abstract. XD    [2011-04-27 21:31:42 +0000]
    • Josh Ko ⇒ It seems to be customary for the abstract to be excerpted from the introduction?    [2011-04-27 21:43:28 +0000]
  33. The abstract produced!    [2011-04-28 10:15:17 +0000]
    • Josh Ko ⇒ Dependently typed programmers are encouraged to use inductive families to integrate constraints with data construction. Different constraints are used in different contexts, which lead to different version of datatypes for the same data structure. How the common operations can be modularly implemented for these structurally similar datatypes has been a longstanding problem. We propose a datatype-generic solution based on McBride's datatype ornaments, exploiting an isomorphism which can be interpreted in terms of realisability. Relevant properties of the operations are separately proven for each constraint, and after the programmer selects several constraints to impose on a basic datatype and synthesises an inductive family incorporating those constraints, the operations can be routinely upgraded to work with the synthesised inductive family.    [2011-04-28 10:15:24 +0000]
  34. Twelve pages!    [2011-04-28 15:13:23 +0000]
    • Josh Ko ⇒ Further tweaking can change that easily, though.    [2011-04-28 15:14:35 +0000]
  35. Global refinement to be done tonight.    [2011-04-28 17:17:06 +0000]
  36. Just gone through the whole paper again. I'll ask Jeremy about some details and then the paper can be finalised!    [2011-04-28 19:18:04 +0000]

Labels:

posted by Josh Ko @ 10:00 pm   0 項意見