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

This course uses Haskell as a tool to provide an overview of some of the essential knowledge related to function programming in order to bridge the gap with other courses. Starting with structural induction, we will talk about data structures and the inductive definition of functions, and discover that the definition of a function can follow the definition of a data structure. If you want to prove the properties of a function, you can use induction, and the proof will follow the definition of the function. We then turn to the notion of fold, which we find can be regarded as an abstraction of structural induction. Finally, the red-black tree will be used as an example of programming and inductive proofs, in preparation for the subsequent course on dependent types.

#### Taught by

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.

#### Taught by

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.

#### Taught by

Liang-Ting Chen
Institute of Information Science, Academia Sinica

### Dependently Typed Programming

The expressiveness of dependent types far exceeds that of type systems in mainstream languages, so that properties that would otherwise need to be proved additionally can be written directly as dependent types. As we provide more information to the type checker through the dependent type, the latter can in turn tell us what is known and what is yet to be satisfied, and write the correct program interactively. Mathematical theorems and proofs, when expressed in the language of the dependent type, not only ensure that the inference is correct, but also that it is computationally meaningful. Here mathematics, logic and computation become one, forming a solid basis for the design of a new generation of programming languages.

#### Taught by

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

#### Taught by

Chung‑Chieh Shan
Department of Computer Science, Indiana University