## Announcements

• 03/10 - 網站上線
• 06/08 - 報名開始
• 07/22 - 發出非台大學生修課錄取／未錄取通知
• 07/27 - 發出台大學生修課錄取／未錄取通知
• 07/28 - 發出旁聽錄取／未錄取通知
• 07/28 - 更改上課地點為臺灣大學新生教學館 202 教室

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

#### Lecturer(s)

Shin‑Cheng Mu
Institute of Information Science, Academia Sinica

### 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.

#### Lecturer(s)

Josh Ko
Institute of Information Science, Academia Sinica

### λ-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.

#### Lecturer(s)

Liang‑Ting Chen
Institute of Information Science, Academia Sinica

### Dependently Typed Programming

#### Lecturer(s)

Shin‑Cheng Mu
Institute of Information Science, Academia Sinica
Josh Ko
Institute of Information Science, Academia Sinica
Liang‑Ting Chen
Institute of Information Science, Academia Sinica

### Special Topic: Monad and Side Effects

#### Lecturer(s)

Chung‑Chieh Shan
Department of Computer Science, Indiana University

## 課表

1st week Mon Tue Wed Thu Fri
Morning Functional Programming 0Inductive definitions Functional Programming 1Folds λ-Calculus 0Untyped λ-Calculus λ-Calculus 1Simply typed λ-Calculus λ-Calculus 2Polymorphic λ-Calculus
Afternoon Logic 0Propositional logic & natural deduction Logic 1Classical semantics of propositional logic Functional Programming 2Red-black trees Logic 2Curry–Howard correspondence 討論Discussion
2nd week Mon Tue Wed Thu Fri
Morning Special Topic: Monad and Side Effects 0Dualism: Pure programming with effects, monad, type classes Special Topic: Monad and Side Effects 1Choices: Nondeterministic search & lazy sharing, parsing, probabability Special Topic: Monad and Side Effects 2AI: Gradient descent, automatic differentiation, equational reasoning Special Topic: Monad and Side Effects 3Optional topics 考試Exam
Afternoon 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