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.