Notes and Materials for a Course on Programming Languages
Spoiler Alert: For now, I don't recommend reading the notes ahead of the lecture as I am planning to develop the material together in class, so it can be more fun and more interesting if you don't yet know the answers to the questions I am going to ask in class.
Below are linked the files containing the material covered already. I expect you to have read and reviewed this material before the next lecture. If anything is unclear, let me know and I am happy to add material.
Remark: An interesting discussion on the relationship between programming languages in industry and research can be found in Martin Berger's post at stack exchange. To quote "cutting edge theory does not address the concerns of current programming languages. It is about future languages. It will take a while for the 'real world' to catch up. The knowledge you use to build languages for today is the programming language theory of the past." As this is an introductory course to programming languages I will concentrate mostly on such well established theory of the past up to say, very roughly, 1995. I hope that at the end of the course you will agree that this theory is useful for real world programmers now.
We will touch on many topics that are treated in much greater depth in the first two volumes of the series of online textbooks on Software Foundations, which I recommend for further reading. A related course is Programming Language Foundations in Agda . Other references will be added to the lectures.
Lecture 1.1: Overview and Organisation
Lecture 1.2: What is Computation? Numbers, Addition, Multiplication
Lecture 1.3: Computing with High-School Algebra: Adding Variables
Lecture 2.1: Syntax, Semantics, Soundness, Completeness (Part 1)
Lecture 2.2: Discrete Maths: Sets and Relations (and Functions)
Lecture 2.2-b: Meaning in Syntax. Or: Syntax, Semantics, Soundness, Completeness (Part 2)
Lecture 3.1: Abstract Reduction Systems: Introductory Examples
Lecture 3.2: Abstract Reduction Systems: Confluence and Normal Forms
Lecture 3.3: How does induction really work? Or: Excursion on Induction, Isabelle, Idris (Part 1)
Lecture 4.1: Excursion on Induction, Isabelle, Idris (Part 2)
Lecture 4.2: Abstract Reduction Systems: Termination
Lecture 4.3: Abstract Reduction Systems: Termination (Finitely Branching Systems)
Lecture 5.1: Excursion on the rules of logic
Lecture 5.2, 6.1: Abstract Reduction Systems: Termination (Lexicographic Orderings)
Lecture 5.3: Invariants
Lecture 6.2-6.3: Normalisation by Evaluation
Lecture 7.1-7.3: Hoare Logic
Lecture 8.1: Wrapping up Hoare logic plus an excursion on the mathematics of software engineering
Lecture 8.2-8.3: Universal Algebra: Abstract Data Types
Lecture 9.1: Structure Preserving Maps
Lecture 9.2-10.1: Universal Algebra: Termalgebras, Homomorphisms, Initiality, Induction
Lecture 10.2: Universal Algebra: Variables, Free Algebras, Equations
Lecture 10.3 Term Rewriting
Exercises: Exercises are a preparation for the final exam and should be solved by all students.
Index on mathematics
Appendix on Jargon
Appendix on Big Ideas
Appendix on Programming Languages
What is still to come? A list of loose ends and possible topics to cover