Some of the material and ZOOM links (mostly passcode protected) are provided below for each lesson! We will use D2L and email for communications.
Description of the course
The purpose of the course is to study the principles behind the definition, design and implementation of a programming language and of the tools that provide software correctness. Its goals are to build an ability to evaluate and compare programming languages, to master the theoretical and practical aspects of programming language design and implementation, both from the user's and implementor's view, and to develop precise mechanisms for specifying the semantics of programming languages. Specific topics include: order theory, inductive definitions, operational and denotational semantics, type systems, the design of an interpreter, properties of programs, logics of programs, principles of program analysis and verification, and abstract interpretation.
Students who complete this course will be familiar with design and implementation of a programming language, with particular emphasis in the definition of its semantics, in understanding properties of programs and their constructs, and in the design and implementation of tools for verifying code correctness.
Expected Learning Outcomes
● Gain experience with methods for formal reasoning and modelling of programming languages;
● Understand and practice on how to turn a formal semantics specification into an interpreter;
● Understand how design tools for program analysis and verification.
Course Prerequisites
CSC453 (Compilers and Systems Software)
Activities
● Midterm exam (30%): Thursday, October 10, based on Part 1.
● Final exam (30%): Tuesday, December 17, based on Part 2.
● Homework (HW) assignments (40%). There will be 4 homework assignments during the semester, each assigned at the end of a main block of lectures. Extra backup-homework in correspondence with HW3 and HW4 will be provided for those that want to improve a unsatisfactory score obtained in previous homework.
Lectures
Part 1: Principles (13 lectures)
08/27: Course introduction: A brief history of PL and research trends (1 lecture)
08/29: Order Theory: Posets, lattices, fixpoint theory, inductive/deductive definitions (6 lectures)
Set Theory, Lattice Theory, Fixpoints and inductive/deductive definitions.
09/17: Homework 1 assignment
09/19: Operational Semantics of PL (2 lectures)
09/26: Denotational Semantics of PL & Types (4 lectures)
10/01: Homework 2 assignment
Part 2: Design and implementation (16 lectures)
10/08: The design and implementation of an interpreter (5 lectures).
10/15: Mid-Term Exam
10/17: Homework 3 assignment (see the text of D2L)
10/29: Properties of programs and program logics (4 lectures)
11/14: Homework 4 assignment
11/12: Principles of program analysis and verification (7 lectures) Slides, Video1
Final Examination: Tue, December 17, 2024
Bibliography
● B. A. Davey and H. A. Priestley, Introduction to Lattices and Order. Cambridge University Press
● Glynn Winskel, The Formal Semantics of Programming Languagesm. MIT Press.
● John C. Mitchell, Concepts in Programming Languages. Cambridge University Press.
● Benjamin C. Pierce, Types and Programming Languages. MIT Press.
● Patrick Cousot, Principles of Abstract Interpretation. MIT Press.
Grading Scale and Policies
Your final grade is based on the percentage of all available points that you receive. A typical example of how percentages might translate into letter grades is A: 91-100, B: 71-90, C: 51-70, D:31-50, E:0-30. I do not claim that the grade cutoffs for this class will be the same. These cutoffs are merely to give you an idea of how I have graded in the past. Without prior arrangement, missed exams and late homework assignments are not graded for credit. In exceptional circumstances extra time can be requested. If you discuss with me well before the due date, requests will be considered reasonably.