Require stricter constructor types

This adds a premise to constructor types that requires them the have to correct form

Data types

This adds data types to the language, but without case expressions to match on them yet

Mutual typing judgement

This introduces a context validity judgement that is mutually called by the kinding judgement

System F

This extends the simply typed lamda calculus to System F and proves its type safety.

Nominal2

This moves the whole proof over to Nominal2 so they keep alpha equivalence in mind

Add let bindings

This is a soundness proof of the simply typed lambda calculus with let bindings

Simply Typed Lambda calculus

A complete soundness proof of the simply typed lambda calculus.