# Links (Week 7)

## Table of Contents

## 1 Monads

My favourite Monad tutorial, to understand Monads in Haskell, is Dan Piponi's "You could have invented monads!", located here:

http://blog.sigfpe.com/2006/08/you-could-have-invented-monads-and.html

Also, the Typeclassopedia is a good resource to understand the various abstractions built into the standard library, including monads:

## 2 Curry-Howard Correspondence

Philip Wadler has written a lovely, detailed exposition of the Curry-Howard correspondence between propositions and types in this very readable paper, located here:

http://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf

He has also given a nice talk on the topic at Strange Loop in 2015:

## 3 Safety/Liveness properties

The proof that was the topic of the extension lecture in Week 7 was first given in this paper:

https://www.cs.cornell.edu/fbs/publications/defliveness.pdf

This paper proves that every property is the intersection of a safety and a liveness property. None of this is examinable, but it is very interesting.

Also, the proof is reasonably readable if you have some exposure to metric spaces or topology before.