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.
cs.cmu.edu/~crary/819-f09…
"An Axiomatic Basis for Computer Programming," C.A.R. Hoare, 1969. Introduced Hoare Logic for proving program properties.
cs.cmu.edu/~crary/819-f09…
"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.
di.ens.fr/~cousot/COUSOT…
di.ens.fr/~cousot/COUSOT…
"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.
cs.cmu.edu/~emc/papers/In…
cs.cmu.edu/~emc/papers/In…
"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.
web.eecs.umich.edu/~weimerw/2011-…
web.eecs.umich.edu/~weimerw/2011-…
"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's "Most Influential Paper" Award in 2007.
cs.jhu.edu/~fabian/course…
cs.jhu.edu/~fabian/course…
Had to go for a bit; back now!
"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…
"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…
"From System F to Typed Assembly Language," @GMorrisett et al, 1998. Introduced a typed assembly language + type-preserving translation. Being able to prove properties of assembly through types is huge! POPL "Most Influential Paper" in 2008.
cs.cornell.edu/talc/papers/ta…
cs.cornell.edu/talc/papers/ta…
@GMorrisett "Formal Certification of a Compiler Back-end," Xavier Leroy (OCaml creator!), 2006. First paper to use interactive theorem-proving (with Coq) to program and formally verify a C compiler. Landmark paper in verification. POPL "Most Influential Paper" 2016.
xavierleroy.org/publi/compiler…
xavierleroy.org/publi/compiler…
@GMorrisett "Towards a Mathematical Semantics for Computer Languages," Dana Scott and Christopher Strachey, 1971. A classic in modeling programs using math.
cs.cmu.edu/~crary/819-f09…
cs.cmu.edu/~crary/819-f09…
@GMorrisett And we'll end on a major classic, "Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I," John McCarthy, 1960. The OG functional programming paper, introducing Lisp. Fortran is the only widely-used language older than Lisp!
cs.cmu.edu/~crary/819-f09…
cs.cmu.edu/~crary/819-f09…
