[Functional programming with bananas, lenses, envelopes and barbed wire](https://maartenfokkinga.github.io/utwente/mmf91m.pdf) - this paper has some really nice ideas about higher order functions that translate well to proofs [forall x: Calgary Remix](http://forallx.openlogicproject.org/) - open textbook on natural deduction
Functional programming with bananas, lenses, envelopes and barbed wire - this paper has some really nice ideas about higher order functions that translate well to proofs
forall x: Calgary Remix - open textbook on natural deduction