Taylor Swift as important papers in programming languages, a thread.

"An Axiomatic Basis for Computer Programming," C.A.R. Hoare, 1969. Introduced Hoare Logic for proving program properties.

https://www.cs.cmu.edu/~crary/819-f09/Hoare69.pdf">https://www.cs.cmu.edu/~crary/81...

"Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints," Cousot & Cousot, 1977. Introduced abstract interpretation for statically analyzing program properties. Now used by Airbus.

https://www.di.ens.fr/~cousot/COUSOTpapers/publications.www/CousotCousot-POPL-77-ACM-p238--252-1977.pdf">https://www.di.ens.fr/~cousot/C...

"Design and synthesis of synchronization skeletons using branching time temporal logic," Clarke & Emerson, 1981. The first paper on model checking for program correctness. Led to the 2007 Turing Award.

http://www.cs.cmu.edu/~emc/papers/Invited%20Conference%20Articles/Design%20and%20Synthesis%20of%20Synchronization%20Skeletons%20Using%20Branching%20Time%20Temporal%20Logic.pdf">https://www.cs.cmu.edu/~emc/pape...

"Abstraction Mechanisms in CLU," Liskov et al, 1977. One of the most foundational papers in objected-oriented language design. Barbara Liskov won the Turing Award in 2009.

https://web.eecs.umich.edu/~weimerw/2011-6610/reading/liskov-clu-abstraction.pdf">https://web.eecs.umich.edu/~weimerw/...

"Proof-Carrying Code," Necula, 1997. The standard reference paper on the idea of compiling executables that carry verifiable proofs of their own properties. Won POPL& #39;s "Most Influential Paper" Award in 2007.

http://www.cs.jhu.edu/~fabian/courses/CS600.624/proof-carrying-code.pdf">https://www.cs.jhu.edu/~fabian/c...