The second part discusses lamda calculus and formalizes a version in Agda. The first part should introduce enough Agda to understand the second part.
If you like Haskell and Scheme, I think you would enjoy Agda as well. It’s (to simplify a lot) lambda calculus extended with dependent types, which imho feels more consistent and cohesive to understand than Haskell and all the various ghc extensions (for me at least, it was easier to understand the advanced extensions after having dealt with a fully dependently typed language)
I also think Benjamin Pierce’s Types and Programming Languages ( https://www.cis.upenn.edu/~bcpierce/tapl/ ) could be useful to you. It introduces lambda calculus as the computational foundation, and then builds various type theories on top of that.
Comments
It’s not exactly what you’re asking for, but have you come across the book Programming Language Foundations in Agda?
https://plfa.github.io/
The second part discusses lamda calculus and formalizes a version in Agda. The first part should introduce enough Agda to understand the second part.
If you like Haskell and Scheme, I think you would enjoy Agda as well. It’s (to simplify a lot) lambda calculus extended with dependent types, which imho feels more consistent and cohesive to understand than Haskell and all the various ghc extensions (for me at least, it was easier to understand the advanced extensions after having dealt with a fully dependently typed language)
I also think Benjamin Pierce’s Types and Programming Languages ( https://www.cis.upenn.edu/~bcpierce/tapl/ ) could be useful to you. It introduces lambda calculus as the computational foundation, and then builds various type theories on top of that.