• Case study: simply-typed lambda-calculus
  • Syntax
  • Operational semantics
  • Type-checker
  • Soundness proof
  • Exercises for STLC
• Intro to tactics
• Pattern-matching tactics
  • Contents
  • Motivation
  • Some utility functions
  • Pattern types
  • Pattern matching exceptions
    • Types of exceptions
    • The exception monad
    • Liftings
  • Pattern interpretation
  • Pattern-matching problems
    • Definitions
    • Resolution
  • A DSL for pattern-matching
    • Pattern notations
    • Problem notations
    • Continuations
  • Putting it all together
  • Examples
    • Simple examples
    • A real-life example
  • Possible extensions
  • Notes