Ken Thomson. Reflections on Trusting Trust. Turing Award Lecture. Phillip Wadler. Propositions as Types. Andrew Appel. SSA is Functional Programming. Phillip Wadler. Theorems for free! https://homepages.inf.ed.ac.uk/wadler/papers/propositions-as-types/propositions-as-types.pdf Xavier Leroy. A formally verified compiler back-end. Journal of Automated Reasoning. C. A. R. Hoare. An Axiomatic Basis for Computer Programming.