Last hour of class on Wednesday, August 5, 2026.
Everyone takes the exam at the same time.
The final is technically cumulative, but 75% of the focus will be on material since the midterm, namely type theory, lambda calculus, language theory, and programming language elements, syntax, and semantics.
You will take the exam on paper. There is a one hour time limit.
You may bring four sheets of paper with notes written on both sides (8 sides).
Do each of the following to maximize your preparation:
Were you able to check off every box?
The fact that active recall is better for acquiring long-term knowledge does not mean that outlines and concept maps are not useful. Learners should use multiple techniques—think “both and” rather than “either or.”
Foundations of Computer Science
Computer Science is the study of:
Information
Computation
Automation
Why have foundations
Five major areas of CS foundations
Information
Shannon
Entropy
Bit
Computation
Ishango Bone
Numerals
Egyptian
Arabic
Ancient texts
Babylonian
Rhind
Euclid
Al-Khwarizmi
19th and 20th century
Babbage
Boole
Turing
Church
Limitations of computation
Automation
Automation vs computation
Early devices
Astrolabe
Antikythera Mechanism
Pascaline Calculator
Jacquard Loom
Babbage’s engines
Ada Lovelace
ENIAC
Language
Three views:
Mathematical: Formal Languages
Cultural: Human Linguistic
Engineering/Statistics: LLMs
People
Booth - assembly language
Hopper - high level languages
McCarthy - Lisp
Liskov - CLU
Implementation
Human-computer interaction
Logic
Sneak peak only this early in the class
Theories of Computation
What is a theory?
Organized body of knowledge with explanatory and predictive power
Why study theory?
To have a vocabulary for communication
To reason from more fundamental and precise principles
To predict and generate new knowledge
To not flail and guess and have our thinking stuck in a box
Big questions in computer science
What is computation?
What can and cannot be known through computation?
What can and cannot be computed?
What can and cannot be efficiently computed?
Language Theory
Definition: how computations are expressed
Symbols
Alphabets
Strings
Languages
Functions
Automata Theory
Definition: how computations are carried out
Early computing machines
How and why Turing came up with his machine model
Representing a Turing Machine as a table
Representing a Turing Machine as a state diagram
Computability Theory
Definition: what computations are (theoretically)possible
Why not every function is computable
The simple counting argument: there are more functions than programs
Church-Turing Thesis
The Halting Problem
Complexity Theory
Definition: what resources are required for computations
Kinds of computability measures
P vs. NP
Logic
What it deals with
The central question of logic
Basic notation
Encodings of various English statements
Terms vs Formulas
Term world: objects, functions
Formula world: predicates, connectives, quantifiers
Syntax of logic terms and formulas
When can we elide parentheses?
Variables
Free vs bound variables
Scope of quantifiers
Judgments
Difference between judgments and formulas
Notation
Hypothetical judgments
Logical arguments
Based on judgments, not formulas themselves
Validity
A catalog of different types of Logics
Bivalent
Propositional
Syllogistic
Predicate
First-order
nth-order
Higher-order
Classical
bivalent
excluded middle
non-contradiction
monotonic entailment
conjunction commutativity
lots of duals
Intuitionistic
Proof over truth
Constructive
No excluded middle
No indirect proof
No double negation elimination
Paraconsistent
No explosion
Relevance
Premises and conclusion must be related
Many-valued
Catuṣkoṭi
Four corners
True, False, Both, Neither
Aggi-Vacchagotta Sutta
Yeah-No and Mu
Free (not covered on any exam)
Non-monotonic (not covered on any exam)
Fuzzy
Modal
Alethic
Deontic
Epistemic
Doxastic
Temporal
Dynamic
Formal Logic
Logical System = Formal System + Semantics
Formal System
Syntax
Symbols
Formation rules
Proof system
Axioms
Inference rules
Derivability (Proof)
Semantics
Truth-conditional semantics
Model-theoretic semantics
Examples
Propositional logic
First-order logic
Q0 logic
Modal logic (formalization not on any exam)
Satisfiability and Validity
Satisfiability: is there a model that makes the formula true?
Validity: is the formula true in all models?
Metalogic
Soundness
Completeness
Consistency
Decidability
Foundations of Mathematics
Why they are important
Backstory for why they had to develop
Three schools of thought
Logicism
Formalism
Intuitionism
Differences between set theory, type theory, and category theory
Key philosophical differences
Key features of each
Key concepts behind each
Characteristic notations
Applications
Mathematical objects
Booleans
Numbers
Different ways to classify numbers
Operations, including tetration and pentation
Understanding logs
A sense of big numbers
Cardinal and ordinal infinities (WATCH THE VIDEOS)
Pairs
Tuples
Important: these are just nested pairs
Sets
Lots of notation!
Relations
How to write them
Composition ("after")
Reflexive, symmetric, transitive, antisymmetric, asymmetric, irreflexive, etc.
Functions
Notation
Naming
Sugars
Iteration
Composition ("after")
Similarities to relations
Sequences
Functions from natural numbers to the things in the sequence
Lists
Constructed from [] and ::
Not the same as sequences, but similar
Characters
Unit of textual information
Has name and code point
Strings
Just a list of characters, that is the definition
Maps
Similar to functions, but with restricted domain
No real computation to get the value at a key
Others
Graphs, Vectors, Matrices, Tensors, etc.
Encoding of mathematical objects
Basic ideas of set theory encodings
EVERYTHING is a set (wild!)
Basic ideas of type theory encodings
Construction rules
Look like logical arguments (this will turn out to be not a coincidence)
Math vs Computation
Where the two fields diverge
Why Type Theory is a better foundation for computation than Set Theory
Set Theory
What is a set?
Why use sets for foundations?
History
Frege
Russell (Russell's Paradox)
Different formalizations
ZFC - the big one
NBG - introduced classes
NF - stratified comprehension
Basic notation
element of (∈)
subset of (⊆)
Axioms of ZFC
Empty set (∅)
Extensionality
Pairing
Union
Power set
Infinity
Foundation
Replacement
Separation
Choice
Encodings of mathematical objects
Natural numbers
generated as in the Axiom of Infinity
Booleans
false is 0
true is 1
The set of all booleans is 2
Ordered pairs
(a,b) = { {a}, {a,b} }
Tuples
(are really nested ordered pairs)
Relations
encoded as sets of ordered pairs
from domain and codomain
subset of powerset of the product of domain and codomain
ambiguity of R² = R o R vs. R² = R x R
Functions
relations with the functional property
Injections
Surjections
Bijections
Sequences
functions with domain the natural numbers
Lists
empty list is the empty set
non-empty list is a pair of an element and a list
Characters
encoded as the code point of the character
Strings
list of characters
Maps
functions
Integers
sets of pairs of natural numbers with the same difference
Rational numbers
set of pairs of integers with the same ratio
denominator must be positive
Real numbers
defined as Dedekind cuts of rational numbers
Cardinals
Finite vs. Infinite
Diagonalization
Countable vs. Uncountable
Cantor’s Theorem
Ordinals
Von Neumann ordinals
Type Theory
What is it
Characteristic notation x:t
Logic emerges from type theory
Inductive definitions
Booleans
Natural numbers
Integers
Rationals
Fixed size numbers
Products (pairs)
Unit
List
Unicode
More custom types
String
Option
Void
Function types (NON-INDUCTIVE)
Notation
Matching syntax
Naming functions
Examples from arithmetic and logic
Composition of functions
Integers
The cond function (important for the exam)
Sugar
List functions
Type inference
Polymorphism
Partial functions
Subtypes
Unions
Intersections
Sums, products, and exponents
Sets
Equality
Not for free in Type Theory
Real numbers
How the formation rules have to be restricted to avoid paradoxes
Well-foundedness
Strict positivity
Dependent types
What kind of types are dependent types
Dependent types vs. polymorphic types
How to define vectors and matrices with dependent types
Why dependent types are useful
Dependent function types and their notation
Dependent pair types and their notation
Propositions as types (Read the Wadler paper and watch the two videos)
Curry-Howard correspondence
Propositions as types
False-Void
True-Unit
And-Product
Or-Sum
Implies-Function
Forall-Dependent function type
Exists-Dependent pair type
Proofs as programs
Universes
Why Type:Type is a problem
Stratification of universes
Cumulativity
Typical ambiguity
Brief History
Russell
Church
System F
MLTT
Andrews
CoC
HoTT
What Church’s and Andrews’ systems look like
The Lambda Calculus
What is it
Why was it created
Characteristic notation
Why it matters
The syntax of the lambda calculus
Variables
Constants (if applied, not pure)
Abstraction
Application (the only form that is not a value)
Parentheses can be removed in certain cases
Conversions
Alpha conversion
Beta conversion
Eta conversion
How to avoid capture and escape
Free vs bound occurrences
Defining proper substitution
Reduction
Redexes
Normal forms
Church-Rosser property
CBV vs CBN
NORS vs AORS
Lambda expression in various programming languages
Pure Lambda Calculus
How to define booleans, numbers, and lists
Recursion
Fixpoints
Y Combinator
Combinators
Typed Lambda Calculus
When types are needed
What types restrict us from saying
Lambda Cube (not on the exam)
Language Theory
Why a theory of language would be nice
Basic definitions of syntax, semantics, pragmatics
Symbols
Alphabets
Strings
length
empty string
concatenation
reversal
substring
Kleene star (important)
The set of all possible strings over an alphabet is enumerable
Formal Languages
Definition: a set of strings over an alphabet
Utterance
Operations
Two ways to define syntax
By generation
By recognition
Generative Grammars
Notation
Derivation
Parse trees
Predefined variables
Ambiguity
Formal Definition
Restrictions
Type 0: unrestricted
Type 1: context-sensitive (essentially noncontracting)
Type 2: context-free
Type 3: regular
Chomsky Hierarchy
Other kinds of grammars
Linear
Regular expression notation
Analytic grammars
Notation
Semantics
Simple case study
PLT
Applications of Language Theory
The Study of Programming Languages
Greetings in several human languages
Sum of even squares in multiple programming languages
Why study PLs
How to study PLs - the six dimensions
History
Language diversity
Impactful languages
Why languages were created
Language-independent concepts
Definitions
Statics and Dynamics
Big Questions
Ontologies
Naming
Evaluation
Control Flow
Types
Functional Abstraction
Modularity
Concurrency
Metaprogramming
Foundational theories (logic, math, information, computation)
Logic
Foundations of Math
Set Theory
Type Theory
Category Theory
Computation Theories
Syntax
Semantics
Pragmatics
Language Vision and Values
Evaluation
Technical Criteria
Nontechnical Criteria
Expressiveness
Tradeoff Analysis
Implementation
Programming Language Elements
Values
Numbers
Symbols
Characters
Tuples
Sequences
Strings
Records
Sets
Dictionaries
References
Null - the trillion dollar mistake
Types
Entities
Literals
Declarations
Expressions
Statements
Functions
Generators
Classes
Modules
Behaviors
Control Flow
Sequencing
Selection
Iteration
Nondeterminism
Disruption
Concurrency
Syntax
Motivation
Choices in language design for syntax
Definition
Identifiers, entities, keywords, reserved words
Syntax Diagrams
Ovals vs rectangles
Lexical vs Phrase syntax
Lexical nodes for characters and tokens
Tokens
Phrase nodes for phrases
Parse trees
Ambiguity
Precedence
Associativity
Programming Language Grammars
Analytic Grammars
Context
Abstract Syntax
Tree Grammars
Two styles
Multiple concrete syntaxes for the same abstract syntax
Real-world syntax
Alternate syntax descriptions
BNF
EBNF
ABNF
Semantics
Approaches
Informal
Formal
Operational
Denotational
Axiomatic
Whatever the interpreter does
Context
Context-free syntax or static semantics?
Statics vs Dynamics
Semantics in Practice
Operational Semantics
Concrete: translate it to a low-level machine
SOS (small-step)
Natural Semantics (big-step)
Case Study: Astro
Case Study: Bella
Language Features
If statements
Parallel assignment
Swap
Repeat-until
Repeat-n-times
For loops
Nondeterminism
Concurrency
Types
Strong typing (typing violations are errors)
Static typing (checking before execution)
Denotational Semantics
What it is
Semantic functions
Loops require fixpoint semantics
Domain theory
Complete partial orders
Least upper bounds
Continuous functions
Fixpoints
Errors
Continuations
Language Features
If statements
Parallel assignment
Swap
Repeat-until
Repeat-n-times
For loops
Nondeterminism
Concurrency
As a timed exam, the problems will be mostly focused on measuring your immediate fluency with the material rather than working out complex multi-step problems.
That said, to encourage preparation, several of the questions on the exam will come from the course Practice Problems. Work on these problems with friends before the exam. You’ll have some pre-solved!
Here’s the focus for each of the problems:
All content on the assigned readings is fair game for questions, so do not neglect the readings, and by all means do the recall questions!