課程介紹

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

公告事項

特別講題：依值型別編程

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

程式不可能寫錯

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

寫程式不再孤單

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

數學定理也能跑

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

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

重要日期

  1. 07/26
    外地實習生報名截止
  2. 07/29
    非台大學生報名截止
  3. 07/30
    非台大學生錄取通知
  4. 08/03
    台大學生報名截止
  5. 08/04
    旁聽報名截止
  6. 08/05
    旁聽與台大學生錄取通知
  7. 08/10
    課程開始
  8. 08/20
    課程結束
  9. 08/21
    考試

課程

函數編程

講師

穆信成
中央研究院資訊科學所

教學資源

講義
原始檔
練習解答
考試範圍
  • 講義 Section 0 & 1, Practical 1. 不包括 Section 2: Program Derivation 與 Practical 2.

邏輯

講師

柯向上
中央研究院資訊科學所

教學資源

投影片
考試範圍
  • 投影片全部

程式語言導論

講師

陳亮廷
中央研究院資訊科學所
游書泓
Department of Computer Science, Northwestern University

教學資源

投影片
補充資料
習題解答
考試範圍
  • PLT 1: 全部 PLT 2: 全部 PLT 3: P1-15

依值型別編程

講師

穆信成
中央研究院資訊科學所
科向上
中央研究院資訊科學所
陳亮廷
中央研究院資訊科學所

教學資源

Agda 安裝指南
原始檔
其他
考試範圍
  • DTP Part 1 (Logic.agda) 到 equality predicate 前面（不含 equality）

特別演講 — 驗證真實世界的系統

案例討論：快閃轉換層的形式化驗證

形式化驗證是透過數理邏輯來對程式正確性進行推論的一套方法。由於這套方法通常被認為不易實現且需大量人力，因此也被認為只適用於小型程式或是與生命攸關的系統。然而，隨著理論與工具的發展，許多像是編譯器和作業系統這類我們在日常生活中會接觸的系統，都在最近這十年內成功地被驗證。在這演講的前半段，我會先討論怎麼樣算是一個「正確的程式」，再介紹一些驗證的技術，最後以示範驗證一個小程式作結。演講的後半段，我會分享在中研院進行形式化驗證的經驗：我們驗證了位於許多固態硬碟內部，一個叫作快閃轉換層的核心軟體元件。內容將包括它的形式規格、斷電的行為模型、我們採用的驗證方法以及驗證時遇到的挑戰。

主講人

張耘盛
中央研究院資訊科學研究所

投影片

下載

課表

第一週 星期一 星期二 星期三 星期四 星期五
上午 程式語言導論 0Introduction 邏輯 0Natural deduction and intuitionistic propositional logic 函數編程 1Functional program derivation 邏輯 1Classical semantics and meta-theoretic properties 函數編程 2TBA
下午 函數編程 0Inductive functions and equational reasoning 程式語言導論 1Untyped λ-calculus 程式語言導論 2Simply typed λ-calculus 程式語言導論 3Imperative language constructs 程式語言導論 4What's out there / Agda Installation
第二週 星期一 星期二 星期三 星期四 星期五
上午 依值型別編程 0Agda basics 依值型別編程 1Shallow and deep embeddings of intuitionistic logic 依值型別編程 2Intrinsic representation of simply typed lambda calculus 依值型別編程 3McBride's razor 考試
下午 邏輯 2Curry–Howard correspondence 程式語言導論 5Polymorphic lambda calculus 程式語言導論 6Hoare logic 特別演講Verification of a Snapshot-Consistent Flash Translation Layer