"An Axiomatic Basis for Computer Programming," C.A.R. Hoare, 1969. Introduced Hoare Logic for proving program properties.
cs.cmu.edu/~crary/819-f09…
![](https://pbs.twimg.com/media/EfHH8L2UYAAkZny.jpg)
![](https://pbs.twimg.com/media/EfHH-wzVAAA5Dmg.jpg)
di.ens.fr/~cousot/COUSOT…
![](https://pbs.twimg.com/media/EfHJbkJUEAUvJkK.jpg)
![](https://pbs.twimg.com/media/EfHJdqSUMAAz6m0.jpg)
cs.cmu.edu/~emc/papers/In…
![](https://pbs.twimg.com/media/EfHLTzWUMAEIo43.png)
![](https://pbs.twimg.com/media/EfHLWD2U4AEtA3G.jpg)
web.eecs.umich.edu/~weimerw/2011-…
![](https://pbs.twimg.com/media/EfHNAk9UYAAkpAv.png)
![](https://pbs.twimg.com/media/EfHNCMQU0AAQPNA.jpg)
cs.jhu.edu/~fabian/course…
![](https://pbs.twimg.com/media/EfHOkBbUYAA4X88.png)
![](https://pbs.twimg.com/media/EfHOmvMVAAEyx3F.jpg)
"Imperative functional programming," Simon Peyton Jones and Philip Wadler, 1993. Introduces monads for I/O in pure functional languages. POPL "Most Influential Paper" Award in 2003.
microsoft.com/en-us/research…
![](https://pbs.twimg.com/media/EfHdsaAU4AA3mkW.png)
![](https://pbs.twimg.com/media/EfHduSoU8AAd2U-.jpg)
cs.cornell.edu/talc/papers/ta…
![](https://pbs.twimg.com/media/EfHfY5RVoAA3S4W.png)
![](https://pbs.twimg.com/media/EfHfhP3UcAAf3so.jpg)
xavierleroy.org/publi/compiler…
![](https://pbs.twimg.com/media/EfHgchzUEAEbsAg.png)
![](https://pbs.twimg.com/media/EfHge7qUYAAmxxd.jpg)
cs.cmu.edu/~crary/819-f09…
![](https://pbs.twimg.com/media/EfHiyImUMAAx5zI.jpg)
![](https://pbs.twimg.com/media/EfHjEUHVAAE8W-v.jpg)
cs.cmu.edu/~crary/819-f09…
![](https://pbs.twimg.com/media/EfHmQ5SUEAAMqQV.png)
![](https://pbs.twimg.com/media/EfHmSvBUEAE82kL.jpg)