[a-nikolaev]

Watch Oregon Programming Language School lectures "Basic Proof Theory" by Frank Pfenning.

https://www.cs.uoregon.edu/research/summerschool/summer15/cu...

Very clean and easy to follow video lectures on the relation between, types, programs, and logical proofs. One does not need functors and monoids to appreciate the beauty of functional type systems. (And to see why such type systems are indeed discovered rather than invented.)

[z1mm32m4n]

I second this. Frank's material is always thorough and approachable. He's designed and taught many courses at CMU, and his lecture notes for them are never less than impeccable.