2009/05/27

Warmed up

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

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

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

Labels:

Blogger anfranion5/27/2009 5:03 pm 說:

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

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

今天辛苦學長了~

 
Anonymous hcsoso5/27/2009 5:08 pm 說:

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

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

 
Blogger Josh Ko5/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 scm5/28/2009 5:18 am 說:

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

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

 
Blogger anfranion5/28/2009 12:57 pm 說:

噢噢

是58號同學
有PTT2個板 Will_lab ~

 

<< 回到主頁