Undergraduate Course: Topics in Programming Languages and Semantics (INFR11302)
Course Outline
| School | School of Informatics |
College | College of Science and Engineering |
| Credit level (Normal year taken) | SCQF Level 11 (Year 4 Undergraduate) |
Availability | Not available to visiting students |
| SCQF Credits | 20 |
ECTS Credits | 10 |
| Summary | This course is intended for those who wish to enter research in programming languages or to be technical experts in their future roles in industry. Each year the course selects topics representative of current research and practice in programming languages and semantics. These topics may include dependent type theory for language semantics and verification, concurrency theory, or type systems and applications to language design.
The course gives a deeper understanding of the principles of programming languages and their design and implementation, building upon other courses covering elementary material such as Elements of Programming Languages (INFR10061) or Introduction to Theoretical Computer Science (INFR10059) by introducing more advanced topics and recent developments in the field. We recommend that students have either taken a general introduction to programming languages either in Edinburgh (such as EPL (INFR10061)) or elsewhere, or have a sufficient background in mathematics or logic to quickly familiarise with this material.
Visiting undergraduate students are eligible to enrol on Topics in Programming Languages and Semantics (UG) (INFR11305). |
| Course description |
The course consists of multiple independent topic tracks (usually three), of which students are expected to attend, and will be assessed on, two of their choice. Each track covers one important direction in programming languages, including its mathematical foundations and relevance to current research and practice.
Although topics may range from mainly theoretical to applied, a working knowledge of mathematical concepts (logic, discrete structures, induction, probability as covered in pre-honours Informatics programmes) and some programming experience are assumed. Familiarity with basic concepts of programming language semantics, type systems, and language implementation techniques is also assumed.
Each track will typically consist of one lecture hour per week, with some variation based on topic. Each track will have a series of formative questions for study, supported by tutorials, a class forum, and some targeted feedback.
The topics vary from year to year, dependent on availability and current research interests of teaching staff (the course website will describe in detail the topics each year). Possible topics include:
- Type theory, dependent types, mechanised reasoning about programming languages and calculi, verification of program correctness, operational and denotational semantics, induction and recursion
- Modelling concurrent systems, formal techniques for reasoning about concurrency, labelled transition systems, notions of equivalence of concurrent systems, bisimulation and coinduction
- Type systems and language design, advanced functional programming, rewriting theory and termination/strong normalization, type inference, applications to for example safe concurrent programming, functional reactive programming, language integrated query, concurrent/reactive programming
- Probabilistic programming and semantics of probabilistic programs using denotational techniques, applications in machine learning, probabilistic modelling, statistics
|
Entry Requirements (not applicable to Visiting Students)
| Pre-requisites |
It is RECOMMENDED that students have passed
Elements of Programming Languages (INFR10061) OR
Introduction to Theoretical Computer Science (INFR10059)
|
Co-requisites | |
| Prohibited Combinations | |
Other requirements | MSc students must register for this course, while Undergraduate students must register for INFR11305 instead.
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.
This course requires practical mathematical application of discrete structures (trees, graphs, induction), logic and symbolic reasoning (inference rules, rewriting systems) and problem solving. For example, topics may require you to define or study the properties of a type system for tracking the ways different variables are used in a program. Some of the required details can be learned during the course, but some familiarity with these mathematical topics (or the ability to quickly acquire it through self study) is required
We assume that students have taken a basic introduction to programming languages, compilers, and/or theoretical computer science. |
Course Delivery Information
|
| Academic year 2026/27, Not available to visiting students (SS1)
|
Quota: None |
| Course Start |
Semester 2 |
Timetable |
Timetable |
| Learning and Teaching activities (Further Info) |
Total Hours:
200
(
Lecture Hours 20,
Seminar/Tutorial Hours 16,
Summative Assessment Hours 2,
Programme Level Learning and Teaching Hours 4,
Directed Learning and Independent Learning Hours
158 )
|
| Assessment (Further Info) |
Written Exam
70 %,
Coursework
30 %,
Practical Exam
0 %
|
| Feedback |
Targeted individual feedback will be provided on some of the formative work provided throughout the materials. Students are expected to engage with the course content in weekly tutorial sessions with teaching assistants, and to discuss any unanswered questions on the class forum. |
| Exam Information |
| Exam Diet |
Paper Name |
Minutes |
|
| Main Exam Diet S2 (April/May) | Topics in Programming Languages and Semantics INFR11302 and INFR11305 | 120 | |
Learning Outcomes
On completion of this course, the student will be able to:
- identify how an aspect of an advanced programming languages topic applies to a given applied problem
- use programming languages techniques to model, reason about, or formally verify properties of a system
- critically compare and contrast alternative choices or variants of methods or approaches in the area
- identify the technical, ethical and societal implications, including both benefits and risks, of different approaches to programming language design and implementation
|
Reading List
Programming language foundations in Agda (Wadler, Kokke)
Practical foundations of programming languages (Harper)
Introduction to Process Algebra (Fokkink) |
Additional Information
| Graduate Attributes and Skills |
Apply critical analysis, evaluation and synthesis to issues, or issues that are informed by forefront developments in the subject / discipline / sector.
Identify, conceptualise, and define new and abstract problems and issues.
Develop original and creative responses to problems and issues.
Critically review, consolidate and extend knowledge, skills, practices and thinking in subject / discipline / sector.
Deal with complex issues and make informed judgements in situations in the absence of complete or consistent data / information. |
| Keywords | Programming languages,Concurrency,Verification,Type theory,Type inference,Semantics |
Contacts
| Course organiser | Dr Ohad Kammar
Tel:
Email: ohad.kammar@ed.ac.uk |
Course secretary | Mr Lachlan Boyd
Tel:
Email: lboyd@ed.ac.uk |
|
|
University Homepage