課程介紹

本課程將講授程式語言領域之入門理論與知識,希望培養學生以型式邏輯進行清晰思考的能力,了解邏輯與程式語言、型別系統的密切關係,以及型別系統在程式語言中扮演的角色,使學生能以遞迴/迭構方式理解並解決程式設計問題,能運用軟體工具輔助邏輯推理及證明程式正確性,並具備進一步探索程式語言相關領域的知識基礎。

重要日期
  • 07/26 外地實習生報名截止
  • 07/29 非台大學生報名截止
  • 07/30 非台大學生錄取通知
  • 08/03 台大學生報名截止
  • 08/04 旁聽報名截止
  • 08/05 旁聽與台大學生錄取通知
  • 08/10 課程開始
  • 08/20 課程結束
  • 08/21 考試

特別講題介紹

依值型別編程

本次特別講題將重返中研院資訊所講師群鑽研已久的主題「依值型別編程」(dependently typed programming),接力呈現其各個面向。

程式不可能寫錯

依值型別之表達能力遠超過主流語言的型別系統,一些原先需要另外證明的程式性質可直接編寫為依值型別,程式只要通過型別檢查即可保證性質成立。

寫程式不再孤單

當程式員透過依值型別提供更多資訊給型別檢查器 (type-checker),後者就能反過來隨時告訴程式員當下已知與尚待滿足的條件,互動地寫出正確程式。

數學定理也能跑

依值型別語言的表達能力強到能夠將數學型式化,數學定理與證明在依值型別語言中表達出來後,不僅能保證推論過程正確無誤,還一定具有計算意義。

歡迎一同來體驗數學、邏輯、計算融為一體的舒暢感!

課程與講師
函數編程
穆信成 中研院資訊所
邏輯
柯向上 中研院資訊所
程式語言導論
  • 陳亮廷 中研院資訊所
  • 游書泓 Department of Computer Science, Northwestern University
依值型別編程
  • 穆信成
  • 柯向上
  • 陳亮廷
特別演講
張耘盛 中研院資訊所
課表
第一週 星期一 星期二 星期三 星期四 星期五
上午 T₀ T₁ F₁ L₁ F₂
下午 F₀ L₀ T₂ T₃ T₄
第二週 星期一 星期二 星期三 星期四 星期五
上午 D₀ D₁ D₂ D₃ E
下午 L₂ T₅ T₆ I
  • F: 函數編程
  • L: 邏輯
  • T: 程式語言導論
  • D: 依值型別編程
  • I: 特別演講
  • E: 考試