Foundations of software
CS-452
Lecture 1: Logistic, Proof Principles, Abstract Syntax and Abstract Machine
Description
Summary of the lecture to remember what it was about during the exam period:
This first lecture introduced how we'll study programming languages as mathematical objects. We learned that we need three main mathematical tools: functions (which map each input to exactly one output), relations (which are more general connections between elements), and inductive definitions (ways of building up sets of things from simple rules).
The lecture showed how to use these tools by working through several examples. We saw how to define the terms of a language inductively (the syntax), how to give an operational semantics to a tiny arithmetic language inductively and how to define functions recursively (where a function uses itself in its own definition). We learned why we need to be careful to make sure such definitions make sense.
The key technique introduced in this class was induction, which lets us prove properties about all possible objects of an inductive definition by considering simple base cases and then showing how the property carries over to the compound cases. We practiced this by proving things like "the number of constants in a program is at most its size," which helped us understand how mathematical proofs work in programming language theory.
The course will use Lean4, which is both a programming language and a proof system, to help us work with these concepts practically. The last part of the lecture covered the examples presented in the lecture in a live-coding session.