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

Course Outline
School	School of Informatics	College	College of Science and Engineering
Credit level (Normal year taken)	SCQF Level 11 (Year 4 Undergraduate)	Availability	Available to all students
SCQF Credits	10	ECTS Credits	5
Summary	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 what 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. PLEASE NOTE - THIS COURSE HAS REPLACED Types and Semantics for Programming Languages (INFR10040)
Course description	Inductive definitions and proof by induction 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. Principles of operational semantics. *Key concepts of semantics: compositionality, adequacy, observational equivalence, full abstraction, and definability. Relevant QAA Computing Curriculum Sections: Comparative Programming Languages, Compilers and Syntax Directed Tools, Programming Fundamentals, Theoretical Computing

Entry Requirements (not applicable to Visiting Students)
Pre-requisites	It is RECOMMENDED that students have passed Compiling Techniques (INFR10053) OR Compiling Techniques (INFR10065)	Co-requisites	It is RECOMMENDED that students also take Advances in Programming Languages (INFR11101)
Prohibited Combinations		Other requirements	This course is open to all Informatics students including those on joint degrees. For external students where this course is not listed in your DPT, please seek special permission from the course organiser. Some mathematical aptitude is also expected.

Information for Visiting Students
Pre-requisites	None
High Demand Course?	Yes

Course Delivery Information

Academic year 2017/18, Available to all students (SV1)		Quota: None
Course Start	Semester 1
Timetable	Timetable
Learning and Teaching activities (Further Info)	Total Hours: 100 ( Lecture Hours 20, Seminar/Tutorial Hours 20, Summative Assessment Hours 2, Programme Level Learning and Teaching Hours 2, Directed Learning and Independent Learning Hours 56 )
Assessment (Further Info)	Written Exam 0 %, Coursework 25 %, Practical Exam 75 %
Additional Information (Assessment)	Short 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.
Feedback	Not entered
Exam Information
Exam Diet	Paper Name		Hours & Minutes
Main Exam Diet S2 (April/May)			2:00

Academic year 2017/18, Part-year visiting students only (VV1)		Quota: None
Course Start	Semester 1
Timetable	Timetable
Learning and Teaching activities (Further Info)	Total Hours: 100 ( Lecture Hours 20, Seminar/Tutorial Hours 20, Summative Assessment Hours 2, Programme Level Learning and Teaching Hours 2, Directed Learning and Independent Learning Hours 56 )
Assessment (Further Info)	Written Exam 0 %, Coursework 25 %, Practical Exam 75 %
Additional Information (Assessment)	Short 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.
Feedback	Not entered
Exam Information
Exam Diet	Paper Name		Hours & Minutes
Main Exam Diet S1 (December)			2:00

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.Read a formal semantics for a small programming language written in operational denotational style, interpret it in informal terms, and predict how a given program will behave according to the semantic denition. 5.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 6.Be able to write inductive definitions and prove properties of them using induction.