More references for further reading

[nbloomf]

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