Develop the simply typed lambda calculus from types and contexts to products and sums, with the syntax and lemmas needed for rigorous reasoning.

Extend PCF with unit, sum, and recursive types, and discover how a few carefully chosen constructors dramatically expand what a language can express.

Connect records and tuples to deeper questions about iteration, tail recursion, and the expressive power of total recursive functions in PCF.

What does a PCF program mean? Compare axiomatic, operational, and denotational semantics and see how each perspective defines program equivalence.

Make predictions without knowing the future by combining expert advice, from the halving algorithm to weighted majority and bounded cumulative mistakes.

Can a random walk find a satisfying assignment? Compare randomized approaches to 2-SAT and 3-SAT and analyze why the improved strategy succeeds.

Meet PCF as a compact laboratory for language theory, and learn how types, terms, functions, currying, and binding form a precise syntax.

Approximate a difficult DNF counting problem with Monte Carlo sampling, then refine the estimator to obtain a practical probabilistic algorithm.

Compare Bloom filters and cuckoo hashing to see how randomized data structures trade memory, lookup speed, relocation cost, and false positives.

Why does choosing the better of two random bins transform load balancing? Explore the balls-into-bins model and its surprising impact on hashing.