This page describes courses taught at WPI. At CMU, I previously taught functional programming and cyber-physical systems verification.
The course explores programming language theory, aimed at 4th-year undergrad students. Functional languages are emphasized, but imperative programming and objects are also discussed. In the homework assignments, you will develop interpreters for a language discussed in class, using the Racket programming language. The course does not teach Racket, but is okay to spend the first week remembering the details of it.
The main course topics are the same as in previous years. Compared to the last time it was taught, I plan to emphasize theory more and include more references to recent research. However, I do not expect major changes to the assignment difficulty.
A cyber-physical system is any system where a computer controls a physical thing, from a car to a power plant to a medical device. These systems are often responsible for human safety, so we need to get them right. This course teaches you how to do that, using logic.
It is a graduate course, but interested undergraduates are
Students have significant freedom in designing final projects about correct cyber-physical systems, which can be done individually or in pairs. The project includes a report and a presentation.
The textbook, “Logical Foundations of Cyber-Physical Systems” by André Platzer, should be freely accessible online through the library. The textbook may be supplemented with research papers.
Prerequisites: We will use the basics of Newtonian mechanics (e.g. PH 1111), calculus (e.g. MA 1021-1022), and logic (e.g. CS 2022). You should be comfortable with rigorous mathematical modeling and proof, plus informal reasoning about programs. If you are unsure whether to skip a prerequisite, a pre-test can be made available upon request to self-check your readiness. We will review and learn differential equations and formal logic, so a differential equations course (MA 2051) is explicitly