Undergraduate Course: Types and Semantics for Programming Languages (INFR10040)
Course Outline
| School |
School of Informatics |
College |
College of Science and Engineering |
| Course type |
Standard |
Availability |
Available to all students |
| Credit level (Normal year taken) |
SCQF Level 10 (Year 4 Undergraduate) |
Credits |
10 |
| Home subject area |
Informatics |
Other subject area |
None |
| Course website |
http://www.inf.ed.ac.uk/teaching/courses/tspl |
|
|
| Course description |
Type systems and semantics are mathematical tools for precisely describing aspects of programming language. A type system imposes constraints on legal programs in order to guarantee their safe execution, whilst a semantics specifies how a program will do when executed. This course gives an introduction to the main ideas and methods of type systems and semantics. This enables a deeper understanding of existing programming languages, as well as the ability to design and specify new language features. |
Course Delivery Information
Summary of Intended Learning Outcomes
1 - Read and understand the presentation of operational semantics and type systems via inference rules for lambda calculus, and be able to modify such a presentation to include a new language feature, such as state and exceptions.
2 - State and prove the theorems that relate big-step and small-step semantics, and the preservation and progress theorems that link operational semantics and type systems.
3 - Exploit the connection between logic and type systems, where propositions correspond to types and proofs correspond to programs; understand how conjunction corresponds to products, disjunction to sums, and implication to functions.
4 - Explain the differences between informal and formal semantics of programming languages, and between the operational, denotational and axiomatic approaches to formal semantics.
5 - Read a formal semantics for a small programming language written in operational or denotational style, interpret it in informal terms, and predict how a given program will behave according to the semantic definition.
6 - Write a formal semantics for a programming language in the operational style, given a careful informal description of the language, and explain how any inadequacies in the informal description have been addressed in the formal one. |
Assessment Information
Written Examination 75
Assessed Assignments 25
Oral Presentations 0
Assessment
Short handwritten exercises each week.
If delivered in semester 1, this course will have an option for semester 1 only visiting undergraduate students, providing assessment prior to the end of the calendar year. |
| Please see Visiting Student Prospectus website for Visiting Student Assessment information |
Special Arrangements
| Not entered |
Contacts
| Course organiser |
Dr Amos Storkey
Tel: (0131 6)51 1208
Email: A.Storkey@ed.ac.uk |
Course secretary |
Miss Kate Weston
Tel: (0131 6)50 2701
Email: Kate.Weston@ed.ac.uk |
|
copyright 2010 The University of Edinburgh -
1 September 2010 6:10 am
|
University Homepage