This course introduces formal semantics of programming languages. It starts with different semantic approaches (operational, denotational, and axiomatic) in the imperative setting. It then focusses on the semantics of functional languages, with lambda-calculus as the central core.
Learning outcomes:
- To describe the prominent features of operational, axiomatic and denotational approaches to the semantics of programming languages.
- To attribute formal meaning to different aspects of a simple imperative or functional language.
- To use inductive techniques to argue about properties of programming languages.
- To use lambda-calculus as a computational model and as a rewriting system.
- To use type systems for regulating the good formation of programs.
| Date | Description |
|---|---|
| 03 feb. 2025 | Introduction to the module and its logistics (slides) |
| 04 feb. 2025 | NA |
| 10 feb. 2025 | Baby steps with small-step semantics (slides) |
| 11 feb. 2025 | Exercises |
| 17 feb. 2025 | Big steps with big-step semantics (slides) |
| 18 feb. 2025 | Exercises. Implementation of a while-language and its big-step semantics (code) |
| 24 feb. 2025 | Introduction to denotational semantics (slides) |
| 25 feb. 2025 | Exercises |
| 03 mar. 2025 | Domain theory and fixpoints (slides) |
| 04 mar. 2025 | Carnival |
| 10 mar. 2025 | Introduction to axiomatic semantics (slides) |
| 11 mar. 2025 | Weakest pre-condition semantics (slides) |
| 17 mar. 2025 | Hoare calculus. Soundness and Completeness (slides) |
| 18 mar. 2025 | Revisions (handout) |
| 24 mar. 2025 | Test |
| 25 mar. 2025 | NA |
| 30 mar. 2025 | Introduction to the simply-typed lambda-calculus (slides) |
| 31 mar. 2025 | Continuation of the previous lecture |
Two tests (24 Mar and 26 May)
The day and time for appointments is Wednesday afternoon. Please email me the day before if you wish to meet. If you prefer you can also send an email with your questions to me or we can have an online meeting.
Hanne Riis Nielson and Flemming Nielson. Semantics with Applications: An Appetizer. Springer London, 2007. [ bib | DOI ]
Roy L. Crole. Categories for Types. Cambridge mathematical textbooks. Cambridge University Press, 1993. [ bib ]
Glynn Winskel. The formal semantics of programming languages - an introduction. Foundation of computing series. MIT Press, 1993. [ bib ]
This file was generated by bibtex2html 1.99.
Chucky Ellison and Grigore Rosu. An executable formal semantics of C with applications. In John Field and Michael Hicks, editors, Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, Philadelphia, Pennsylvania, USA, January 22-28, 2012, pages 533--544. ACM, 2012. [ bib | DOI | http ]
D. Adams. The Hitchhiker's Guide to the Galaxy. Pan MacMillan, 2009. [ bib ]
This file was generated by bibtex2html 1.99.