Those topics fall under the general heading of Mathematical Logic. Wikipedia is usually a pretty good place to start for any such question: https://en.wikiped

Those topics fall under the general heading of Mathematical Logic. Wikipedia is usually a pretty good place to start for any such question: https://en.wikipedia.org/wiki/Lambda_calculus https://en.wikipedia.org/wiki/Lambda_calculus there are a lot of external links and references there. I don't know if there's a lot of work still being done with the original untyped lambda calculus but typed lambda calculi (or analogous models), on which I believe Haskell is based, are another story. You may also find this interesting: https://softwarefoundations.cis.upenn.edu/current/lf-current/index.html https://softwarefoundations.cis.upenn.edu/current/lf-current... It's an introduction to the coq proof assistant which is based (at least to the best of my understanding) on a kind of typed lambda calculus. In the first few chapters you will learn how to construct the natural numbers and formally (ie. in a machine verifiable way) prove theorems about them.