"The great idea of constructive type theory is that there is no distinction between programs and proofs... Theorems are types (specifications), and proofs are programs" (Robert Harper)

This is a collection of modern resources on various undergrad level computer science topics, for someone with an interest in theory. Use LibGen if you can't buy these books. You don't have to do everything here, just the topics of interest to you. If for any reason you want a condensed version, watch the Great Theoretical Ideas in Computer Science lecture series to see what interests you in the field. Almost all the material in each resource is self contained so will cover necessary background which if you don't have see the preliminaries.

How to Learn

On Isaac Newton's iteration method to self-learn geometry:

"He bought Descartes' Geometry and read it by himself .. when he was got over 2 or 3 pages he could understand no farther, than he began again and got 3 or 4 pages father till he came to another difficult place, than he began again and advanced farther and continued so doing till he made himself master of the whole without having the least light or instruction from anybody" (King's Cam.,Keynes MS 130.10,fol. 2/v/)

Cal Newport has some anecdotes on how he was able to get the best grade in his Discrete Mathematics class, and the rest of the site is full of advice on studying, how to schedule yourself and deliberate practice. Further anecdotes exist on the importance of deep work and deliberate practice. There is a free course Learning How to Learn on which suggest the same techniques plus Cornell style note taking and how to read a research paper.


Everything here is optional, you could try just starting with CS 3110.

Intro to Computation

The book How to Design Programs (HtDP) has proven success teaching an introduction to programming while remaining rigorous. One of it's authors is now running a public school curriculum project called Bootstrap and gave a talk why this style of teaching programming has the most success, and how it's curriculum transfers to other fields such as how the students writing games are actually writing differential equations, as the behavior of a game over time is the integral. If you really want to understand programming you should start with this book. If you liked HtDP, it's sequel is PAPL (original Racket version also exists, but Pyret and Racket are essentially the same languages just the author was tired of parenthesis complaints from other professors). A very rigorous introduction exists as the classic MIT book Structural Interpretation of Computer Programs (SICP) but the more programming you do before reading SICP, the more you get out of it.

Some Additional Optional Intros

Common Lisp Intro

It's possible to do (or at least model) every course in this list using Common Lisp, such as building your own domain-specific machine code while completing 15-213 Computer Systems, or hacking together purely functional data structures, or writing your own pattern matcher, or simulating a turing machine, ect. Of course you will do the courses using their recommended languages and tools, but in addition to this, building your own toy prototypes for the topics here in Lisp can help you learn this material as you discover it for yourself with active learning. Another shill for Common Lisp as a good language choice is it hasn't changed much in decades, so an old library you found that hasn't been updated in 15 years will still work. There is also the joy of programming Lisp as a system.

Little Schemer Series

The Little Schemer series books are a Q&A format/Socratic method for learning the basics of computation (read the Preface of each book). You can do the Little Schemer with pencil and paper in a weekend though the authors recommend at least 3 sittings. The first in the series is The Little Schemer which teaches you to think recursively. The second is the Seasoned Schemer covering higher-order functions, which will help understand calculus. The differential operator is a higher-order function: given a function on the real line it yields its first derivative as a function on the real line.

Carnegie Mellon University

Students with direct entry to this CMU course already have a background in programming. Good information here on style, design and efficiency, with an introduction to complexity otherwise you would learn all of this in HtDP.

Elementary Math

"So I went to Case, and the Dean of Case says to us, it's a all men's school, "Men, look at, look to the person on your left, and the person on your right. One of you isn't going to be here next year; one of you is going to fail." So I get to Case, and again I'm studying all the time, working really hard on my classes, and so for that I had to be kind of a machine. In high school, our math program wasn't much, and I had never heard of calculus until I got to college. But the calculus book that we had was (in college) was great, and in the back of the book there were supplementary problems that weren't assigned by the teacher. So this was a famous calculus text by a man named George Thomas (second edition), and I mention it especially because it was one of the first books published by Addison-Wesley, and I loved this calculus book so much that later I chose Addison-Wesley to be the publisher of my own book. Our teacher would assign, say, the even numbered problems, or something like that (from the book). I would also do the odd numbered problems. In the back of Thomas's book he had supplementary problems, the teacher didn't assign the supplementary problems; I worked the supplementary problems. I was scared I wouldn't learn calculus, so I worked hard on it, and it turned out that of course it took me longer to solve all these problems than the kids who were only working on what was assigned, at first. But after a year, I could do all of those problems in the same time as my classmates were doing the assigned problems, and after that I could just coast in mathematics, because I'd learned how to solve problems" (Don Knuth )

I bought George Thomas' Calculus and Analytical Geometry 3rd edition for around $12 off Thrift Books and can see why Knuth liked this book so much as Thomas carefully goes through each proof describing what is happening. The second or classic edition is the one Knuth used and was reprinted recently. There's a review of trigonometry in the 3rd edition as well.

Nonexistent Math Background

The Gelfand Correspondence Program in Mathematics existed in the 90s, where students were sent books and could mail back assignments to be graded and coached. These books are still around and are excellent taking a problem solving approach on every page. Algebra and Trigonometry are both recommended. While you go through any of these books try a survey of The Better Explained Math and Calculus series books, which explain basic math such as the natural logarithm. Gilbert Strang also has a lecture series Highlights of Calculus. Cambridge also offers advice for incoming undergrads on readable texts.

Weak/Forgotten Math Background

Start with Po-Shen Loh's new site which presents topics in a brief intuitive manner, then feeds you problems in that domain and makes decisions based on your answers if you need more practice problems. The Advanced Topics have all kinds of great tutorials on CS Theory as well as Number Theory.

Calculus With Theory

Optional, Thomas' text will teach you the theory of calculus, though doing the exercises of Apostol's Calculus I is a great way to build mathematical maturity. This alternative Calculus w/Theory lecture series only uses a simple algebraic framework, eliminating limits/infinity. Linear algebraic ideas and the Discrete Calculus are both highly relevant to the material here. There is also a full course available.

Functional Programming

Principles of Functional Programming

The 2012 version by Dan Licata has the best lecture notes, optionally combine with most recent course notes. Robert Harper keeps a blog and a follow up post on the success of teaching this course. SML is used because it's syntax and module system is simple, much like Scheme's easy syntax was once preferred for introductory courses so the complexity of the language gets out of the way and you learn the fundamentals.

Intro to Programming using OCaml

This Cornell OCaml course is totally self contained with it's own textbook. You will want to archive the entire course locally using wget. The release code for the assignments wget them here and change URL to /a4/, /a3/, they range -


It is possible in a functional language like ML to do algebra with types, proving two types are isomorphic with the desired properties of reflexivity, symmetry, and transitivity. It's also possible to abstract Lists and Trees into polynomials, as every polynomial looks like a sum of terms. As you will learn in 15-150 Principles of Functional Programming "most functional datastructures have constant time access near the outer layer of their structure, ie: the head of a list or the root of a tree. However, access at some random point inside the structure is typically linear since looking at some element of a list is linear in the length of the list, and looking at some element of a tree is linear in the depth of the tree. Datatype derivatives allow constant time access to the entire structure."

Linear Algebra

Abstract Algebra

Discrete Mathematics

Resources to learn undergrad Discrete Mathematics.

Introduction to Pure Mathematics

Discrete Math with Standard ML

The merging of proof and program is what makes this a great book. If you can't get this book Discrete Mathematics, by L. Lovász, J. Pelikán, and K. Vesztergombi is normally used or just skip to 15-251 Great Theoretical Ideas in CS. If you can finish this book you've essentially done most of 15-150 Principles of Functional Programming (such as proving programs correct) and most of 15-215 Great Theoretical Ideas in Computer Science.

Great Theoretical Ideas in Computer Science

This is a crash course in multiple topics such as Probability, Linear Algebra, Modular Arithmetic, Polynomials, Cryptography and Complexity Theory. 15-251 assumes students have completed An Infinite Descent into Pure Mathematics though it is self contained. "This course teaches the mathematical underpinnings of computation and explores some of the central results and questions regarding the nature of computation."

Computer Systems

"[Computer science] is not really about computers - and it's not about computers in the same sense that physics is not really about particle accelerators, and biology is not about microscopes and Petri dishes...and geometry isn't really about using surveying instruments. Now the reason that we think computer science is about computers is pretty much the same reason that the Egyptians thought geometry was about surveying instruments: when some field is just getting started and you don't really understand it very well, it's very easy to confuse the essence of what you're doing with the tools that you use." (Hal Abelson)

This covers computer architecture from a programmer's perspective, such as how to write cache friendly code, and other optimizations for the x86-64 arch. You learn how to manually write loops in assembly and see how recursion works at a lower abstraction. You learn machine code instructions, how compilers work, return oriented programming (ROP) to bypass stack protections, the memory hierarchy, and networks. You could read K&R's The C Programming Language for a brief intro, though this course will explain C as you go anyway and fully covers pointers at the assembly language level making it self contained.

Designing Systems

Knuth constructed a futuristic architecture with 256 registers for his Art of Computer Programming series to make hacking around with experimental systems programming easier. If you ever find yourself implementing instructions for something (webAssembly devs) you should read through MMIX documentation, for gems like MOR/MXOR.


Search or sci-hub for additional papers or books on parsers/compilers.

Database Systems

Interesting post on the future of database systems by Andy Pavlo.

Practical Data Science

Meta-Linguistic Abstraction

A classic introductory computer science book on thinking about the big picture of programs with abstraction: finding general patterns from specific problems and building programs based on these patterns. An applied example of this is the package manager GNU Guix and distro GuixSD, which is a GNU implementation of the NixOS functional software deployment model. Package builds, including entire system builds, are declared in one text file. The resulting software deployment is functional: build inputs go in such as compilers, customizations, environments ect, and a reproducible, immutable build comes out with a hashed identifier meaning you can do roll backs to previous successful builds. A recent GUixSD feature gexp (g-expressions) is a good example what can be achieved through syntactic extensions of the Scheme language.

You are more likely to benefit from this book after having some programming experience, but no matter what level of programmer you are you'll still benefit from SICP.

Natural Language Processing

Programming Language Theory

Read these reasons for studying programming languages.

Isolating Software Failure, Proving Safety and Testing

How to verify software, and strategies of programming that minimize catastrophe during failure. The Little Prover is a good introduction in determining facts about computer programs. Prof Rob Simmons can be hired as a tutor to teach you Coq, the curriculum follows the Software Foundations book series below.

Physical Systems Software Security


Introduction to Parallel and Sequential Algorithms

Unlike a traditional introduction to algorithms and data structures, this puts an emphasis on thinking about how algorithms can do multiple things at once instead of one at a time and ways to design to exploit these properties. It uses a language based analysis model to estimate complexity for abstractions such as garbage collection.

Advanced Algorithms (Purely Functional Data Structures)

The typical text for a senior undergrad or graduate course on algorithm analysis is The Design and Analysis of Algorithms by Kozen (1992). This is an excellent book to study with difficult problems well presented and clearly analyzed by Kozen. The Okasaki book (1999), Purely Functional Data Structures gives examples in Standard ML and Haskell.

Complexity Theory

Undergraduate Complexity Theory

Expands on the lectures in 15-251.

Graduate Complexity Theory

You may want to try solving some of the problems in this domain.

Useful Math for Theoretical CS

These scribed lecture notes give you a diverse background in math useful for theoretical CS, from the excellent book The Nature of Computation such as these slides from A Theorist's ToolKit which describe how to find research, how to write math in LaTeX, how to give a talk, resources on math.overflow ect.

Introduction to Quantum Computing

This is a graduate introduction to quantum computation/information theory, from the perspective of theoretical computer science.


This service matches your skills to people who want to pay you. Jane Street Capital is a finance tech company that hires functional programmers worldwide, you may want to apply there. There are numerous opportunities to apprentice as a security researcher or get paid to prove business logic programs like 'smart contracts'. Check your local university employment listings as well, often students do not take these jobs as they are off chasing that startup stock options payday or doing industry internships, plenty of opportunities to work with post-doc researchers writing algorithms or analyzing data. For web programming there exists free programming notes for software like NodeJS, which you can write software for in OCaml by compiling it into JS with bucklescript or compile to web assembly.

Graduate Research in Type Theory

Read these slides from A Theorist's ToolKit on how to find research, how to write math in LaTeX, how to give a talk, where to ask on stackexchange ect.

Basic Proof Theory

Intro to Category Theory

Type Theory Foundations

Higher Dimensional Type Theory

Start with this talk A Functional Programmer's Guide to Homotopy Type Theory with intro to Cubical Type Theory

Further Research

Graduate Research in Machine Learning/AI

Read these slides from A Theorist's ToolKit on how to find research, how to write math in LaTeX, how to give a talk, where to ask on stackexchange ect.

Graduate Introduction to General AI

These notes here cover more topics, such as Computer Vision/NLP/AGI and follows AI: A Modern Approach book by Norvig. The 15-780 course is specific to some topics in AI providing them 2-3 lectures each.

Math Background for ML

A series of recorded lectures and recommended texts for a crash course in the Math background for ML introductory courses

Statistics Theory

Graduate Introduction to ML

Advanced Introduction to ML

Convex Optimization

Deep Learning

If you're interested in parallel GPU programming for training see these lectures and notes.

Algorithms for Big Data

Further Research

Graduate Research Elective: Cryptography

Read these slides from A Theorist's ToolKit on how to find research, how to write math in LaTeX, how to give a talk, where to ask on stackexchange ect.

Graduate Cryptography Intro

This course covers post-quantum crypto, elliptic curve crypto, and is taught by premiere researcher Tanja Lange (TU/e)

Applied Cryptography

Future Research