累

儘管事前盡量多睡了，當場聽完 Jean-Pierre 的演講然後講 AoPA 還是很累，一離開就直奔宿舍，吃個麵包睡到八點。（明天有西洋哲學史期中考…）我覺得講到中間就已經把線索丟掉了，講完一張投影片時完全忘記下一張是什麼（只好偷瞄 presenter display），accessibility 那一段近乎崩潰 XD。（本來想和 Jean-Pierre 的 strong normalisation 交叉對照一下，可是我不會念他的姓 XD。）蔡老師這次開場和結束時修正上次的評語為「就大學生而言」英文流利，我覺得這樣中肯許多 XD。不過他還（友善地）說「背稿有點明顯」，這個讓我比較意外，因為我沒寫稿 XD。（很久以前還試著把一個版本打成 presenter notes 備用，可是打了幾張就不想打了 XD。）或許是事前練習的時候我有幾條鋪陳路線比較熟，所以當場一走到那幾條路上就會比較順利地走一段。像 accessibility 就完全沒走到事先練習的路線上，整個講得支離破碎 XD。總之第一次比較正式的 English presentation 就獻給這個帶點交際意味的小小 seminar 啦。

內容部份：scm 老師果真料事如神，Jean-Pierre 問我有沒有比較過 qsort 在 AoPA 和 Coq 上面的證明（我聽不出來是誰做 Coq 版的…），他覺得有些部份很明顯適合用 Coq 的 tactics 做。我就搬之前在 DTP 一塊吃早餐的那個法國人做的 porting 出來回答啦。（我還是不會念他的姓名…）最後，我似乎太過於強調 sorting，greedy theorem 和 activity-selection 只用一張投影片輕輕帶過，以致於 Jean-Pierre 問我除了 sorting 有沒有做別的問題。（他用 "standard problem" 描述 sorting，不過我猜他心裡想的是 "trivial problem" XD。）解法就是再翻回那張投影片給他看啦。

--
很可惜不能說「下次不玩了」，以後還有更多 XD。