This course has been developed by Alexander Kurz and Samuel Balco for the students of Chapman University and will be taught by Alexander Kurz.
Notes and Materials for a course on Programming Languages Fall 2020 at Chapman University.
Quick links:
Acknowledgements:
The specific way we intertwine theory and practice may be original, but we build on a long tradition of teaching courses on principles of programming languages. The idea that the best way to understand how programming languages work under the hood is to learn how to build your own, goes back at least to the MIT course/"Wizard Book" by Abelson and Sussman, Structure and Interpretation of Computer Programs, which is still worth reading today. Our use of the parser generator BNFC for the language LambdaNat follows Aarne Ranta's book Implementing Programming Langugages, which forms the basis for the Programming Language Technology course at Chalmers University. We will hear more about this in our course on Compiler Construction next semester. LambdaNat itself is a lambda calculus with just enough additional syntactic sugar so that writing programs in LambdaNat is similar enough to mainstream functional programming. The way we then extend LambdaNat to our second language, LambdaFun, by adding while loops, memory allocation, assignment, and pointers is inspired by Michael Spivey's course on Programming Languages at Oxford University.
I am also grateful to my friends and colleagues from the Midlands Graduate School in the Foundations of Computing Science who have influenced with their graduate level courses from 2002 onwards the choice of material. In fact, it is one of the aims of this course to provide at the undergraduate level the foundations that will equip interested students with the knowledge needed to study more advanced topics in programming languages. Many of the paragraphs labelled "Further Study'' are meant to provide bridges to such graduate level courses.
Many thanks to all with whom I had the opportunity to discuss the contents of the course, including (but not limited to) Roy Crole, Peter Jipsen, Drew Moshier, Paula Severi, and Fer-Jan de Vries; to the students of 2018 and 19 for continuing challenge and feedback; to all the colleagues from whom I have been learning over the years.
I list some books that stood the test of time and are less technical and of wider interest, more foundational than practical. Not required reading, but great background if you like to read widely.
-
Hofstadter: Goedel, Escher, Bach. A wide ranging book bringing together history, art, music and computer science. Contains a lot of rewriting and computability theory. The reader ends up with a proof of Goedel's incompleteness theorem, without going through a technical and advanced course of logic.
-
Smullyan: To Mock a Mockingbird. Presents a deep but playful account of combinatory logic and the lambda-calculus.
-
Petzold: The Annotated Turing. Goes through Turing's famous paper line by line. Can be read from a technical point of view, but one can also browse it lightly and pick out the anecdotes.
-
Doxiadis, Papadimitriou: Logicomix. This graphical novel about the life of Bertrand Russell introduces many of the main players in the history of logic and computing in the early 19 hundreds. Co-authored by one of the most influential contemporary theoretical computer scientists.
... I'd be curious to learn about your favourites ...
While Wikipedia is a good place to gain a first impression of a new topic, a great starting point for scholarly explorations are the articles in the SEP. I link some that are useful to locate the current course in the wider landscape of mathematics, logic, philosophy, computation, history. The articles can get quite technial but even just reading the introductions will broaden horizons. A nice exercise could be to arrange the topics and protagonists of these articles into a timeline and then to attempt a short history of the most important ideas and how they hang together.
- The Modern History of Computing
- Dedekind and The Early Development of Set Theory
- Russell's Paradox and Self-Reference
- Hilbert's Program and The Development of Proof Theory
- Brouwer and Constructive Mathematics
- Alan Turing and Turing Machines
- The Lambda Calculus and The Church-Turing Thesis
- Recursive Functions and Kurt Gödel and Incompleteness Theorems
- Combinatory Logic and Computability and Complexity
- Church's Type Theory and Type Theory
- Paradoxes and Contemporary Logic
- Logic and Artificial Intelligence and Automated Reasoning
- Computational Linguistics and Typelogical Grammar
- Propositional Dynamic Logic and Temporal Logic
- Proof Theory and Proof-Theoretic Semantics
- The Hole Argument and Symmetry and Symmetry Breaking
Get in touch if you want to hear more about how these articles are related to this course.
None of this is required reading, but all of it is part of the wider landscape in which this course is situated. Many of these links are to talks, videos, articles and blogs that do not represent carefully researched peer-reviewed authoritative expert consensus. Do not take opinions for granted but as an invitation to start a discussion.
-
rise4fun has a long list of software engineering tools for program analysis and verification that you can run in your webbrowser.
-
Unison is a new programming language based on the idea of content-addressed code. Search the linked tour for "functional" to see why it is important for Unison to be a pure functional programming language. I only worked through the tour sofar, but it looks very interesting.
-
Rust's concept of Ownership strikes a balance between C-style memory allocation and Java-style garbage collection. This ideas is related to linear type systems. For more on how Rust combines imperative with functional features see eg the blog Is Rust a functional programming language?.
-
Charles Scalfani on Haskell: He writes from the point of view of a software engineer who had to learn Haskell the hard way. I first came across his article Goodbye, Object Oriented Programming. His more recent articles contain more lessons about how and why to learn Haskell.
-
Terence Tao: Compactness and contradiction. Tao is one of the leading mathematicians of his generation. Nevertheless, Chapter 1 on "Logic and foundations" of this book is quite accessible to a reader with background in computing and/or logic and it touches on many topics that crop up in this course. Highly recommended to everybody with a taste for mathematics. I found Sections 1.11 about vagueness and 1.12 about a computational perspective on set theory particularly insightful. Section 1.4 on "Stable implications" is closely related to a favourite topic of mine, namely "Mathematics as a programming language".
-
Turing Incomplete Languages. This blog illustrates a general topic: If you want a language that can express important ideas easily, you can also use this language to express rubbish easily. If you want to limit language so that it becomes impossible to express rubbish, good ideas become also more difficult to express. And then, after a while, you notice that you can still write rubbish in the restricted language anyway. (Sam Griffin in the comments has a more nuanced view on this.) So you end up making the language expressive again (unless there is a specific technical reason not to do so, such as efficient automatization (see also the last sentence of Chapter 1 of Tao's book referenced above)). Btw, in this context one should recall Turing's theorem: Every language that allows us to express all terminating programs must necessarily allow us to write non-terminating programs. One thing one should add to the article (but see the comments), is that there are actually languages, known as type theories, with powerful recursion principles in which all programmable functions do terminate.
-
Programming Languages and Machine Learning. Could that be combined with theorem proving as in the approach of Ganesalingam and Gowers?
-
Video: Modelling Pandemics in Julia features many of the topics that appear in our course.
-
Video: Visualised Recursion ... Explanation
-
Hoare's 1980 Turing Award Lecture has a lot of interesting anecdotes about Quicksort, Algol, the switch statement, early compilers, operating systems, Hoare logic. Also some valuable general lessons about software engineering. I collected some of my favourite quotes.
-
Multi-Paradigm Languages:
- Julia may well be on the way to replace Python as the language for scientific computing.
- Scala continues the success of Java but adds FP features such as higher-order functions, algebraic data types and pattern matching.
- Rust builds on the success of C, but adds features of modern languages including FP.
- ...
-
Comparing different programming paradigms. There is a raging debate about the pros and cons of different programming paradigms. Reading widely to get a lot of different views is recommended. Often the comments are the most interesting part. Here are some entry points. Was object-oriented programming a failure? ...
-
Notes on Programming Paradigms A course that shares many aims and methods with this one. I just browsed over the content, but it looks promising ... recommended if you want to have a different point of view on the same topic.
-
Videos and podcasts:
-
Bjarne Stroustrup, the creator of C++, talks about The Essence of C++.
-
Simon Peyton Jones, one of the inventors of Haskell, talks about Functional Programming Languages and the Pursuit of Laziness.
-
Bob Martin, one of the inventors of agile computing talks about the The Future of Programming.
-
Alan Kay, one of the inventors of personal computing and object-oriented programming, talks about how the invention of personal computing goes back to a project of reforming school education in Inventing the Future. "The best way to predict the future is to invent it."
-
...
-