Special Lecture

FLOLAC 2024 很榮幸邀請到劍橋大學 Neel Krishnaswami 教授擔任特別講師,講題待定。

Important dates

  1. 01/26
  2. 02/15
  3. 03/15


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


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


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


Taught by

Neel Krishnaswami
Department of Computer Science and Technology, University of Cambridge