2009/05/27

Warmed up

今晚的 AoPA "talk" 發展完全出我意料之外，台下發問踴躍，以致於光只是當作前導的十頁暖身投影片就已經花掉一個小時。休息一下之後聽眾的興趣轉移到 Agda 身上，demo 又花掉一個小時。於是投影片還停在 "switching to relations" 的第一頁，時間就用完了，嚴格來說根本沒進入正題 XD。

我覺得期末大家都忙翻了，應該不太可能續攤吧。也罷，那就留給 scm 老師講吧 XD。

--
和當初準備的方向相比是完全偏開了 XD。

Labels:

posted by Josh Ko @ 2:43 pm   5 項意見

Blogger Nan 在 5/27/2009 5:03 pm 說：

今天見識到有趣的東西(雖然好難XD)
還挺開心的

謝謝學長一直讓我們問好多問題!
(雖然我的問題都很XD)

今天辛苦學長了~

 
Anonymous hcsoso 在 5/27/2009 5:08 pm 說：

哈哈，其實雖然講的不多，
但是只要讓大家對它感到有趣，感到漂亮，
我想份量上這樣試相當足夠的~~
你的那個內容我想對我這種聽眾來說，
應該是一學期的課程(笑)
也許有一些基礎之後，看後面的東西才感受的到它們的美...
(我剛剛偷翻了一下relation的部份，那是你們那篇paper的contribution嗎？還是都其實還在簡介而已...)

本日最大收穫：
Types are propositions,
and programs are proofs!

 
Blogger Josh Ko 在 5/27/2009 5:28 pm 說：

to anfranion: 台下的問題最能讓講者振奮了。以後有空可以關心一下 FP 喔 :P 。

P.S. 今天和你一起來的是誰呀？忘了問…

to hcsoso: 或許我還是太貪心了，總是希望儘可能多講一些東西。我打的如意算盤是儘可能略過細節，沒想到大家對細節這麼有興趣。更跌破我眼鏡的是大家竟然對 Agda 這麼有興趣，我本來的預期是 derivation 為主、附帶推銷 Agda 的 XD。

我們的 paper 主要是從 "Formalisation in Agda" 開始的，activity-selection problem 是其中一個例子。

沒錯！Curry-Howard correspondence！這是我亟欲傳達的大重點之一！我的希望是可以促進資訊系和數學系之間的交流啦，特別是希望資訊系可以一堆人跑去修高微代導之類的 :P 。

 
Anonymous scm 在 5/28/2009 5:18 am 說：

感覺很不錯唷，能引起大家的興趣就很棒了。多謝啦！

To hcsoso: 那段應該是簡介已經有的概念而已... 由於這個paper 要顧及兩邊（program derivation and type theory）的讀者，所以兩方面的簡介都要做...

 
Blogger Nan 在 5/28/2009 12:57 pm 說：

噢噢

是58號同學
有PTT2個板 Will_lab ~

 

<< 回到主頁