TAPL-Practice

TODO

• UTLC
  • Semantics
    • Small-step
    • Big-step
  • Evaluation Strategy
    • Call-By-Value
    • Call-By-Name
    • Lazy Evaluation
• STLC
• Subtyping
• Recursive Types
• Polymorphism
  • Type Reconstruction
    • Constraint-Based Typing & Unification
    • Principal Types & Incremental Unification
    • Implicit Type Annotations
    • Let-Polymorphism
• Higher-Order Systems
• Create a new toy language with all these features
• Important Prove all the theorems in Coq

make slow progress...