Asian-Pacific Summer School on Formal Methods

下午剛結束在北京輕學大學的暑期課程之旅,來之前記得最原始 Coq Summer School,但後來叫做 Asian-Pacific Summer School on Formal Methods,顧名思義以正規方法來處理軟體的問題為主,講師們都從法國 INRIA 來。題材前半段集中在 Coq 本身,以及相關的題材,像是 dependent type, inductive type, coinductive type, Curry-Howard isomorphism。後半段則是以互動式定理證明跟自動證明器應用在程式語言的檢驗,像是 why tool , frama-C 能夠用來處理 Objective ML, 甚至是 Java, C 語言的正確性。最後則是說明將來還有哪些問題要處理的。總共 8.5 天,其中一天結束 Coq 的材料,去清華校園隔壁的頤和園逛逛。

整體來說,相當驚人的暑期課程。先從費用來看,學生是 100 人民幣包含了住宿,三餐(儲值80元的餐卡),課本 Coq’Art中文版,Coq Live USB(2GB的USB隨身碟上裝好 Ubuntu 跟 Coq ),一件衣服,完整的 INRIA 師資群。算下來,實際上得到的比 100 還要多很多。

課程方面相當緊湊扎實,我不曉得到底有沒有預設背景知識,但是作業從 functional programming 到定理證明以及用 Hoare logic 描述 insertion sort 並用證明器證明,作業非常多。好在講師全程參與,所以上機實做的課程,敢問都能夠得到不錯的回應。純上課的話,我個人習慣自己念,常常上到打瞌睡就是了,下午實做精神就好多了 … orz.

參加的同學以中國各地為主,有好一些人都是教授老師等級,中科院的來了不少,還有的是教授帶著自己的學生一起來上課,學習相當勤奮啊。另外有三個韓國人,不過沒有聊過,不曉得來歷如何,但是光看外表我想也差不多是教授級了吧 …;台灣來的好像只有我這麼一個,還好都很好相處,比台灣人還熱情(大概跟台灣人對外國人一樣熱情了 …),第二天晚上就有伴了。一直以為自己的社交工程不及格,不過看起來還可以。

語言方面問題比較大,習慣英式美式標準腔調,法國人的腔調不適應,一開始不好進入狀況。原本以為是英文退步,但最後在講 smart card 的應用時,講師的口音比較標準,邊寫程式邊聽都沒問題,顯然是腔調無法適應。這點跟中國學生聊天的時候也一樣,一來用語不大一樣腔調各異,常常也是有聽沒有懂,要一直講才比較好。(但是換個人聊又聽不大懂了 …)

不過教學設備上,個人對於投影機直接投在白色牆面上有些感冒,色彩失真不說,反射面的效果頗差,其實看得不是很清楚,再加上後期到大教室上課,可視角度不變,但是前後距離變遠,反而看得不是很清楚,如果要用電腦坐在兩旁或是後面,或者試用到白板解說,… 位置角度不好完全看不到。

課程本身的規劃設計不錯,連貫性很好,沒有評分壓力比較小,比較能夠享受上課以及解問題的樂趣。但教學方面,如果有以中文為主的助教幫忙學習上的問題,可能會更好,我看滿多人有問題不敢問,相當可惜。中間應該在穿插一整天的休息,有不少人連上了六七天,最後就蹺課去溜達玩玩去了。到後面我也有點疲憊了,每天的作息就是七點多起床,吃早餐,去上課,中午吃飯休息,下午上機寫習題,晚上吃晚餐,回去想下午的問題,然後睡覺,再加上來之前沒日沒夜的趕申請學校的 research proposal ,一連好幾天下來有點疲乏。

最後徵博士生做的問題,不巧都沒啥興趣,一開始看的是 SSReflect 要作 simple group 的分類問題的正規證明,剛好不在這次的徵選範圍之內,再加上 Coq 的語法讓我很痛苦(跟 Agda 比較起來),暫時打消問細節的意願。另外就是 Coq 上發展一套給 rewriting system 驗證 termination proofs 的 library,給其他的 prover 作為基礎。看起來是比較有意思的,跟其中的研究員討論一下留個名片之後,還在看看細節中。

題外話,總覺得應該印個名片一下 …我到這邊來交換個人資料的場合挺多的,每次都寫給別人真怕哪邊寫錯就聯絡不到了 囧。

Advertisements

2 thoughts on “Asian-Pacific Summer School on Formal Methods

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s