Programming Languages

CS 263, Spring 2019

Instructor: Qinxiang Cao (曹钦翔)

TAs: Shuyang Tang (汤舒扬) and Zhuyang Wang (王竹阳)


Lectures
Time: Tuesday 8:00-9:40, Friday 10:00-11:40
Location: East Middle Hall 2-202 (东中院2-202)
Office Hours
Time: Thursday 16:00-17:00
Location: Software Building 1110-2 (软件学院1110-2)
Emails
Instructor: caoqinxiang@sjtu.edu.cn
TAs: htftsy@sjtu.edu.cn & wzy1997@sjtu.edu.cn


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 and basic functional programming and proof engineering in Coq (Coq 8.9.0).

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: 3/12. Due date: 3/19.
  2. Download Release date: 3/30. Due date: 4/09. （Library: DS.v)
  3. Download Release date: 4/25. Due date: 5/06.
  4. Download Release date: 5/21. Due date: 5/28.

Final project

  1. Part I: Download release date: 6/4
  2. Part II: Instruction.html Topics.html
  3. Due date: 6/24

Lecture Schedule

All lectures:

Week Date Lecture Notes
1 2/26    Introduction.html    Introduction.v
3/1    Hoare_Logic_1.html    Hoare_Logic_1.v    Imp1.v
2 3/5    Hoare_Logic_2.html    Hoare_Logic_2.v
3/8    Hoare_Logic_3.html    Hoare_Logic_3.v    Imp2.v
3 3/12    Hoare_Logic_4.html    Hoare_Logic_4.v    Imp3.v
   Lab1.v    Lab1_Answer.v    Additional_Comment.txt    Lab at SEIEE (电信群楼) 4-208.
3/15    First_Order_Logic_1.html    First_Order_Logic_1.v    Imp4.v
4 3/19    First_Order_Logic_2.html    First_Order_Logic_2.v    Imp5.v
3/22    Lab2_1.v   Lab2_2.v    Lab2_1_Answer.v    Lab at SEIEE (电信群楼) 4-208.
5 3/26    Denotational_Semantics_1.html    Denotational_Semantics_1.v    Imp6.v
3/29    Denotational_Semantics_2.html    Denotational_Semantics_2.v
6 4/2    Lab3_1.v   Lab3_2.v    Lab at SEIEE (电信群楼) 4-208.
4/5    Qingming. No lecture.
7 4/9    Denotational_Semantics_3.html    Denotational_Semantics_3.v    Lab at SEIEE (电信群楼) 4-208.
4/12    Small_Step_Semantics_1.html    Small_Step_Semantics_1.v
8 4/16    Small_Step_Semantics_2.html    Small_Step_Semantics_2.v
4/19    Steps_vs_Denotations.html    Steps_vs_Denotations.v    Imp7.v
9 4/23    Denotations_vs_Triples_1.html    Denotations_vs_Triples_1.v    Imp8.v
4/26    Denotations_vs_Triples_2.html    Denotations_vs_Triples_2.v
10 4/30    Denotations_vs_Triples_3.html    Denotations_vs_Triples_3.v
5/5    Denotations_vs_Triples_4.html    Denotations_vs_Triples_4.v    Imp9.v
11 5/7    Denotations_vs_Triples_5.html    Denotations_vs_Triples_5.v
5/10    VST.v    README    VST-2.4-bin-i686.zip    VST-2.4-bin-x86.zip    VST-2.4-src.zip    C.zip    _CoqProject
12 5/14    Lab5.v    Lab at SEIEE (电信群楼) 4-208. No lecture.
5/17    Lab6.v    Lab at SEIEE (电信群楼) 4-208. No lecture.
13 5/21    Control_Flow.html    Control_Flow.v
5/24    Run_Time_Error_1.html    Run_Time_Error_1.v
14 5/28    Run_Time_Error_2.html    Run_Time_Error_2.v
5/31    Termination.html    Termination.v
15 6/4    Separation_1.html    Separation_1.v
6/7    The Dragon Boat Festival. No lecture.
16 6/11    Separation_2.html    Separation_2.v
6/14    Final Project Summary.