Introduction

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

Announcements

特別講題:Monad and Side Effects

Important dates

  1. 03/10
    網站上線
  2. 07/17
    外地實習生報名截止
  3. 07/20
    外校學生修課報名截止
  4. 07/25
    臺大學生報名截止
  5. 07/27
    旁聽報名截止
  6. 08/01
    課程開始
  7. 08/08
    期中停修截止
  8. 08/12
    課程結束

Courses

Functional Programming

講師

Shin-Cheng Mu
中央研究院資訊科學研究所

教學資源

講義
投影片
原始檔
習題
習題解答
補充資料
考試範圍

Logic

Mathematical proofs are built upon valid inference structures; in formal logic, we express these structures with precise and succinct symbols, and study their properties. This course module focuses on the natural deduction system of propositional intuitionistic logic, introduces the basic syntactic and semantic proof methods used in formal logic, and points out the intimate relationship between logic and computation, leading into the topic of dependently typed programming. By studying the inference structures formally, this course module also introduces the necessary proof techniques used in other modules.

講師

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

教學資源

投影片
考試範圍

λ-Calculus

Nowadays many languages such as Haskell and Agda are based on variants of λ-calculus. In this course module, we will investigate λ-calculus and its notions and properties mathematically. For example, we will define computation and computational equivalence; after introducing types, we show how ‘a well-typed program does not go wrong’. Apart from theoretical interests, we also discuss a prevalent language feature —polymorphism— which has been applied to solve the code duplication problem in practice. Continuing into the dependently typed programming module, we will use Agda to implement λ-calculus and prove its properties.

講師

陳亮廷
中央研究院資訊科學研究所

教學資源

投影片
補充資料
習題解答
考試範圍

Dependently Typed Programming

講師

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

教學資源

Agda 安裝指南
Unicode 符號對照表
原始檔
考試範圍

特別講題:Monad and Side Effects

講師

單中杰
Department of Computer Science, Indiana University

教學資源

投影片
習題
  • 習題
    考試範圍

    課表

    第一週 星期一 星期二 星期三 星期四 星期五
    上午 Functional Programming 0Inductive definitions Functional Programming 1Folds λ-Calculus 0Untyped λ-Calculus λ-Calculus 1Simply typed λ-Calculus λ-Calculus 2Polymorphic λ-Calculus
    下午 Logic 0Propositional logic & natural deduction Logic 1Classical semantics of propositional logic Functional Programming 2Red-black trees Logic 2Curry–Howard correspondence 討論Discussion
    第二週 星期一 星期二 星期三 星期四 星期五
    上午 Monad and Side Effects 0Dualism: Pure programming with effects, monad, type classes Monad and Side Effects 1Choices: Nondeterministic search & lazy sharing, parsing, probabability Monad and Side Effects 2AI: Gradient descent, automatic differentiation, equational reasoning Monad and Side Effects 3Optional topics 考試Exam
    下午 Dependently Typed Programming 0Indexed datatypes & dependent pattern matching Dependently Typed Programming 1Shallow embedding of higher-order logic & deep embedding of propositional logic Dependently Typed Programming 2Formalisation of simply typed λ-Calculus 討論Discussion