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.Textbook
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.Course Schedule and Homework
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.Mailing List
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.
|Last update: Wednesday, February 20th, firstname.lastname@example.org|