Fundamentals of Programming Languages (X037515)

Winter Semester 2017/2018

to master students, school of software


Guoqiang Li

Teaching Assistant

Yuwei WANG: wangyuwei95 (AT) qq (DOT) com


8:00am - 10:45am every Wednesday


Chen Rui Qiu 311

Office hour

Tue. 14:00-17:00 at 3203 Building of Software


  • Edmund M. Clarke Jr., Orna Grumberg, Doron A. Peled. Model Checking. MIT Press, 1999

  • Glynn Winskel. Formal Semantics of Programming Languages: An Introduction. MIT Press, 1993

  • Benjamin C. Pierce. Types and Programming Languages. MIT Press, 2002

  • Lectures

    Sep. 20
    Lecture 1. Introduction and logic basics.

    Sep. 27
    Lecture 2. Model checking.

    Oct.  4
    Mid-Autumn Day!

    Oct. 11
    Lecture 3. Finite automata and Buchi automata.

    Oct. 18
    Lecture 4. LTL model checking.

    Oct. 25
    Lecture 5. Abstract interpretation I.

    Nov.  1
    Lecture 5. Abstract interpretation II.

    Nov.  8
    Lecture 6. Pushdown automata and interprocedural programs.

    Nov. 15
    Exercise I.

    Nov. 22
    Lecture 7. Programming semantics I.

    Nov. 29
    Lecture 7. Programming semantics II.

    Dec.  6
    Lecture 8. Lambda calculus and types I.

    Dec. 13
    Lecture 8. Lambda calculus and types II.

    Dec. 20
    Lecture 9. Conclusions.

    Dec. 27
    Exercise II.


    Fundamentals of Programming Languages
    by Evan Chang @ University of Colorado Boulder

    Principles of Programming Languages
    by Sam Staton @ Oxford

    Foundations of Programming Languages
    by Robert Simmons @ CMU

    Principles of Programming Languages
    by Hongwei Xi @ Boston U.

    Introduction to Programming Languages Theory
    by anonymous @ Standford


    Assignment 1, deadline: Oct. 18

    Assignment 2, deadline: Nov. 15

    Assignment 3, deadline: Nov. 29

    Final Reports

    Report 1. Probabilistic model checking (3/3)

    Report 2. Stochastic model checking (3/3)

    Report 3. Model checking in a specific field (5/5)

    Report 4. Antichain for Universality, subset of automata (0/3)

    Report 5. Bounded model checking for LTL (3/3)

    Report 6. Algorithms for widening and narrowing (1/3)

    Report 7. An interprocedural program analysis methodology other than PDS (1/3)

    Report 8. Semantics and Key Properties of CCS (0/3)

    Report 9. Semantics and Key Properties of CSP (0/3)

    Guoqiang Li
    Last modified: Wednesday, Aug. 9, 2017.