Conor McBride's lecture series CS410 at Strathclyde is freely available on Youtube, and my team is watching that at lunchtimes - excellent gentle introduction t

Conor McBride's lecture series CS410 at Strathclyde is freely available on Youtube, and my team is watching that at lunchtimes - excellent gentle introduction to proofs-as-types and so forth, and it has turned me onto Agda as a theorem proving environment.