plt17:top
Table of Contents
Programming Language Theory 2017
Instructor: Hossein Hojjat
Email: hh at cs rit edu
Office hours (GOL-3545):
- Tu 11am – 12am
- Th 11am - 12am
Lectures: MoWeFr 1:25PM - 2:20PM (GOL-1445)
Final Exam: 12/18/2017 (12:30 PM - 2:30 PM) , Place: GOL-1445
Description & Policies:
CS Common Course Policies
Grading Policies
Homework Assignment Policies
Acknowledgements:
Portions of this course material based upon similar courses offered by Armando Solar-Lezama and Adam Chlipala.
Recommended Books:
Course Materials
Week 1
| Monday 08/28 | Lecture 1: Course Overview | Slides |
| Wednesday 08/30 | Lecture 2: Introduction to Scala | Slides |
| Friday 09/01 | Lecture 3: Functions in Scala | Slides |
Week 2
| Monday 09/04 | Labor Day | |
| Wednesday 09/06 | Lecture 4: Types in Scala | Slides |
| Friday 09/08 | Lecture 5: Boolean Satisfiability (SAT) Solving | Slides |
Week 3
| Monday 09/11 | Lecture 6: The λ-calculus | Slides |
| Wednesday 09/13 | Instructor attending RV 2017 | |
| Friday 09/15 | Lecture 7: Programming in the λ-calculus | Slides |
Week 4
| Monday 09/18 | Lecture 8: The λ-calculus Semantics | Slides |
| Wednesday 09/20 | Lecture 9: Introduction to Coq | Slides |
| Friday 09/22 | Lecture 10: Coq Demo |
Week 5
| Monday 09/25 | Lecture 11: Introduction to Simple Types | Slides |
| Wednesday 09/27 | Lecture 12: Simple Types: Progress & Preservation | Slides |
| Friday 09/29 | Lecture 13: Type Inference & Polymorphism | Slides |
Week 6
| Monday 10/02 | Lecture 14: Hindley-Milner Type System | Slides |
| Wednesday 10/04 | Lecture 15: Subtyping | Slides |
| Friday 10/06 | Lecture 16: Semantics for Imperative Programs | Slides |
Week 7
| Monday 10/09 | October Break | |
| Wednesday 10/11 | Lecture 17: Types for Imperative Features | Slides |
| Friday 10/13 | Lecture 18: Types for Information Flow | Slides |
Week 8
| Monday 10/16 | Recitation - Assignment 2 Discussion | |
| Wednesday 10/18 | Lecture 19: Introduction to Axiomatic Semantics | Slides |
| Friday 10/20 | Lecture 20: Hoare Rules | Slides |
Week 9
| Monday 10/23 | Lecture 21: Verification Condition Generation (I) | Slides |
| Wednesday 10/25 | Lecture 22: Verification Condition Generation (II) | Slides |
| Friday 10/27 | Lecture 23: Verification by Solving Horn Clauses | Slides |
Week 10
| Monday 10/30 | Lecture 24: Verifying Programs with Arrays | Slides |
| Wednesday 11/01 | Lecture 25: Verifying Programs with Dynamic Allocation | Slides |
| Friday 11/03 | Lecture 26: Hoare Logic for Concurrent Programs | Slides |
Week 11
| Monday 11/06 | Lecture 27: Introduction to Abstract Interpretation | Slides |
| Wednesday 11/08 | Lecture 28: Gallois Connection | Slides |
| Friday 11/10 | Lecture 29: Collecting Semantics | Slides |
Week 12
| Monday 11/13 | Lecture 30: Widening and Narrowing | Slides |
| Wednesday 11/15 | Lecture 31: Introduction to Models and Properties | Slides |
| Friday 11/17 | Lecture 32: Temporal Logic | Slides |
Week 13
| Monday 11/20 | Lecture 33: Automata Theoretic Model Checking | Slides |
| Wednesday 11/22 | Thanksgiving Break | |
| Friday 11/24 | Thanksgiving Break |
Week 14
| Monday 11/27 | Lecture 34: Partial Order Reduction | Slides |
| Wednesday 11/29 | Lecture 35: Bounded Model Checking | Slides |
| Friday 12/01 | Lecture 36: Software Model Checking | Slides |
Week 15
| Monday 12/04 | Software Synthesis for Networks |
| Wednesday 12/06 | Final Presentation: Quinn,Kyle,Bhavin,Joshua |
| Friday 12/08 | Final Presentation: Dustin,Anindo,Harlan,Giovanni |
Week 16
| Monday 12/11 | Course Conclusion |
plt17/top.txt · Last modified: 2017/12/03 20:04 by hossein