Programming Languages

CS 263, Spring 2021

Instructor: Qinxiang Cao (曹钦翔)

TA: Zhang Cheng (程章)


Lectures
Time: Monday 10:00-11:40, Wednessday 8:00-9:40
Location: East Up Hall 107
Discussions
QQ Group: 885615034
Emails
Instructor: caoqinxiang@sjtu.edu.cn
TAs: mooc3535@gmail.com


Overview

This course, Programming Languages, is about the theory for the following questions: is this program correct? why is it correct? why is it not correct? how to describe the behavior of a program? how to describe the designed functionality of a program? You will learn operational semantics, denotational semantics, Hoare logic, basic functional programming and proof engineering in Coq (official download, local mirror).

Extended Reading

  1. Schmidt, David. Denotational semantics: a methodology for language development William C. Brown Publishers, 1986
  2. Winskel, Glynn. The Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993.
  3. Ebbinghaus, Heinz-Dieter. Mathematical Logic. Springer, 1996.
  4. Pierce, Benjamin, et. al. Software Foundation. Online.
  5. Harper, Robert. Practical Foundations for Programming Languages. Cambridge: Cambridge UP, 2016.

Homework

  1. Download Release date: 2/24. Due date: 2/28.
  2. Download Release date: 3/08. Due date: 3/12.
  3. Download (a) Release date: 3/17. Due date: 3/21.
    Download (b) Release date: 3/22. Due date: 3/26.
  4. Download Release date: 3/29. Due date: 4/02.
  5. Download Release date: 4/12. Due date: 4/18.
  6. Download (a) Release date: 4/21. Due date: 4/25.
    Download (b) Release date: 4/21. Due date: 4/25.
  7. Download Release date: 5/08. Due date: 5/12.
  8. Download Release date: 5/17. Due date: 5/21.
  9. Download Release date: 5/24. Due date: 5/28.
  10. Download Release date: 5/31. Due date: 6/04.

Quiz

  1. Download Release date: 4/28. Due date: 5/07.
  2. Download Release date: 6/09. Due date: 6/25.
  3. To Be Released

Final project

  1. Instructions
  2. Topics
  3. Useful definitions and references

Lecture Schedule

All lectures:

Week Date Lecture Notes Additional Readings
1 2/22    Introduction.html / .v
2/24    Hoare_Logic_1.html / .v
2 3/01    Hoare_Logic_2.html / .v
3/03    Hoare_Logic_3.html / .v
3 3/08    Hoare_Logic_4.html / .v
3/10    Denotational_Semantics_1.html / .v
4 3/15    Denotational_Semantics_2.html / .v
3/17    Denotational_Semantics_3.html / .v Taski_Fix_Point.html
5 3/22    Denotational_Semantics_4.html / .v
3/24    Small_Step_Semantics_1.html / .v
6 3/29    Small_Step_Semantics_2.html / .v
3/31    Steps_vs_Denotations.html / .v
7 4/05    Qing Ming, No Lecture
4/07    Denotations_vs_Triples_1.html / .v
8 4/12    Denotations_vs_Triples_2.html / .v
4/14    Denotations_vs_Triples_3.html / .v
9 4/19    VST and Tutorial Package for Windows (.zip)
   Tutorial Only (.zip)
4/21    VST tutorial
10 4/26    Control_Flow.html / .v
4/28    Function_Call.html / .v
11 5/03    Labor's day, No Lecture
5/05    Labor's day, No Lecture
5/08    Error_1.html / .v
12 5/10    Error_2.html / .v
5/12    Nondeterminism_and_Nontermination.html / .v
13 5/17    Pointer_And_Address.html / .v
5/19    Lambda_Calculus_1.html / .v
14 5/24    Lambda_Calculus_2.html / .v
5/26    Lambda_Calculus_3.html / .v
15 5/31    Lambda_Calculus_4.html / .v
6/02    SSA_1.html / .v
16 6/07    SSA_2.html / .v
6/09    SSA_3.html / .v

Additional Coq library support: RTClosure.v, Imp.v, ImpExt.v, ImpExt2.v, ImpExt3.v, ImpCF.v, Lambda.v