streamcode9

To start learning MLTT-72 (Martin-Löf Type Theory from 1972), you’ll need a minimal foundation in:

  1. Basic mathematical logic - understanding of logical connectives, quantifiers, and proof techniques
  2. Set theory fundamentals - familiarity with sets, functions, and basic operations
  3. Some exposure to the lambda calculus - the notation and concept of function abstraction
  4. Understanding of the concept of types in programming languages

You don’t need deep expertise in any of these areas to begin. The most important prerequisite is comfort with mathematical notation and abstract thinking.

If you’re completely new to type theory, I’d recommend starting with:

Foundational Resources:

  1. “Programming in Martin-Löf’s Type Theory” by Bengt Nordström, Kent Petersson, and Jan M. Smith - A classic introduction that’s freely available online.

  2. “Type Theory and Functional Programming” by Simon Thompson - Available free online, provides a gentle introduction to type theory and its connection to programming.

  3. “Proofs and Types” by Jean-Yves Girard - A concise introduction to the connection between proofs and types.

Online Courses and Lecture Notes:

  1. Robert Harper’s “Practical Foundations for Programming Languages” - Contains sections on type theory that are very accessible.

  2. The Oregon Programming Languages Summer School (OPLSS) - Their recorded lectures often include excellent introductions to type theory.

Supplementary Materials:

  1. “Lambda Calculus and Types” by Henk Barendregt - For understanding the lambda calculus foundation.

  2. “Introduction to Dependent Type Theory” lecture notes by Herman Geuvers - Helps bridge from simple type theory to dependent types.

Software Tools to Experiment With:

  1. Agda - A dependently typed programming language based on Martin-Löf Type Theory.

  2. Coq - While based on the Calculus of Inductive Constructions, it shares many concepts with MLTT.

Phase 1: Foundations (2-3 weeks)

  1. Start with Simon Thompson’s “Type Theory and Functional Programming” - Read chapters 1-3
    • Focus on understanding the correspondence between logic and types
    • Practice the simple exercises to reinforce concepts
  2. Supplement with selected chapters from “Proofs and Types” by Girard
    • Read the first two chapters for a different perspective
    • Pay special attention to the Curry-Howard correspondence

Phase 2: Core MLTT Concepts (3-4 weeks)

  1. Return to Thompson’s book for chapters 4-6
    • Study the rules of type formation, introduction, and elimination
    • Work through examples of dependent types
  2. Begin with “Programming in Martin-Löf’s Type Theory” by Nordström et al.
    • Focus on chapters 1-3 for the formal presentation
    • Pay close attention to the judgment forms and inference rules

Phase 3: Practical Implementation (2-3 weeks)

  1. Install Agda and work through the “Programming Language Foundations in Agda” tutorial
    • Start with simple type definitions
    • Implement basic proofs to see type theory in action
  2. Study Philip Wadler’s “Propositions as Types” paper (freely available online)
    • This connects the theory to practical programming concerns

Phase 4: Advanced Concepts (4+ weeks)

  1. Complete Thompson’s book, focusing on chapters 7-9
    • Pay special attention to universes and higher-order concepts
  2. Work through the remaining chapters of “Programming in Martin-Löf’s Type Theory”
    • Focus on the implementation of various mathematical concepts
  3. Explore Robert Harper’s “Practical Foundations for Programming Languages”
    • Chapters related to type theory will deepen your understanding

Throughout this process, I recommend: