Greatest of the great: C. A. R. Hoare. An axiomatic basis for computer programming: http://sigpl.or.kr/school/2005w/slides/2_17_1.pdf http://sigpl.or.kr/school

Greatest of the great: C. A. R. Hoare. An axiomatic basis for computer programming: http://sigpl.or.kr/school/2005w/slides/2_17_1.pdf http://sigpl.or.kr/school/2005w/slides/2_17_1.pdf Peter J. Landin. The next 700 programming languages: http://www.thecorememory.com/Next_700.pdf http://www.thecorememory.com/Next_700.pdf Robin Milner. A theory of type polymorphism in programming: http://courses.engr.illinois.edu/cs421/sp2012/project/milner-polymorphism.pdf http://courses.engr.illinois.edu/cs421/sp2012/project/milner... Gordon Plotkin. Call-by-name, call-by-value, and the λ-calculus : http://www.sciencedirect.com/science/article/pii/0304397575900171 http://www.sciencedirect.com/science/article/pii/03043975759... (PDF link at upper right of page) John C. Reynolds. Towards a theory of type structure: http://repository.cmu.edu/cgi/viewcontent.cgi?article=2289&context=compsci&sei-redir=1 http://repository.cmu.edu/cgi/viewcontent.cgi?article=2289&c... Pretty great works: Luca Cardelli. A semantics of multiple inheritance: http://lucacardelli.name/Papers/Inheritance.pdf http://lucacardelli.name/Papers/Inheritance.pdf Luis Damas and Robin Milner. Principal type schemes for functional programs: http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_types.pdf http://web.cs.wpi.edu/~cs4536/c12/milner-damas_principal_typ... Edsger W. Dijkstra. Recursive programming: http://oai.cwi.nl/oai/asset/9253/9253A.pdf http://oai.cwi.nl/oai/asset/9253/9253A.pdf Edsger W. Dijkstra. Go to statement considered harmful: http://www.massey.ac.nz/~kahawick/159331/Goto-Harmful-Dijkstra.pdf http://www.massey.ac.nz/~kahawick/159331/Goto-Harmful-Dijkst... William A. Howard. The formulas-as-types notion of construction: http://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf http://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf Robert Kowalski. Predicate logic as programming language: http://65.99.230.10:81/collect/computer/index/assoc/HASH0183.dir/doc.pdf http://65.99.230.10:81/collect/computer/index/assoc/HASH0183... Peter J. Landin. The mechanical evaluation of expressions: http://ropas.snu.ac.kr/lib/dock/La1964.pdf http://ropas.snu.ac.kr/lib/dock/La1964.pdf John McCarthy. Recursive functions of symbolic expressions and their computation by machine: http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.111.8833&rep=rep1&type=pdf http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.111... Eugenio Moggi. Computational lambda-calculus and monads: http://pdf.aminer.org/000/267/711/lazy_lambda_calculus_theories_models_and_local_structure_characterization_extended.pdf http://pdf.aminer.org/000/267/711/lazy_lambda_calculus_theor... Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System-F to typed assembly language: http://staff.ustc.edu.cn/~xyfeng/reading/p527-morrisett.pdf http://staff.ustc.edu.cn/~xyfeng/reading/p527-morrisett.pdf George C. Necula. Proof-carrying code: http://www.utdallas.edu/~kxh060100/Papers/necula96.pdf http://www.utdallas.edu/~kxh060100/Papers/necula96.pdf Gordon D. Plotkin. LCF considered as a programming language: http://www.sciencedirect.com/science/article/pii/0304397577900445 http://www.sciencedirect.com/science/article/pii/03043975779... Gordon D. Plotkin. A structural approach to operational semantics: https://www.alice.virginia.edu/~weimer/2006-655/reading/plotkin81structural.pdf https://www.alice.virginia.edu/~weimer/2006-655/reading/plot... Guy Lewis Steele Jr. RABBIT: A compiler for SCHEME ftp://publications.ai.mit.edu/ai-publications/pdf/AITR-474.pdf OK, I think the first two sections are plenty. You can search for the rest yourself on Google Scholar (I found most of these as the first hit on Google Scholar, one or two took looking through a few hits or doing a Google search as well)