Programming language foundations
Summary
This course provides an introduction to the theory of programming languages, with an emphasis on language design and formal semantics.
Content
Students will learn how to formalize common programming constructs using operational, denotational, and axiomatic models; to prove properties about programs using language-based reasoning tools; and to apply these ideas in the design of a new domain-specific language.
Note that the list of topics is tentative and different topics will be explored at different levels of detail. In class participation is strongly recommended.
Introduction and Mathematical Preliminaries
- Coures overview and motivation; sets, relations, functions, induction, etc.
Operational Semantics
- Large and small-step semantics; evaluation rules; proofs by induction.
Denotational Semantics
- Relational models; fixpoints; relationship to operational semantics
Axiomatic Semantics
- Partial and total correctness; Hoare logic; soundness and relative completeness
Imperative Features
- Pointers and heaps; separation logic
Lambda Calculus
- Syntax and semantics; substitution; encodings; fixed-point combinators
Type Systems
- Typing rules; type soundness; normalization
Polymorphism
- System F; type inference; relational parametricity
Continuations
- Continuation-passing style; exceptions and control operators; compilation
Effects
- Monads, effect handlers
Relational Reasoning
- Program equivalence; algebraic methods; relational logics
Concurrency
- Interleaving semantics; message-passing; bisimulation
Domain-Specific Languages
- Case studes from selected domains (e.g., databases, graphics, networking, etc.)
Victory Lap
- Project presentations; research in programming languages
Learning Prerequisites
Required courses
Any previous programming courses
Recommended courses
- CS-214 Software construction
- CS-320 Computer language processing
Important concepts to start the course
- Discrete math
- Proofs and induction
Learning Outcomes
By the end of the course, the student must be able to:
- Define the formal semantics of common programming constructs
- Prove programs properties using program logics and type-based reasoning
- Design and implement a domain-specific language (DSL)
Teaching methods
Ex cathedra lectures; labs
Expected student activities
- Lectures
- Programming assignments
- Course project
- Final exam
Assessment methods
- Programming assignments (20%)
- Course project (20%)
- Final exam (60%)
Supervision
| Office hours | Yes |
| Assistant.e.s | Yes |
In the programs
- Semester: Fall
- Exam form: Written (winter session)
- Subject examined: Programming language foundations
- Courses: 3 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Fall
- Exam form: Written (winter session)
- Subject examined: Programming language foundations
- Courses: 3 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: optional
- Semester: Fall
- Exam form: Written (winter session)
- Subject examined: Programming language foundations
- Courses: 3 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: mandatory
- Semester: Fall
- Exam form: Written (winter session)
- Subject examined: Programming language foundations
- Courses: 3 Hour(s) per week x 14 weeks
- Exercises: 2 Hour(s) per week x 14 weeks
- Project: 2 Hour(s) per week x 14 weeks
- Type: mandatory