大預告 II

Relational derivation 寫完以後，我會再寫一篇 dependent types 簡介，預設觀眾背景仍然是一般的 CS 學生！我會試著從為人熟知的 imperative languages 導入（大概就是 C++/Java 吧，用 C++ template 和 Java generics 做第一層近似），盡量不要找 Agda 出來嚇人 XD。

這兩篇綜合起來，正好就是 scm 老師、Patrik Jansson 和我最近投到 MPC '08 的 paper 內容。同時也算是幫 scm 老師的 research interests 打廣告 ─ 老師很缺人手的樣子 XD。先就非技術面廣告一下：老師人很好（造型很前衛？），入門門檻很低（我主要的基礎是在兩星期裡面學會的），Salary/Work 比值又挺高（對我而言啦…XD），有興趣的人千萬不可錯過！

--
喔，scm 老師剛剛終於現蹤了！消失好幾天還挺恐怖的 XD。（16 小時的時差也很恐怖 XD。）