Term 1 (Fall), 20182019 
Mon. & Wed. 3:00pm  4:30pm DMP 201 
Ronald Garcia 
Office: ICICS 387 
Email: 
Office hours: To Be Determined 
This course is intended for graduate students in computer science. There are no formal course prerequisites, but you are expected to have the kind of mathematical maturity typical of one who has taken an undergraduate discrete math or theory of computation course. We will explicitly cover proof techniques in this course, so don't worry if you are rusty or not very familiar. Here are some resources I find helpful for refreshing or improving your skill at writing proofs:
To facilitate discussion among students in the class and
myself, we are using the Piazza Q&A platform. The system
allows you to ask questions, refine answers as a group, carry
on followup discussions, and disseminate relevant information.
Rather than emailing questions to me, I ask that you post your
questions to Piazza. If you have any problems or feedback for
the developers, email team@piazza.com.
Find our class
page
here
.
This course has no required textbook. Material will be primarily be provided in a set of notes and/or covered in class, as well as through some supplementary readings. The material we cover will draw from a variety of sources.
The following books are recommended but not required:There will be an inclass midterm exam (date TBD).
Students will give a final presentation to the class on a topic of their own choosing related to Programming Language Principles.
There will be approximately 6 homework assignments during
the course of the semester. Homeworks will
I recommend that homeworks be typeset using the LaTeX
document preparation system, but will not require it:
you have the option to prepare your homework by hand, so long
as you make sure that it is clearly legible by me. I plan to
provide LaTeX templates for you, so this is a good chance to
learn one of the more common tools for writing academic
computer science papers, though the learning curve may be
steep at first. I'm happy to give guidance on how to work
with LaTeX (though I probably don't know all the latest tricks).
You can turn in assignments electronically as PDF's either
scanned or generated by LaTeX.
Assignments must be your individual work. You may discuss the homeworks with others, but you must write up and hand in your own solutions. In particular, follow the whiteboard policy: at the end of the discussion the "whiteboard" must be erased and you must not transcribe or take with you anything that has been written on the board (or elsewhere) during your discussion. You must be able to reproduce the results solely on your own after any such discussion.
Do not draw upon solutions to assignments (or in notes) from similar courses, nor use other such materials (e.g., programs) from any web site or other external source in preparing your work.
The final grade will be comprised of the following components, with the following plan for distribution of marks (subject to revision):
The following resources are to help you succeed in the class.
The following is a draft course schedule, based on a prior offering of the course. The exact details (including some topics) will vary depending on the content covered in class and the interests and needs of the students (and myself).
I often update the notes as the term goes along. They are timestamped, so that you can tell when the most recent version was uploaded (note that the timestamp is distinct from the original date of creation).
Under Construction!#  Date  Topics  Notes  Supplementary Readings  

1  Sep  5  Course Introduction  
2  10 
Modeling Programming Languages; Set Theory and Logic 
Modeling Languages Set Theory 

3  12 
B: A Language with many programs and few results Inductive Definitions Proof by Induction 
Inductive Definitions Proof by Induction 
Proof Techniques Proving Something False 

4  17 
FirstOrder Set Theory Proof Techniques (Structure follows Proposition) 
Proof Techniques Proving Something False 

5  19 
HW1 Review The Truth™ About Inductive Definitions and Induction Principles 

6  24 
Video on Operational Semantics: (Ron Out Of Town: ICFP)

BS Notes SS Notes RS Notes AM Notes 

7  26 
Guest Lecturer (Ron Out Of Town: ICFP) Syntax: Parsing as Proof Search From Inversion Lemmas to Implementations 

8  Oct  1  Proofs are Programs (Certifying Interpreters)  
9  3 
You Can't Even Define All The Functions (?!?) InterRelating Operational Semantics Styles 

8  Thanksgiving: No Class  
10  10 
HW2 Review? Lexical Variables 1 
Notes  
11  15 
HW3 Review Review of Inversion Lemmas Lexical Variables 2 
Lecture 10 Notes  
12  17  (Bound Variable) Names Are For Gravestones: αequivalence classes  Lecture 10 Notes  
13  22  Procedures and Recursion 
Procedures More Procedures 

14  24 
Choose Your Own Induction Principle Variable Scoping and Environments 
Induction Gone Wild! Environments 

15  29 
EnvironmentPassing Semantics Lexical Scoping vs. Dynamic Scoping StorePassing Semantics and Mutable References 
Mutable References  
16  31 
Proper Tail Calls Modeling Divergence 
Tail Calls 

17  Nov  5 
Abstracting Abstract Syntax (Gödel Numbering) Coinduction 

18  7  Type Systems  
19  12  Remembrance Day: No Class  
20  14  Exam  
16  19 
Boyan: Automatic Differentiation Chris: Action Semantics 
Slides  
17  21 
Kumseok: Observational Equivalence in JavaScript Nabil: Undefined Behaviour in C 
Observational Equivalence Undefined Behaviour 

18  26  Adam and Wilder: Pi Calculus 
Slides Go Examples 

19  28  Nico and Renato: Session Types  Slides  
Last modified: Mon Dec 06:52:44 UTC 2018 by ronaldgarcia