Software foundations is a practical introduction to Coq's type theory (calculus of inductive constructions). You get a really strong feel for the concept of pro

Software foundations is a practical introduction to Coq's type theory (calculus of inductive constructions). You get a really strong feel for the concept of proofs as types. One of the sections builds the theory of typed lamda calculus within Coq. It's otherwise lighter on theory than other resources. https://softwarefoundations.cis.upenn.edu/ https://softwarefoundations.cis.upenn.edu/