CS578 Programming Language Semantics Spring 2024
-
Email: tolmach@pdx.edu
-
Office Hours: please email for an appointment in person or on zoom.
Course Information
-
Syllabus
-
Slack channel Note: the first time you use this link, it may take you to the general page for the pdx-cs workspace; you need to sign in to access the cs578-specific channel.
Review Quiz
- To check whether you have the necessary background for this course, trying taking this review quiz.
If these problems aren't reasonably straightforward for you (maybe after a bit of review from previous courses), don't despair, but
please do consult the instructor about whether it makes sense to stay in the course.
(Here are sample solutions if you get really stuck.)
Exams
Additional Readings
Lecture Notes
Recordings, whiteboard photos, and selected on-line notes for lectures will appear here.
Homework Assignments
Textbook Resources
- OCAML code for the various typechecker implementations.
- An import list of errata
for Types and Programming Languages. Check here first if you can't make sense of something in the text.
OCaml Resources
Latex Resources
- Download information for latex.
- The Overleaf online system.
- Pierce's style file for typesetting the definitions of inference rules.
(You need to download this and put into the directory where you run latex.)
- Documentation for Tatsuta's proof style file which I often use for typesetting derivations.
(This is already in standard latex distributions.)
- Here is an example (with the corresponding output)
of how I do typesetting in the style of Pierce's book
- The detexify tool is handy for finding symbol names.
- A page
discussing recommendations for where to start learning latex.
Semantics Resources
Mechanized Proofs
These references cover similar material to this course using fully formalized proofs that are
mechanically checked in various systems:
