resources.md

Resources

Outline of (mostly) Wikipedia articles which provide the conceptual framework for this project

Topics

• Curry-Howard correspondence
  • Table of correspondences
  • Hilbert-style deduction systems <=> combinatory logic
    • Modus ponens inference rule <=> combinator application
    • K and S axiom schemas <=> K and S combinators
      • Intuitionistic implicational logic <=> typed SK combinator caluclus
    • Summary <->
    • Details
    • Brief mention
    • Hilbert-style proof of a -> a <=> type inhabitation I = SKK
  • Bottom
    • Falsity / logical absurdity <=> bottom type
      • Uninhabited type
      • Type of function that never returns
    • Least element of a lattice
      • Boolean algebra for classical logic (examples)
      • Heyting algebra for intuitionistic logic (examples)
• Unification
• key parts
  • formal definition
  • syntactic first-order unification algorithm
• first-order vs higher-order unification
• semi-decidable unification for typed lambda calculus
• Hindley-Milner type system

Unsorted

• Intuitionistic logic
• Implicational propositional logic
• SKI combinator calculus
• Peano arithmetic
• First-order theories
• LF and first-order dependent type theory
• Lambda cube