Calendar and Slides

1. 1/22: Intro, Motivation, Goals.
   • Reading: Hoare: Hints For Programming Language Design
2. 1/24: A Simple Imperative Language Operational Semantics
   • Reading: Winskel Chapter 2 and Mitchell Chapter 6.3
3. 1/29: Proof Techniques Based on Operational Semantics
   • Reading: Winskel Chapter 3.
4. 1/29: Same as previous lecture
5. 2/5: Introduction to Denotational Semantics
6. 2/7: Same as previous lecture
7. 2/12: Introduction to Axiomatic Semantics
   • Reading: Hoare: An Axiomatic Basis for Computer Programming
8. 2/14: Same as previous lecture
9. 2/19: Same as previous lecture
   • Reading: Completeness proof for axiomatic semantics (Errata: reverse the direction implication in the first formula)
10. 2/21: Same as previous lecture
11. 2/26: Symbolic execution
    • Reading: Symbolic Execution for Software Testing: Three Decades Later
12. 2/28: Same as lecture 7
13. 3/5: MultiSE: same as lecture 11
    • Reading: MultiSE: Multi-Path Symbolic Execution using Value Summaries
14. 3/7: Lambda Calculus
    • Reading: An Introduction to Lambda Calculus

15. 3/12: Lambda-calculus and Functional Programming

16. 3/14: Type systems

• Reading: Luca Cardelli "Type Systems"

17. 3/21: same as previous lecture

18. 4/2: same as previous lecture

19. 4/4: Subtyping

• Read Chapter 15 of Benjamin Pierce. "Types and Programming Languages", MIT Press, 2005.

20. 4/9: Second-order types

• Read Chapter 22 and 23 in Benjamin Pierce. "Types and Programming Languages", MIT Press, 2005.

21. 4/11: Abstract Interpretation

Topics (tentative):

• Introduction, Motivation
• Introduction to Operational Semantics
• Proofs by Structural Induction
• Continue and finish proofs
• Introduction to Denotational Semantics
• Axiomatic Semantics
• Symbolic Execution
• Introduction to Lambda Calculus
• Lambda Calculus and Functional Programming
• First-Order Type Systems
• Recursive Types, Subtyping
• Second-Order Type Systems: Polymorphism, Abstract Types
• Types and Effects: Region-Based Type Systems
• 
  
•