Rose

Teaching

This page describes courses taught at WPI. At CMU, I previously taught functional programming and cyber-physical systems verification.

Programming Languages CS 4536-A01 (2021)

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.

Special Topic: Logical Foundations of Cyber-Physical Systems CS 525 (Spring 2022)

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 explicitly encouraged to enroll. It is a logic course at heart. Students will learn to model cyber-physical systems using programs and differential equations, then prove them. You will learn to do formal proofs on a computer for homework. A robot will be available to optionally run your code (for fun).

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 not a prerequisite.