Term 1 (Fall), 2016-2017 |
Mon. & Wed. 1:30pm - 3:00pm DMP 101 |
Ronald Garcia |
Office: ICICS 387 |
Email: |
Office hours: Wednesdays 11am-12pm or by appointment |
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 covered in class, as well as through some supplementary readings. That being said, the material we will cover is will draw from a variety of sources.
The following books are recommended but not required:There will be an in-class 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 be typeset using the LaTeX document preparation system, and turned in electronically as PDFs. Assignments will be made available on Thursdays (i.e. the day after the second class of the week) and each will be due the following Thursday.
Assignments are to be done in pairs, each student with a partner (adjustments will be made for odd numbers of students as needed). You may only discuss the homework with your partner, and turn in an assignment with both of your names on it. You may switch partners throughout the course, but that is not necessary.
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 resources are to help you succeed in the class.
The following is a draft course schedule. The exact details (including some topics) will vary depending on the content covered in class and the interests 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).
# | Date | Topics | Notes | Supplementary Readings | |
---|---|---|---|---|---|
1 | Sep | 7 | Course Introduction | ||
2 | 12 | Modeling Programming Languages, Sets, and Logic | Notes | Set Theory | |
3 | 14 | Logic, Formally |
Logical Reasoning Verifications |
Proving Things False | |
4 | 19 |
Syntax: Parsing as Proof Search Big-Step (or Natural) Semantics From Inversion Lemmas to Racket Code |
Notes | ||
5 | 21 | Structural Operational (Small-Step) Semantics (S.O.S.) | Notes | ||
6 | 26 | Logic Revisited; Syntax as Proofs | |||
7 | 28 | Proofs are Programs (Certifying Interpreters) | |||
8 | Oct | 3 | Inductive Definitions | Notes | |
9 | 5 | Proof by Induction | Notes | ||
10 | Thanksgiving: No Class | ||||
10 | 12 | Induction Boot Camp! | bootcamp.rkt | ||
11 | 17 |
Abstracting Abstract Syntax (Gödel Numbering) Reduction Semantics |
Notes | ||
12 | 19 | IMP: Imperative Programming | |||
13 | 24 | Induction and Coinduction | |||
14 | 28 | Coinduction, Part 2 | |||
31 | Modeling Divergence | ||||
Nov | 2 | Floyd-Hoare Program Logics | |||
15 | 7 | Lexical Variables | |||
9 | Procedures and Recursion | Notes | |||
16 | 14 | Choose Your Own Induction Principle | Notes | ||
17 | 16 | Type Systems | |||
18 | 21 | Static Analysis | |||
19 | 23 | Exam | |||
20 | 28 | Presentations: Joey and Jodi (Pi Calculus) | Slides | ||
21 | 30 | Presentations: Xing and Enrique (Probabilistic Programming Languages) | Slides | ||
22 | Dec | 2 | Presentations: David, Rodrigo, and Nodir (NetKAT: Network Programming Languages) | Slides | |
Last modified: Sat Dec 07:57:25 UTC 2016 by ronaldgarcia