- ARCHIVE for reference only

University Homepage
DRPS Homepage
DRPS Search
DRPS Contact
DRPS : Course Catalogue : School of Informatics : Informatics

Undergraduate Course: Types and Semantics for Programming Languages (INFR10040)

Course Outline
SchoolSchool of Informatics CollegeCollege of Science and Engineering
Course typeStandard AvailabilityAvailable to all students
Credit level (Normal year taken)SCQF Level 10 (Year 4 Undergraduate) Credits10
Home subject areaInformatics Other subject areaNone
Course website Taught in Gaelic?No
Course descriptionType 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 (not applicable to Visiting Students)
Pre-requisites It is RECOMMENDED that students have passed Language Semantics and Implementation (INFR09014) AND Compiling Techniques (INFR09007) AND ( Functional Programming and Specification (Level 9) (INFR09033) OR Functional Programming and Specification (Level 10) (INFR10043))
Co-requisites It is RECOMMENDED that students also take Advances in Programming Languages (INFR10003)
Prohibited Combinations Other requirements 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.
Additional Costs None
Information for Visiting Students
Displayed in Visiting Students Prospectus?No
Course Delivery Information
Not being delivered
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

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.
Special Arrangements
Additional Information
Academic description Not entered
Syllabus Type systems for programming languages
* Untyped and simply-typed lambda calculus. Variable binding.
* Small step and big step semantics.
* Progress and preservation theorems.
* Products, sums, and list types.
* Reference types and exceptions.
* Subtyping. Subsumption and its understanding as inclusion or coercion.

Formal semantics for programming languages
* Principles of operational, denotational and axiomatic semantics.
* Key concepts of semantics: compositionality, adequacy, observational equivalence, full abstraction and definability.
* Case study: operational semantics for a fragment of Java.
* Game semantics as an example of denotational semantics.
* Game semantics for a simple object oriented language.

Relevant QAA Computing Curriculum Sections: Comparative Programming Languages, Compilers and Syntax Directed Tools, Programming Fundamentals, Theoretical Computing
Transferable skills Not entered
Reading list * Benjamin C Pierce, Types and Programming Languages, MIT Press, 2002.
* Benjamin C Pierce, editor, Advanced Topics in Types and Programming Languages, MIT Press, 2005.
* G. Winskel, The Formal Semantics of Programming Languages: an introduction. MIT Press, 1993.
Study Abroad Not entered
Study Pattern Not entered
KeywordsNot entered
Course organiserDr Amos Storkey
Tel: (0131 6)51 1208
Course secretaryMiss Kate Weston
Tel: (0131 6)50 2701
Help & Information
Search DPTs and Courses
Degree Programmes
Browse DPTs
Humanities and Social Science
Science and Engineering
Medicine and Veterinary Medicine
Other Information
Important Information
© Copyright 2011 The University of Edinburgh - 16 January 2012 6:16 am