SLP-2425

Course on "Semantics of Programming Languages" at the U. of Minho, Portugal

Introduction and objectives 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.

Summaries

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
31 mar. 2025	Introduction to the simply-typed lambda-calculus (slides)
01 apr. 2025	Continuation of the previous lecture (slides)
07 apr. 2025	Equational system of simply-typed lambda-calculus (slides)
08 apr. 2025	Continuation of the previous lecture (slides)
22 apr. 2025	Disjunctive types (slides)

Assessment

Two tests (24 Mar and 26 May)

Contacts

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.

Bibliography

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.

Supplementary bibliography

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.