THE UNIVERSITY of EDINBURGH

DEGREE REGULATIONS & PROGRAMMES OF STUDY 2024/2025

Timetable information in the Course Catalogue may be subject to change.

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

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

Course Outline
SchoolSchool of Informatics CollegeCollege of Science and Engineering
Credit level (Normal year taken)SCQF Level 11 (Year 4 Undergraduate) AvailabilityAvailable to all students
SCQF Credits10 ECTS Credits5
SummaryType systems and semantics are mathematical tools for precisely describing aspects of programming language. A type system imposes constraints on 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. The course also introduces relevant parts of logic and discrete mathematics used to describe types and semantics.
Course description - Inductive definitions and proof by induction
- Products, sums, unit, empty, and implication.
- Intuitionistic and classical logic.
- Universals and existentials.
- Lists and higher-order types.
- Simply-typed lambda calculus. Variable binding.
- Call-by-value and call-by-name.
- Small-step operational semantics.
- Progress and preservation.
- Type inference.
- Untyped lambda calculus.

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 Co-requisites
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-requisitesNone
High Demand Course? Yes
Course Delivery Information
Academic year 2024/25, 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, Programme Level Learning and Teaching Hours 2, Directed Learning and Independent Learning Hours 58 )
Assessment (Further Info) Written Exam 0 %, Coursework 100 %, Practical Exam 0 %
Additional Information (Assessment) Coursework Assignments 80%
Essay 20%
Feedback Not entered
No Exam Information
Learning Outcomes
On completion of this course, the student will be able to:
  1. write inductive definitions and prove properties of them using induction
  2. 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
  3. 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 exceptions
  4. write a formal semantics for a programming language in the operational style, given a careful informal description of the language
  5. state and prove the preservation and progress theorems that link operational semantics and type systems
Reading List
* Philip Wadler, Programming Language Foundations in Agda [Required reading. Available online: plfa.inf.ed.ac.uk]
* Benjamin Pierce, et al, Software Foundations, 2012. [Optional reading. Available online: softwarefoundations.cis.upenn.edu]
Additional Information
Course URL https://opencourse.inf.ed.ac.uk/tspl
Graduate Attributes and Skills Not entered
KeywordsTSPL
Contacts
Course organiserProf Philip Wadler
Tel: (0131 6)50 5174
Email: philip.wadler@ed.ac.uk
Course secretaryMiss Yesica Marco Azorin
Tel: (0131 6)50 5194
Email: ymarcoa@ed.ac.uk
Navigation
Help & Information
Home
Introduction
Glossary
Search DPTs and Courses
Regulations
Regulations
Degree Programmes
Introduction
Browse DPTs
Courses
Introduction
Humanities and Social Science
Science and Engineering
Medicine and Veterinary Medicine
Other Information
Combined Course Timetable
Prospectuses
Important Information