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