Formal Semantics of Programming Languages

Last updated: 2024-06-03

Course Info

Abstract

In this course we study methods to define behaviors of programs, and methods to reason about properties of programs. We also practice building verified programs using Coq.

Time

Every Thu., 8:30am - 11:45am, starting from Mar 7

Classroom

Room A3-3-201 | Zoom: 559 700 6085 (pw: BIMSA)

Schedule

DateTopicReading
Mar. 07Introduction, (untyped) $\lambda$-calculus
Mar. 14$\lambda$-calculus, cont’; STLC
Mar. 21Curry-Howard Isomorphism; Strong Normalization (Coq Demo)
Mar. 28Strong Normalization, cont’; System F
Apr. 04Holiday
Apr. 11Higher-order Types, Dependent Types
Apr. 18Operational Semantics
Apr. 25Denotational Semantics
May. 02Holiday
May. 09Hoare Logic
May. 16Separation Logic
May. 23Semantics of Concurrent Programs
May. 30Semantics of Quantum Programs
Jun. 06Semantics of Quantum Programs, cont'

Intended Syllabus

  • Lambda calculus
  • Simply-typed lambda calculus
  • Operational semantics
  • Denotational semantics
  • Hoare logic
  • Separation logic
  • Concurrency and Concurrent Separation Logic (CSL)
  • Categorical semantics of quantum programs

References

  1. Benjamin C. Pierce, et al. Software Foundations.
  2. John C. Reynolds. Theories of Programming Languages.
  3. Viktor Vafeiadis. Concurrent separation logic and operational semantics.
  4. Chris Heunen and Jamie Vicary. Categories for Quantum Theory: An Introduction.