Formosan Summer School on Logic, Language, and Computation
邏輯、語言與計算暑期研習營, 20247/1-7/12 09:10-12:10, 13:20–16:20
Location：Room 103, Building 1, College of Management, National Taiwan University
邏輯、語言與計算暑期研習營, 2024This 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.
We are honoured to invite Professor Neel Krishnaswami from the University of Cambridge to give a special lecture entitled Programming with Modal Types. The abstract of the topic is as follows:
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 relatively. 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.
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.
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.
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.
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 relatively. 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.