cs103l
cs103l

cs103l is a CS theory class designed over a long period of time with college roommate Lucas Garron. It was intended to fill a void in the current Stanford CS curriculum.

The class can be summarized as "uncomputability and unprovability". The course description was: Topics in mathematical logic introduced from a computer science perspective, focused around unprovability and uncomputability. Gödel’s incompleteness theorems and the Church-Turing Thesis as limits in various models of computation: Turing machines, lambda calculus, and recursive functions. Formal systems, models, provability, consistency, and completeness. Fixed-point theorems and paradoxes. Connections and implications for computer programs.

This video I made illustrates sample content from Week 6, Lecture 2.

The following was our syllabus:
 • Week 1: Proof Systems
    • Lecture 1: Introduction, Axiom Systems, and Theorem Space
    • Lecture 2: Math vs. Metamath
 • Week 2: Syntax and Semantics
    • Lecture 1: Syntax and Semantics
    • Lecture 2: Interpretations on Systems
 • Week 3: Formal Systems
    • Lecture 1: Models
    • Lecture 2: Compactness, Completeness, and Consistency
 • Week 4: Preparation for Incompleteness
    • Lecture 1: Gödel-numbering
    • Lecture 2: Proof-pairs
 • Week 5: Incompleteness
    • Lecture 1: Fixed Points
    • Lecture 2: Constructing Gödel’s sentence G
 • Week 6: Turing Machines
    • Lecture 1: Turing Machines, the Busy Beaver function
    • Lecture 2: Incompleteness/Uncomputability in Turing Machines
 • Week 7: Primitive Recursive Functions and Recursive Functions
    • Lecture 1: Recursion Theory
    • Lecture 2: Incompleteness/Uncomputability in Recursive Functions
 • Week 8: Lambda Calculus
    • Lecture 1: Lambda Calculus
    • Lecture 2: Incompleteness/Uncomputability in lambda calculus
 • Week 9: Theory of Programming
    • Lecture 1: Programming Languages as Proof Systems
    • Lecture 2: Syntax and Semantics in Programming Languages
 • Week 10: In Practice
    • Lecture 1: Uncomputability and You: A Programmer's Guide to Modest Intuitions
    • Lecture 2: (buffer slot)


We had the following homework plan:
  1. Programming Assignment: Proof Search
  2. Problem Set: Semantics and Provability
  3. Programming Assignment: Higher-Order Quines
  4. Problem Set: Models of Computation

To see lecture slides, e-mail me or Lucas Garron.

cs103l was never finished, and is currently on hiatus, to be resumed at an indeterminate point in the future.