Type Theory in Computer Science and Linguistics, a graduate course in Chung-Ang University, Autumn 2003

Bengt Nordström (guest professor from Chalmers University of Technology, Sweden)

Short Description of the course

Type Theory was developed in the 70's by the Swedish mathematician Per Martin-Löf as a foundation for (constructive) mathematics.

From a Computer Science perspective, it is a language in which it is possible to express both specifications and programs within the same formalism. Furthermore, the proof rules can be used to derive a correct program from a specification as well as to verify that a given program has a certain property. As a programming language, type theory is similar to typed functional languages such as ML and Haskell, but a major difference is that the evaluation of a well-typed program always terminates. The type system is using dependent types, a concept which makes it possible to identify programs and formal proofs.

We can use type theory as a framework in which it is possible to express a whole range of logical formalisms.

An important feature of the language is the possibility of using *inductively defined sets*, a concept which is closely related to XML.

The lectures will assume a general background in Computer Science. We will explain the theory and show its applications to programming, document structure (like the semanic web) and linguistics.

We will not assume any knowledge of functional programming, this will be covered in the first weeks. This homepage will be continuosly updated during the term. The schedule will be changed if I find that the students have another background or interest than expected.

Grading policy

The examination of the course is divided equally between assigned homeworks, term paper and a final exam.

Overview of the course (tentative)

General Background
Functional Programming
Lambda Calculus
Polymorhic Type Theory
Monomorhic Type Theory
Applications:
- Programming
- XML
- The Semantic Web
- Linguistics

Sept 4: General Background

Sept 18: Functional Programming 1

You should download a version of Hugs from the Haskell home page. Here is some reading material:

Course on Functional Programming, from University of New South Wales, Australia
Textbook on Functional Programming by Rex Page, University of Oklahoma, USA
Lecture on Functional Programming , a brief introduction to functional programming by John Hughes, Chalmers University, Sweden
Exercises using Hugs , following the above lecture.
Exercises with integers and recursion, lists and recursion, map and filter, simple data types These examples were made by David Sands for an introductory course at Chalmers.

After the first three weeks I will assume that you are familiar with this material.

Homework

Rational numbers. This is to be handed in on the next lecture (Sept 25)

Sept 25: Functional Programming 2

This week is a continuation of the introduction to programming with functional languages.

Homework

Big numbers. This is to be handed in on the next lecture (Oct 2)

Oct 2: Functional Programming 3

This is a continued introduction to functional programming. I will go through parametric and ad hoc polymorphism and the class mechanism in Haskell. Some examples of how to give the type of an expression.

Homework

Turtle graphics has a deadline on ~~October 16.~~ October 23. (you have been given one extra week.) Here you will find a link to a paper by Paul Hudak giving a background. Another very good background is this description of shallow and deep embedding. This is a major programming exercise and you will not have time to do it if you start a week before. You can do this in groups of two persons.

Oct 9: Functional Programming 4

The lecture this week was mainly devoted to the homework about big numbers. If you have problems with English, I suggest that you prepare written questions which you can give to me in the beginning of the class. It is a good language exercise to write something! (This is also why you have to write programs when you learn Haskell.) I hope that the outcome of this course is not only that you learn functional programming and type theory but also that you improve your English.

Oct 16: Functional programming 5

How to deal with side effects. Input and output.

Oct 23: Lambda Calculus 1

We will give an introduction to lambda calculus. This is a minimalistic programming language which was invented around 70 years ago, long before the existence of digital computers. Here is an introduction written by Prakash Panangaden. You can also read an online tutorial written by Chris Barker, University of California, San Diego.

Homework

Lambda calculus. This is to be handed in on the next lecture (Oct 30)

Oct 30: Lambda Calculus 2

This week will be a continuation of the presentation of the lambda calculus. We will also discuss the homework (turtle graphics). I will give some intuitions around monadic programming. It is not as difficult as it may seem! The new deadline (for those of you who did not do it) for handing in the turtle graphics homework is Wednesday noon November 12. You can leave it with JinHee, who is sitting in the room next to me.

Nov 6: Turtle Graphics example

There will be no lecture this week, we had an extra lecture on Oct 23. I suggest that you meet and discuss the homework on turtle graphics. Discuss principles and not concrete programs. I do not want to discover that you have similar programs! Two of you has already implemented it, I hope that you can help the other students.

Nov 13: Polymorphic Type Theory

Reminder for some of you: Can you mail me (to bengt at cs.chalmers.se) the number of points you received on the first homework!

This week's lectures will be an introduction to the polymorphic set theory. It is possible to see it as a simple functional language with dependent types.

Nov 20: Propositions as Types, an introduction

The lectures presented Prawitz' rule for Natural Deduction for constructive propositional logic. It was shown how this could be implemented in Haskell by letting propositions be types and proof rules be functions. Some examples of derivations were given.

Nov 27: Propositions as Types, contd.

Homework

Your task is to implement propositions in constructive propositional logic as types in Haskell. The deadline is Wednesday next week at 3 PM.

Dec 4: Propositions as Types, contd.

The idea of identifying propositions as types seems to be difficult. The lectures this week was a further exploration of this idea.

Dec 18: Applications: XML and Type Theory

This lecture will be discussion about the relationship between XML and type theory. How can XML benefit from a more careful analysis of fundamental concepts like constants, definitions, types, dependent types, etc.

The exam will take place immediately after the lecture.

Good Luck!

Last modified: Wed Dec 17 12:06:39 KST 2003