# A 2024 Computer Science Curriculum

## Table of Contents

## Welcome

This is a deep dive into what Robert Harper calls The Holy Trinity of the theory of computation. It gives you a framework for discovery and analysis of anything computer science related so this isn't only a programming language theory curriculum. If you want to learn this material with a community some anons have started a Discord channel.

### Stuff we have access to

The categories course has recorded lectures but the lecture notes are high enough quality they can be used as a workbook. You don't have to do everything here obviously take only what you want.

#### Functional Programming

- 15-150 Principles of Functional Programming and Programming with Categories
- We finally have access to the recorded lectures
- Older Assignments & labs can be grabbed from here and here
- TAs also wrote helpful docs for the course
- We can also try whatever current version of hype for types

They are going to fully mechanize 15-210 soon using calf/decalf to prove costs.

- 15-210 Parallel & Sequential Algorithms
- Some recitations/review videos here but we won't need them
- The hw/labs can be found here or here or search github for more
- Or use competitive programming sites like Kattis or CodeForces (OCaml, Haskell, F# etc)
- There's also Functional Data Structures by Prof Ragde

#### Math & Constructive Logic

Classic mathematics is 'element oriented' studying everything through the lens of sets while category theory is 'function oriented' zooming out to the big picture and studying functions and their transformations.

- Discrete Math using Lean
- MIT course Applied Category Theory
- Constructive Logic w/assignments in SML

#### Type Theory

We can take the PFPL book with the HoTT book/course

*Practical Foundations for Programming Languages*book and supplementary materials- Robert Harper OPLSS 2021 lectures and some earlier OPLSS lectures for his book
- We have access to some 15-312 assignments but the exercises in PFPL are hard enough

- 15-819 Homotopy Type Theory and book
- Described as a 'misadventure in formalisms' but explains how univalence works, higher types

#### Some optional topics:

Networks

- Project that Robert Harper calls the greatest and most ignored idea how they designed a network protocol stack in SML by combining two modules that share specs/cohere (a pullback)
- Network Programming OPLSS lectures by Nate Foster a comprehensive intro to network programming

Program transformation

- A very detailed rewrite of the regex matcher we use in 15-150 for proof directed debugging but now with efficient backtracking

#### Research

Robert Harper once spent an entire week reading the source of an operating system to find out in complete detail exactly what happened when he pushed a button on his keyboard how it ended up transformed as pixels on his screen. His advice to grad students is to develop a point of view so when you start a project articulate exactly why it's worthwhile and keep this perspective when you are deep into every technical detail.

What we need to know:

- The PLAi workbook to learn the standard model of most languages you've heard about
- How to use Agda though practicing with Lean will make this easier
- The Edinburgh Logical Framework or LF
- One of those mandatory technical details we have to know
- Created to make it easier to mechanize proofs in an assistant and for more readable notation

- A few Per Martin-Lof papers and Programming in MLTT
- Most of the seminars from OPLSS 2015 curriculum combined with the OPLSS 2012 lectures
- Many proof theory topics also here with assignments in SML

- Robert Harper OPLSS 2011 or 2010 lectures on logical relations that teach this subject from scratch
- There's now logical relations as types or ParamTT they are highly versatile

Finally OPLSS 2018 lectures/draft book on Computational Type Theory and whatever research is going on these days like cartesian cubical type theory and dive into this reading for some categorical logic. There's other research if you prefer for example OPLSS is filled with session-typed concurrent programming seminars by Stephanie Balzer (Rust, Erlang) and you can read the Brown University experimental rewrite of the Rust book to make the often confused concept of ownership easier to understand.

## BEGIN

I'm going to start with the book *The Mechanics of Proof* because 15-150 will assume we know some of this as most CMU students will be taking 15-151 at the same time as 15-150.

- Workbook The Mechanics of Proof Fordham 2023
- See these install instructions
- There's many demos on YouTube by the author Heather Macbeth

#### Local install

Gitpod free tier is easiest. To install Lean locally w/Visual Studio:

- install Lean
- install git
- install code (Visual Studio code) though I use emacs see below
- in terminal type: git clone https://github.com/hrmacbeth/math2001.git
- cd math2001
- in terminal: lake exe cache get
- it downloads 3972+ files (wtf)

- 'code .' to start from present directory
- install lean4 extension

Click on 01ProofsbyCalculation.lean you should get a right panel opening up in VS code called 'Lean Infoview' that displays tactic state goals and all messages.

#### Emacs

Install everything as before then git clone lean4-mode, paste the readme elisp into .emacs or init.el file, restart and open any .lean file. Ctrl-c Ctrl-i opens the lean view in a new window showing goals. If you use vanilla emacs from some distros like Ubuntu you'll have some 'can't verify signature' error which is fixed by updating elpa keyring.

Another way is with gpg:

gpg --homedir ~/.emacs.d/elpa/gnupg --list-keys /home/x/.emacs.d/elpa/gnupg/pubring.kbx ----------------------------------------- pub dsa2048 2014-09-24 [SC] [expired: 2019-09-23] CA442C00F91774F17F59D9B0474F05837FBDEF9B uid [ expired] GNU ELPA Signing Agent (2014) <elpasign@elpa.gnu.org> pub rsa3072 2019-04-23 [SC] [expires: 2024-04-21] C433554766D3DDC64221BFAA066DAFCB81E42C40 uid [ unknown] GNU ELPA Signing Agent (2019) <elpasign@elpa.gnu.org> pub ed25519 2022-12-28 [C] [expires: 2032-12-25] AC49B8A5FDED6931F40EE78BF993C03786DE7ECA uid [ unknown] GNU ELPA Signing Agent (2023) <elpasign@elpa.gnu.org> sub ed25519 2022-12-28 [S] [expires: 2027-12-27]

Update key if your second key is expired:

gpg --homedir ~/.emacs.d/elpa/gnupg --keyserver hkps://keys.openpgp.org --recv-keys 066DAFCB81E42C40

### Proving equalities

Reading 1.1 *Proving equalities* from Mechanics of Proof. Any examples you don't understand come back here after writing some Lean proofs you won't get them all immediately. First example expand out (a - b) and notice you need to add 4ab in order to balance both sides. The problem statement tells us (a - b) = 4 so (a - b)^{2} is 16 after substitution.

1.2.x *Proving equalities in Lean* the .lean files are all included in the Math2001 directory you cloned from github. I had to fight with Lean to get it to accept 1.2.4 so rewrote it exactly like she did with parens:

-- Example 1.2.4. -- Exercise: type out the whole proof printed in the text as a Lean proof. example {a b c d e f : ℤ} (h1 : a * d = b * c) (h2 : c * f = d * e) : d * (a * f - b * e) = 0 := calc d * (a * f - b * e) = d * a * f - d * b * e := by ring _ = (a * d) * f - d * b * e := by ring _ = (b * c) * f - d * b * e := by rw [h1] _ = b * (c * f) - d * b * e := by ring _ = b * (d * e) - d * b * e := by rw [h2] _ = 0 := by ring

We are using 'calc' in Lean hence the name proof by calculation. I'm guessing the underscore represents the entire left hand side of the equation indicating to the rw (rewrite) pattern matcher to ignore it. There's nothing in the documentation I could easily find but Terence Tao describes the underscore here same way.

Look at the infoview/goals it will tell you when that stage is done by 'goals accomplished', also click around various parts of the proof to see how the infoview changes:

-- Example 1.3.2 example {x : ℤ} (h1 : x + 4 = 2) : x = -2 := calc x = (x + 4) - 4 := by ring _ = 2 - 4 := by rw [h1] _ = -2 := by ring

I guessed the syntax for rationals in Lean and it worked:

-- Example 1.3.4 example {w : ℚ} (h1 : 3 * w + 1 = 4) : w = 1 := calc w = (3 * w + 1)/3 - 1/3 := by ring _ = 4/3 - 1/3 := by rw [h1] _ = 1 := by ring

1.3.11 you can use Lean to tell you when the sides have been balanced. You did it correctly if goals panel or infoview shows goals accomplished and the linter hasn't added any red squiggle lines or other errors. Some exercises I tried, you can rewrite a line using both hypotheses and eliminate a lot of steps I kept them here for illustration how Lean works:

example {u v : ℚ} (h1 : 4 * u + v = 3) (h2 : v = 2) : u = 1 / 4 := calc u = (4 * u + v)/4 - v/4 := by ring _ = 3/4 - 2/4 := by rw [h1, h2] _ = 1/4 := by ring example {u v : ℝ} (h1 : u + 1 = v) : u ^ 2 + 3 * u + 1 = v ^ 2 + v - 1 := calc u ^ 2 + 3 * u + 1 = (u + 1) * (u + 1) + (u + 1) - 1 := by ring _ = v * v + v - 1 := by rw [h1] _ = v ^ 2 + v - 1 := by ring

### Tips and tricks

1.3.2 once again we first establish x = x then use the hypothesis to rewrite it

-- Example 1.3.2 example {x : ℤ} (h1 : x + 4 = 2) : x = -2 := calc x = (x + 4) - 4 := by ring _ = 2 - 4 := by rw [h1] _ = -2 := by ring

For the rest of these examples try them yourself going through the 03TipsandTricks.lean file before looking at the solution it's the only way you learn.

-- Example 1.3.5 example {x : ℤ} (h1 : 2 * x + 3 = x) : x = -3 := calc x = (2 * x) - x := by ring _ = 2 * x - (2 * x + 3) := by rw [h1] _ = -3 := by ring

(╯°□°)╯︵ ┻━┻ if you see calc underlined with a red error it means you forgot an equal sign or _ sign in your chain of rewrites or there is an accidental character floating around in the scope out of view somewhere it took me forever to figure that out as Lean kept giving some cryptic message and I was looking at the signature.

1.3.11 exercises all use the examples we just saw. Look at 1.3.8 example when you try exercise 11 and manipulate it so a = (4 + 2) / 3.

example {x y : ℝ} (h1 : x = 3) (h2 : y = 4 * x - 3) : y = 9 := calc y = y := by ring _ = 4*x - 3 := by rw [h2] _ = 4*3 - 3 := by rw [h1] _ = 9 := by ring example {p : ℝ} (h1 : 5 * p - 3 = 3 * p + 1) : p = 2 := calc p = (5*p -3 - 3*p + 1)/2 + 1 := by ring _ = (3*p + 1 - 3*p + 1)/2 + 1 := by rw [h1] _ = 2/2 + 1 := by ring _ = 2 := by ring

TODO