Proposition as Types
speaker: Jingwen Chen event: Papers We Love #26
Notion with depth
- proposition as types
- proofs as programs
- simplication of proofs as evaluation of programs
Gerhard Gentzen (1935) introduces Natural deduction
Connects to the simply typed lambda calculus