Create 2025-04-05-mltt-72.md

Author: streamcode9

_posts/2025-04-05-mltt-72.md

@@ -0,0 +1,81 @@
+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:
+- An introductory text on logic
+- Basic functional programming concepts
+- Familiarity with the idea of formal systems
+
+### 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:
+- Implementing examples in Agda as you learn concepts
+- Discussing concepts in online forums like the Types Forum or Agda mailing list
+- Revisiting earlier material as needed - type theory concepts build on each other