##Type and proof
This is the latex source of Type and proof, a short article about logic, type system, lambda calculus, and curry howard isomorphism.
There may be some mistakes and it is not completed yet. Issues and pull requests are welcomed!
TODO
- denotational semantic of UTLC and STLC
- C-H isomorphism under sequent calculus
- type inference of STLC
- type checking VS. proof checking
- \beta and \eta reduction VS. prooving
- cut elimination and it's role in C-H isomorphism
- intro to proof search
- intro to category theory
- algebra semantic of logic and STLC
- intro to lambda cube
- linear logic and lienar type
- substructural logic and substructural type
- focusing/polarizing in type theory
- First order logic
- basic model theory
Contributors
- rainoftime
- lolisa
- TxmsLou
- txyyss
- dramforever