Introduction

This course will teach elements of programming languages, hoping to cultivate students' ability to reason using formal logic, understand the close relationship between logic, programming languages, and type systems, as well as the role that type systems play in programming languages. To enable students to understand and solve programming problems in a recursive/inductive manner, to use software tools to assist logical reasoning and prove the correctness of programs, and to have the knowledge base to further explore programming language-related fields.

Announcements

Special Lecture

We are honoured to invite Professor Neel Krishnaswami from the University of Cambridge to give a special lecture entitled Programming with Modal Types.

Important dates

  1. 01/26
    網站上線
  2. 02/15
    外地實習生報名開始
  3. 03/15
    外地實習生報名截止
  4. 06/05
    外校學生修課報名截止
  5. 06/09
    台大學生正式報名截止
  6. 06/12
    正式報名錄取回覆截止、台大學生候補報名截止、旁聽報名截止
  7. 06/13
    候補報名錄取回覆截止
  8. 07/01
    課程開始

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

Special Topic:Programming with Modal Types

The celebrated Curry-Howard correspondence establishes a deep correspondence between formal logic and functional programming: logical formulae correspond with types, and the proofs of a formula corresponds with programs of that type. Over the centuries, though, logicians have learned that there is not one single system of logic, but rather that there are many different logical systems. And over the past decades, computer scientists have learned that those logical systems, can in turn offer new insights into programming languages.
One of the most important extensions to traditional logic is modal logic. This extends formal logic to the study of assertions which hold relativelye. For example, it is impossible to say that the statement ``it is raining'' is definitely true or false, because its truth depends on when and where it is asserted. From the point of view of computer science, this suggests that we can extend type systems to go beyond the mere shape of data, to deeper behavioural properties of programs.
This course will study the applications of modal logic to the design of programming languages, starting from how they work type-theoretically and showing how they can be used to organise a wide variety of computational phenomena, ranging from reactive programming, incremental computation, database query languages, and even capability-safe programming.

Taught by

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