Information on the specialist area Programming Languages: Foundations, Implementation and Verification.
Tom Ball and Benjamin Zorn of Microsoft Research recently argued that "industry is ready and waiting for more graduates educated in the principles of programming languages." (http://dl.acm.org/citation.cfm?doid=2663342). Programming languages are the means by which programmers communicate their intent to computers, and to each other. The field of programming languages connects theory with practice: for example, to implement a realistic compiler requires pragmatically realizing automata constructions, parsers, rewriting, and solving NP-complete problems such as graph colouring. Formal program verification draws on logic, type theory and efficient algorithms for symbolic model checking. Yet the discipline of programming languages remains firmly practical, relying on implementability and efficiency as key goals. Advances in programming languages, in the form of better compilers, cleaner programming abstractions, and smarter static analyses and verification techniques, have already had a dramatic impact on practice and offer the potential for major future gains.
The School of Informatics has an international reputation in all three of these areas, and researchers at Edinburgh have made many contributions to logic programming, functional programming, types, interactive theorem proving, model-checking, and parallel programming. The MSc specialist area in Programming Languages includes advanced courses across this range taught by leading researchers in the field, and students undertaking this program will be in an excellent position either to work in industry or pursue PhD study. Students interested in this specialist area would typically take at least 30 credits from among the "core courses" and at least 50 overall from this list.
|Semester 1||Semester 2|
|Core Courses (see notes below)|
Automated Reasoning (level 9)
Compiling Techniques (20 credits, level 10)
Elements of Programming Languages (level 10)
|Optional Courses (see notes below)|
Introduction to Theoretical Computer Science (level 10)
The level 10 core courses "Compiling Techniques" and "Elements of Programming Languages" and the level 9 core course "Automated Reasoning" cover relevant topics at an undergraduate level. Students in this specialist area are encouraged to take at most one or two of these (to fill any gaps not covered in their undergraduate degree) as first semester core courses.
Students strongly interested in compilers and language implementation might also take "Compiler Optimisation" or "Parallel Programming Languages and Systems". "Compiling Techniques" is recommended if a similar course has not already been taken.
Students who are interested in theory or foundations of programming languages might also take "Types and Semantics for Programming Languages" or "Categories and Quantum Informatics". "Elements of Programming Languages" or "Introduction to Theoretical Computer Science" are recommended if a similar course has not already been taken.
Students interested in logic and program verification are encouraged to take "Formal Verification" and "Types and Semantics for Programming Languages". "Automated Reasoning" is recommended if a similar course has not already been taken.
There is no need to focus exclusively on one of these three topics.
The courses "Extreme Computing" and "Secure Programming" involve applications of programming language ideas to some extent in settings such as cloud computing and security.
Most of the courses will assume a good command of the material in the first two (English or European three-year bachelor's) or three (Scottish or American bachelor's) years of a computer science degree. If you don't have this, then don't worry too much: as long as you have good foundation in programming and familiarity with relevant theory (such as languages and automata), most PL courses can be done, though it will be harder work, as you'll have to learn many new concepts. A good place to check your knowledge is to look through the syllabi of our second year courses Informatics 2A and 2B (and 2D for AI and computer reasoning); if you're not certain that you know most of this, then use the course slides (publicly available) and recommended texts to catch up. Some courses, such as "Types and Semantics for Programming Languages" and "Categories and Quantum Informatics", require a solid grasp of mathematical concepts; check their course descriptors and web pages for more details.