TYPE SYSTEMS
Postgraduate level course at ICEX-UFMG
Prof: Carlos
Camarão de Figueiredo
Click here for a Portuguese
version of this page
Course Program:
- Introduction to First-order logic
- Introduction to the Lambda-calculus : syntax, notational conventions, free and bound variables, conversion rules, equality, extensionality, substitution. Representing things in the lambda-calculus: truth-values, pairs and tuples, recursion, recursive functions.
- Type Systems : Introduction (purposes of typing), Typed
lambda-calculus, type rules, second-order typed
lambda-calculus, polymorphic typed lambda-calculus.
Who should attend:
You should attend this course if you have an interest in one or more
of the following:
- study of fundamental questions of computation and computing
science
- design of programming languages
- syntax and semantics of languages
- functional programming
Why you will like this course:
- The course is easy; the course material intends
to make the subjects fun and enjoyable
- The topics are of utmost importance for distinguished students
- The course will give you valuable information if you are
interested in doing a thesis involving some topics
related to one of the areas mentioned above
- Evaluation will not give priority to exams but to
seminars and exercises by the students
- Students will have class time available for reading, thinking,
discussing and preparing exercises and seminars
Bibliography:
- For the first part of the course: Coming soon...
- The lectures on the second part of the course (on introduction to
lambda-calculus) will be based on:
Introduction to Functional Programming
Mike Gordon
Lecture notes and set of transparencies, Cambridge, UK, 1996.
The set of transparencies is thus available there!
Other material to be used on this part of the course:
- Chapter 2 of:
Type Theory and Functional Programming
Simon Thompson (University of Kent at Canterbury)
Addison-Wesley, 1991.
- Chapter 1 of:
The Implementation of Functional Programming Languages
Simon Peyton Jones (University of Glasgow, Scotland)
Prentice Hall, 1987.
These books are available in the department library.
- The third part of the course will be based on:
An Introduction to Polymorphic Lambda Calculus with Subtyping
Kim Mens, Technical report, Vrije Universiteit Brussel, 1994.
This is available frow the WWW.
Other material to be used on this part of the course:
- The article:
Type Systems
Luca Cardelli (DEC/SRC), 1996.
This is available from the WWW.
- The article:
Type Systems for Programming Languages
John Mitchell (Stanford University)
in Handbook of Theoretical Computer Science, The MIT
Press/Elsevier, 1990.
This is available in the department library.
Evaluation:
- Each student will participate in two seminars, of 20 points
each. Each seminar will be given by a group of
students. The subject of the first seminar is
lambda-calculus: one group will base its seminar on
Simon Thompson's book and the other on Peyton Jones's
book.
- Each student will make some lists of exercises, making up a total
of 30 points.
- Each student will make two exams, of 15 points each.