Types for Logic and Functional Programming

Credits: 10
Level: 3 Semester: 2 Staff: Valeria de Paiva
Prerequisite: familiarity with either Functional programming or Logic (Natural deduction) a big advantage Corequisite: none
Objectives: To provide students with an understanding of the basis of Functional Programming, as well as its connections to logic. This should enable them to pursue work on automated deduction and formal methods verification.
Description: We introduce the untyped lambda-calculus, the simply typed calculus and the ML typing system (let-polymorphism, type inference, principal types). From logic we overview natural deduction and we show the important connection between types and propositions, the Curry-Howard correspondence. Time permitting we also survey some applications of types, e.g. second order (polymorphic) lambda calculus, sub-typing, static type systems for objects.
Delivery: lectures and practical exercises, 2 hours per week Type: Closed
Assessment: 75 % a 2-hour written examination, 25% continuous asssessment
Key Texts L Cardelli: Type Systems (In forthcoming CRC Handbook of Computer Science and Engineering)
L Cardelli: Basic Polymorphic Type Checking (Science of Computer Programming 8, 1987, pp. 147-172)
J R Hindley and J P Seldin: Introduction to Combinators and Lambda Calculus (CUP, 1986)
A. M. Pitts Types lecture notes.

Important !!!

In the session 1996-97 the course was a reading course, given in the Spring Term. In the session 1997-98 the course is being taught together with the second year course SEM230, so look for information under this heading.