Department of Computer Science, Unit Catalogue 2009/10 |
CM30226: Logic and semantics of programming languages |
 Credits:
| 6 |
| Level:
| Honours |
| Period: | Semester 2 |
| Assessment:
| CW25EX75 |
| Supplementary Assessment: | Supplementary assessment information not currently available (this will be added shortly) |
| Requisites:
| Before taking this unit you must take CM20167 or take CM20218 |
| Description: | Aims: To develop a detailed understanding of a body of mathematical theory that is used in the formal conceptual analysis of programming languages. Learning Outcomes: By the end of the unit, successful students will be able to: 1. give the central definitions and theorems of one of the mathematical theories underlying the formal study of programming languages; 2. use a mathematical theory to give a formal description of computational phenomena; 3. evaluate a new mathematical theory that is proposed as providing formal support for computation. Skills: Problem Solving, Communication, Application of Number. Content: * Categories, functors, natural transformations, adjoint functors * Cartesian closed categories with natural numbers object * Interpretation of the simply-typed lambda calculus in a Cartesian closed category * Natural deduction for intuitionistic propositional logic * The Curry-Howard isomorphism, relating natural deduction to the lambda-calculus and hence to CCCs. |