This course is about the formal specification of programming languages, especially in terms of operational semantics and formal type rules. The course objective is to enable students to read, write, and reason about formal models of programming languages.

Students will write paper-and-pencil proofs and also implement models using PLT Redex.

Semantics Engineering with PLT Redex
Felleisen, Findler, and Flatt, 2009

Later in the semester, we'll use some notes on type systems (in the same style as the book), to appear.

A light homework assignment will follow most lectures, and it is always due at the beginning of the following class, unless otherwise specified. Homework assignments are posted with the Schedule/Homework Page.

Participants can work on homework in pairs, with the proviso that no pair of students can collaborate on more than 3 homework assignments. Collaborators should submit a single homework solution.

cs7520@list.eng.utah.edu

All course announcements will go to the mainling list, and all students must sign up. To sign up for the mailing list, visit https://sympa.eng.utah.edu/sympa/info/cs7520.

There will be one mid-term exam and a final exam, but final grades will be determined primarily by homework: 60% homework, 20% mid-term, 20% final.

The University of Utah conforms to all standards of the Americans with Disabilities Act (ADA). If you wish to qualify for exemptions under this act, notify the Center for Disabled Students Services, 160 Union.