Programming Languages Reading List
Programming Languages Reading List Core list:
- An Axiomatic Basis of Computer Programming-- C.A.R. Hoare Communications of the ACM, Vol. 12(10), 1969. (Courses: CS477; CS476; CS522)
- A Theory of Type Polymorphism in Programming -- Robin Milner Journal of Computer and System Sciences, Vol 17(3), 1978. (Courses: CS422, CS522)
- Dimensions of Object-Based Language Design -- Peter Wegner ACM SIGPLAN Notices, Vol 22(12), 1987. Also in OOPSLA'87. (Courses: OO concepts also covered in CS422 and CS522)
- Concurrent Object-Oriented Programming -- Gul Agha Communications of the ACM, Vol 33(9), 1990 (Courses: concepts of concurrent OO languages also covered in CS422)
- Call-by-Name, Call-by-Value and the λ-Calculus -- Gordon Plotkin Theoretical Computer Science, Vol 1(2), 1975 --- Covers major functional programming principles, as well as abstract machines (SECD, etc.) (Courses: CS422, CS522)
- The Essence of Functional Programming -- Philip Wadler Proceedings of POPL '92 --- Covers monads and their use to modularly implement interpreters; also a bit about denotational semantics and about continuations (Courses: partly covered in CS422 and CS522, but CS522 will discuss denotational semantics and monads in more depth starting with Spring 2013)
- A Syntactic Approach to Type Soundness --- Andrew K. Wright, Matthias Felleisen Information and Computation, Vol 115(1), 1994 --- Covers modern approach to prove type soundness, based on preservation and progress (Courses: basic ideas covered in CS522)
- The Semantics of Predicate Logic as a Programming Language -- Maarten H. van Emden, Robert A. Kowalski Journal of the ACM, Vol 23(4), 1976. --- Covers the basics of logic programming: operational semantics, denotational/fixed-point semantics, models (Courses: CS522, but will also add a module in CS422)
- Pict: A Programming Language Based on the Pi-Calculus -- Bejamin C. Pierce, David N. Turner Proof, Language and Interaction: Essays in Honor of Robin Milner, MIT Press, 1997 --- Covers pi-calculus (and thus concepts from process algebra and concurrency and communication) in a PL style (Courses: could cover in CS522, as we already have a rewrite semantics of Pict)
- A Rewriting Logic Approach to Operational Semantics -- Traian Serbanuta, Grigore Rosu, Jose Meseguer Information and Computation, Vol 207(2), 2009 --- Covers all major variants of operational semantics, as well as basics of rewriting logic and Maude (Courses: CS422, CS522)
- Separation Logic: A Logic for Shared Mutable Data Structures -- John Reynolds Proceedings of LICS'02 --- Covers the basics of separation logic, used these days as an extension of Hoare logic to better handle heaps (Courses: CS522)
- Notes on Static Analysis -- Michael I. Schwartzbach BRICS Lecture Notes --- Covers type analysis, lattice theory, control flow graphs, dataflow analysis, widening and narrowing, interprocedural analysis, and pointer analysis.
- Programming languages as operating systems -- Matthew Flatt, Robert Bruce Findler, Shriram Krisnamurthi, Matthias Felleisen Proceedings of ICFP'99 --- Covers fundamental principles of virtual machines, in a small and easy to read paper
Optional additional suggested reading:
- A foundation for Actor Computation - Journal of Functional Programming
- Symbolic Execution: A survey of new trends in symbolic execution for software testing and analysis -- Corina S. Pasareanu, Willem Visser Int J Softw Tools Technol Transfer (STTT) 11:339--353.
- Constraint solving/SMT solvers: First-order theories: Chapter 3 of Calculus of Computation (Springer) - Bradley and Manna (~25 pages) Covers various first-order theories and summarizes the decidable logics and their complexity. These are the logics supported by current SMT solvers, pretty much.