CMSI 585: Quiz 4 Preparation

When

Last 15 minutes of class on Monday, August 3, 2026.

Everyone takes the exam at the same time.

Scope

Type Theory, Lambda Calculus, and Language Theory basics.

Ground Rules

You will take the exam on paper. There is a 15 minute time limit.

You may bring two sheets of paper with notes written on both sides (4 sides).

Preparation Checklist

Do each of the following to maximize your preparation:

Review the recordings for class periods you missed, and for portions of the class sessions that you attended but feel you need to review.
Work through the course notes on Type Theory, Lambda Calculus, and the initial sections of Language Theory (up to but not including Generative Grammars).
Watch the embedded videos in the course notes above. ALL OF THEM.
READ THE PROPOSITIONS AS TYPES PAPER BY PHILIP WADLER
Follow some of the links within the course notes to outside articles and videos. This gives you access to new material as well as additional takes on the course content.
Practice with the recall questions on the notes above.
Do as many of the practice problems from the sections on Type Theory and the Lambda Calculus as you can.

Were you able to check off every box?

Outline of Course Content

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.”

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 (Part 1)
    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

About the Problems

This is a timed mini-quiz which tests for immediate understanding of topics and not your ability to work out problems over an extended duration of time. There will be 5–10 questions. Some may be multiple choice, multi-select, matching, and very short answer.

Watch the course Slack channel for announcements regarding the focus of specific 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!