Essentials of Programming Languages
Personal
| Lecture | Prof. Dr. Peter Thiemann | thiemann@info... |
| Exercise | Hannes Saffrich | saffrich@info... |
| Weili Fu | weilifu@info... |
News
| 2020-04-27 | Course availability: Lecture stream and recordings will be available on Ilias |
| 2020-04-27 | Software image available: Agda VM 2020 SS (Ubuntu, 64-bit).ova |
| 2020-04-30 | Video how to Install and start the VM image |
| 2020-05-07 | Video Intro to content of the course |
| 2020-05-13 | Updated Schedule |
| 2020-05-13 | Added Links section |
| 2020-05-14 | Software image update, see below |
| 2020-08-26 | The exam project is now available. |
Lecture Materials
| Date | Content | Code | Solutions | Recording |
|---|---|---|---|---|
| 2010-05-13 | PLFA - Part 1 - Naturals | Naturals.agda | youtube | |
| 2010-05-14 | PLFA - Part 1 - Naturals / Induction | youtube | ||
| 2010-05-20 | PLFA - Part 1 - Induction | Induction.agda | youtube | |
| 2010-05-27 | PLFA - Part 1 - Relations | Relations.agda | youtube | |
| 2010-05-28 | PLFA - Part 1 - Relations (continued) | youtube | ||
| 2010-06-03 | PLFA - Part 1 - Equality | Equality.agda | youtube | |
| 2010-06-10 | PLFA - Part 1 - Isomorphism | Isomorphism.agda | youtube | |
| 2010-06-16 | PLFA - Part 1 - Isomorphism (continued offline) | youtube | ||
| 2010-06-17 | PLFA - Part 1 - Connectives | Connectives.agda | youtube | |
| 2010-06-18 | PLFA - Part 1 - Connectives (continued) | youtube | ||
| 2010-06-24 | PLFA - Part 1 - Negation | Negation.agda | youtube | |
| 2010-06-25 | PLFA - Part 1 - Quantifiers | Quantifiers.agda | youtube | |
| 2010-07-01 | PLFA - Part 1 - Quantifiers (continued) | youtube | ||
| 2010-07-02 | PLFA - Part 1 - Decidable | Decidable.agda | youtube | |
| 2010-07-08 | PLFA - Part 1 - Lists | Lists.agda | youtube | |
| 2010-07-09 | PLFA - Part 1 - Lists (continued) | youtube | ||
| 2010-07-15 | PLFA - Part 2 - Lambda Calculus | Lambda.agda | youtube | |
| 2010-07-16 | PLFA - Part 2 - Lambda Calculus (continued) | youtube | ||
| 2010-07-22 | PLFA - Part 2 - Lambda Calculus (continued) | youtube | ||
| 2010-07-23 | PLFA - Part 2 - Lambda Calculus (continued) | youtube | ||
| 2010-07-29 | PLFA - Part 2 - Lambda Calculus Properties | Properties.agda | youtube | |
| 2010-07-30 | PLFA - Part 2 - Lambda Calculus Properties (continued) | youtube |
Note: "Recordings" are unedited screen recordings of the lecture.
Schedule
| Lecture | We 14-15 ct | Th 16-17 ct | Live Stream |
| Exercise (Weili) | We 17-18 ct | Th 17-18 ct | Zoom Meeting (Password has been sent via mail) |
| Exercise (Hannes) | We 17-18 ct | Th 19-20 ct | Zoom Meeting (Password has been sent via mail) |
Content
This course conveys fundamental concepts of 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.
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 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 the core idea 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
Every week there are two time slots of 90 minutes each where live action is available. Each time slot is dedicated to (part of) a chapter in PLFA. The first half features a live stream were we walk through and demonstrate the salient points of the chapter. We ask you to prepare for this live stream by reading the chapter in advance. We will try to cover questions interactively. (Depending on availability, the Thursday session may be prerecorded.)
For the second half, we will meet (online) in small groups, discuss questions, and pose further example problems that we work on together. The topics will be drawn on the content of the preceding lecture. There may some flexibility in scheduling for these meetings up to the availability of Saffrich and Fu.
Recordings will be available for the live stream so that asychronous participation is possible. 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 building a formal model of a language and prove some properties about it. There is no weekly exercise, but we strongly encourage active participation in the discussion sessions.
Homework Project
The homework project can be found here. An email with further details has been sent via Ilias. If you did not receive the email, please contact us.
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!
Links
- Official Agda Documentation
- Emacs Agda-Mode Documentation
- Agda Standard Library
- Programming Language Foundations in Agda (Book)
Software Image
In case you want to do the book's exercises by directly editing the book source code, we've updated the software image to include a copy of the PLFA book and set up emacs such that it automatically loads the agda-mode when an .lagda.md file is opened.
If you already got the previous image, you can quickly upgrade it by running the following command in a terminal inside your virtual machine:
wget -qO- https://proglang.informatik.uni-freiburg.de/teaching/proglang/2020ss/vm_update | bash