Most of the contents in this notebook are unsorted and may contain incorrect information.
Good Books for PLT and Proof Theory
Logical Foundations, and, Coq!
Verified Functional Algorithms
Programming Language Foundations
Some Thoughts on Loop Invariant
[Intro to Type Theory & Simply Typed $\lambda$ Calculus [STLC] – The simply typed lambda calculus, a form of type theory, is a typed interpretation of the lambda calculus with only one type constructor (→) that builds function types. In type theory, we need to define the following rules:](https://hiroki-chen.notion.site/Intro-to-Type-Theory-Simply-Typed-lambda-Calculus-STLC-The-simply-typed-lambda-calculus-a-fo-d1870032fe1946d5832c07d29392bb72)
Practical Foundations for Programming Language by Robert Harper
(Generalized) Algebraic Data Type, Inductive Types, and Co-induction.
Universe, Impredicativity, and Strict Positivity
Big hint: Induction is very, very, very important in type theories and programming languages. We can say most of the proofs are done using induction on a type; this is because Martin-Lof’s intuitive type theory requires evidence for the thing we need to prove: we simply construct it. The rule of structural induction basically states that if for all term $s$, given a predicate $P(r)$ for all immediate sub-terms $r$ of $s$, we can show $P(s)$, then $P(s)$ holds for all $s$. Also do not forget to perform induction on derivation rules. Say we have a property $P(x)$. We can investigate on how $x$ can be constructed, evaluated, or derived. Almost every type is defined inductively as a smallest set that can generate the thing we want.