Types and Semantics for Programming Languages (U04425)

? Credit Points : 10 ? SCQF Level : 10 ? Acronym : INF-4-TSPL

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.

Entry Requirements

? Pre-requisites : Language Semantics and Implementation is strongly recommended; Compiling Techniques and/or Functional Programming and Specification would also be an advantage. Successful completion of Year 3 of an Informatics Single or Combined Honours Degree, or equivalent by permission of the School. Some mathematical aptitude is also expected.

? Co-requisites : A recommended companion course is Advances in Programming Languages.

Subject Areas

Home subject area

Computer Science, (School of Informatics, Schedule O)

Delivery Information

? Normal year taken : 4th year

? Delivery Period : Not being delivered

? Contact Teaching Time : 2 hour(s) per week for 10 weeks

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.