Essentials of Programming Languages
Schedule
| Lecture | We 14-16:00 | Room 106 SR 00-007 | Prof. Dr. Peter Thiemann | thiemann@info... |
| Tutorials | Fr 14-16:00 | Room 106 SR 00-007 | Hannes Saffrich | saffrich@info... |
News
| 2023-10-19 | The Ilias Course is now available. |
Lecture Materials
| Date | Content | Code | Recording |
|---|---|---|---|
| 2023-10-18 | Overview | ||
| 2023-10-25 | PLFA - Part 1 - Naturals & Induction | Lecture2.agda | Recording |
| 2023-11-01 | PLFA - Part 1 - Relations | Relations.agda | Part1, Part2 (from SS2020) |
| 2023-11-08 | PLFA - Part 1 - Equality | Recording | |
| 2023-11-15 | PLFA - Part 1 - Isomorphism & Connectives (product, unit, sum, empty) | Recording | |
| 2023-11-22 | PLFA - Part 1 - Negation | Recording | |
| 2023-11-29 | PLFA - Part 1 - Quantifiers & Decidable | Recording | |
| 2023-12-06 | PLFA - Part 2 - Lambda | Recording | |
| 2023-12-13 | PLFA - Part 2 - Properties | Recording | |
| 2023-12-20 | Intermezzo - Semantics of While | Imperative.agda | Recording |
| 2023-01-10 | PLFA - Part 2 - DeBruijn | Recording | |
| 2023-01-17 | PLFA - Part 2 - More (finished) | Recording | |
| 2023-01-24 | PLFA - Part 2 - Bisimulation | Recording | |
| 2023-01-31 | PLFA - Part 2 - Inference | Recording | |
| 2023-02-07 | PLFA - Part 2 - Untyped | Recording |
Tutorial Materials
| Date | Content | Solutions | Recording |
|---|---|---|---|
| 2023-10-20 | Propositions as Types, Programming Language Theory, Agda Mode | Recording | |
| 2023-10-27 | PLFA - Part 1 - Naturals & Induction | chap01_naturals.agda, chap02_induction.agda | Recording |
| 2023-11-03 | PLFA - Part 1 - Relations | chap03_relations.agda | Recording |
| 2023-11-10 | PLFA - Part 1 - Equality | chap04_equality.agda | Recording |
| 2023-11-17 | PLFA - Part 1 - Isomorphism & Connectives | chap05_isomorphism.agda, chap06_connectives.agda | Recording |
| 2023-11-24 | PLFA - Part 1 - Negation & Lists | chap07_negation.agda, chap10_lists.agda | Recording corrupted :( |
| 2023-12-01 | PLFA - Part 1 - Quantifiers & Decidable | chap08_quantifiers.agda, chap09_decidable.agda | Recording |
| 2023-12-08 | PLFA - Part 2 - Lambda Calculus | chap11_lambda.lagda.md | Recording |
| 2023-12-15 | PLFA - Part 2 - Properties | chap12_properties.lagda.md | Recording |
| 2023-12-15 | Intermezzo - Hoare Logic | Imperative-Hoare.agda | Recording |
| 2024-01-12 | PLFA - Part 2 - DeBruijn | chap13_debruijn.lagda.md | Recording |
| 2024-01-19 | PLFA - Part 2 - More | chap14_more.agda | Recording |
| 2024-01-26 | PLFA - Part 2 - Bisimulation | chap15_bisimulation.agda | Recording |
| 2024-02-02 | Pointers, Exceptions, Subtyping, Algebraic Data Types, Polymorphism | Recording | |
| 2024-02-09 | PLFA - Part 2 - Untyped & Confluence, Extrinsic Typing, Local Module Imports | Recording |
Content
This course conveys the mathematical and logical concepts underlying programming languages using the language Agda. It mainly follows the online book Programming Language Foundations in Agda (PLFA) by Philipp Wadler, Wen Kokke, and Jeremy Siek. Agda is a functional language with an advanced type system that enables the encoding of many program properties in its types. Agda's type checker verifies proofs of these properties, so that one could also say this course is about verified programming.
The first part of the course covers the logical background needed to study the theory of programming languages to the extent that we can give formal guarantees about the execution of a program. The content of this part should be familiar from an introductory logic class, but it is presented in an entirely different way. The central idea conveyed is that every program (in a language with a reasonable type system) is really a proof about the meaning of the program. Conversely, it means that every proof can be viewed as a program, so that proving becomes programming a function with a certain type. For example, inductive proofs are expressed by terminating recursive functions. This correspondence is called the Curry-Howard correspondence. It is one of the most powerful discoveries in logics and programming and it is one of the core ideas behind Agda.
The second part of the course puts this toolbox to work. We use Agda's features to model the syntax and the semantics of (simple) programming languages. We model type systems and connect them to the semantics through type soundness theorems. We learn about different ways of modeling syntax and semantics and their pros and cons. We study type inference as a means to find a best possible (principal) typing for a given program, if such a typing exists.
Approach
The lecture is closely aligned with the contents of the PLFA book:
- On Wednesdays we discuss (part of) a chapter from the PLFA book. We ask you to prepare for this by reading the chapter in advance. We will try to cover questions interactively.
- On Fridays we discuss the exercises of the corresponding chapters (contained in the book), and answer general questions related to Agda, Theorem Proving and Programming Language Theory. Occasionally we may also show you cool stuff not covered in the book.
Recordings of the lecture will be available so that asychronous participation is possible. The exercise sessions will not be recorded. The PLFA book is freely available in source code, so that everything can be tried hands on. It is amenable to self study, but the pragmatics of using Agda are much easier to deal with in an interactive supportive environment such as we are trying to provide.
Exam
The final grade will be based entirely on a graded homework, which builds on the material covered in the second part of the course. That is, you will be using Agda to build a formal model of a language and prove some properties about it. The exam will be handed out on March 3 and results need to be submitted until March 31, 23:59.
Both the exercises and the exercise sessions are voluntary, but we highly recommend doing the exercises and participating in the discussions. There is no submission of exercises, since the Agda type checker will tell you, when your proofs are correct.
The exam can be downloaded here.
Communication
Announcement will be posted on this page under the rubric News as well as through Ilias. If you do not want to miss these announcements, make sure you have a valid email registered with Ilias!
We also provide a Discord-like chat for questions about the lecture, exercises, and related topics. You can log in there via your RZ-Account, i.e. with the same credentials as for Ilias.
Software
For this course you need the following software setup:
- Agda Version 2.6.3
- Agda Standard Library Version 1.7.2
- Emacs with Agda-Mode or VSCode with Agda-Mode
If you don't want to go through the setup process yourself, then you can use our VirtualBox image that has the required software preinstalled. If you haven't worked with VirtualBox before, you can watch our video tutorial on how to use the image.
If you do want to install the software yourself, make sure to install Agda and its standard library in exactly the specified versions. We recommend to follow the installation process as described in the Getting Started chapter of the PLFA book.
Note that editor support is absolutely crucial when working with dependently typed programming languages, and so far is only provided in sufficient capacity for emacs and vscode. emacs is used in the lecture, exercise sessions, and the book.
Links
- HisInOne Lecture and Exercises
- Programming Language Foundations in Agda (Book)
- Official Agda Documentation
- Emacs Agda-Mode Documentation
- Agda Standard Library
- VirtualBox Image with Agda and Emacs
- Emacs Configuration for Agda (Normal / Vim Keybindings)
- Discord-like chat for questions about the lecture, exercises, and related topics. Login via RZ-Account, i.e. same as for Ilias.
- A list of all unicode symbols that can be typed in agda-mode via LaTeX commands. You probably need to download this file, because the browser uses the wrong character encoding, which causes the unicode characters to look scrambled.