A few good computer science  papers


These papers were recommnended by SWS faculty as both influential and well-written. Take a look at them to see how they present their ideas.  Look at the abstracts, organization, and conclusions.  See how and where they present the related work.  Look at how they give examples, or present the intuition, before they give the technical details.  See how they present and discuss code, algorithms, rules, or theorums.

The papers are orgnized by the general area of software systems
Program Verification
Symbolic Reasoning
Type Systems
Distributed Systems

Area: verification

 Calysto: Scalable and Precise Extended Static Checking
 Domagoj Babic and Alan J. Hu
 ICSE 2008
 http://doi.acm.org/10.1145/1368088.1368118

Notes:   In this paper, look at the literature review, which clearly explains the hole in the research that Calysto fills.  Note that at the end of section 1, there is one sentence that says what the rest of the paper is about, but no section by section outline.  See also the last paragraph of section 3, which has a good explanation of future work.

Lazy Abstraction
Thomas Henzinger, Ranjit Jhala, Rupak Majumdar
POPL 2002
http://mtc.epfl.ch/~tah/Publications/lazy_abstraction.pdf

Notes:  In the abstract, pervious work is given in the first sentence.  The rest of the abstract is about the paper content, and provides good detail.  The details of the paper start in section 2 with an example, which helps make the method of lazy abstraction more concrete. Throughout the paper, look for the examples that are use to motivate the intuitive idea.

An Automata-Theoretic Approach to Automatic Program Verification
Moshe Vardi and Pierre Wolper
LICS 1986
http://www.cs.rice.edu/~vardi/papers/lics86.pdf.gz


Notes:  This paper was very influential in opening up a new research area.  The abstract is very concise.  They clearly state their research goals on the second page.  In the same paragraph, they dismiss tableu models and propose using propositional temporal logic.  They end the introduction with a summary of their work - applying model checking to finite-state programs and then probablistic programs.  In general, they sketch their theories and arguments, and leave fuller explanations to a longer paper.  See if you think they provide enough information to follow their argument.

Area: Symbolic Reasoning 

Graph Based Algorithms for Boolean Function Manipulation
Randal Bryant
IEEE Transactions on Computers 1986
http://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf

Notes: There are 3 paragraphs in the introduction before getting to the point of the paper.  The third paragraph clearly states a problem with previous work (the problem with analyzing Boolean functions), that their work helps address (their algorithm is more efficient). There is a short literature review at the end of section 1.  Also, their notation conventions are given in the introduction.  You can decide whether or not you like this. In section 3, they start their discussion with examples, which they graphically represent. They put some of the technical details in an Appendix.

Area: Type Systems

Manifest types, modules, and separate compilation
Xavier Leroy
POPL 1994
http://gallium.inria.fr/~xleroy/publi/manifest-types-popl.pdf

 Notes:  The general ideas are presented in section 2 before they are formalized in sections 3.  The first two paragraphs of section 4 explain the goal of the section, which is to compare the expressiveness of the  variant of SML presented with the standard SML module system. As this comparison is not straightforward, Leroy is explicit about the assumptions and simplifications he makes.  Look at the related work section in the Conclusion, which is very brief.


From System F to Typed Assembly Language
Greg Morrisett, David Walker, Karl Crary, and Neal Glew
POPL 1998
http://www.eecs.harvard.edu/~greg/cs255sp2004/morrisett98tal.pdf

Notes: This is a good introduction to a variety of ideas in programming languages.  It also won the most influential POPL award at 10 years in 2008.  The first sentence of the abstract is a very high-level overview of the whole paper.  There is no background information, and the abstract works very well.  The last sentence of the abstract is about impact or utility. I like the way this paper does citations.  Many CS papers just give the number of the citation from the bibliography, which is very hard to read in-line in the text, as the reference isn't transparent.  This paper gives authors' last names, which I find much easier to read and more information.  Of course, this takes space.  The overview section 1.1 has a paragraph about ideas and then a paragraph with the layout of the paper.  It also mentions the technical report and says what extra information is in there.  This seems like a good location to say there's a technical report. The sections of the paper map very clearly onto the categories in Figure 1, and each section is introduced with a brief paragraph about where it is in the process, see the first paragraph of section 4 for a nice example.  This really helps the reader make their way through the paper. Notice also how the syntax tables get explained in-line in the text, for example the 4th paragraph of section 5.1 which line by line comments on Figure 6. This is a middle-ground between exhaustively explaining each rule and just putting the rules in the figure and not discussing them.  Think about the advantages of each of these strategies and why this choice works here.

Theorems for Free!
Philip Wadler
FPCA 1989
http://homepages.inf.ed.ac.uk/wadler/papers/free/free.ps 

Notes: The frame model section is quite hard to understand, but the earlier parts which explain the basic idea of free theorems and give various examples are very clear.  This is also a paper that's frequently cited.  The abtract is very short - is this effective? In terms of style, this paper shows the personality of the author.  It's very engaging from the beginning, as he starts out with a parlour trick example.  But he also says that the point of the paper is to explain how the trick works so the reader isn't expected just to tag along with an interesting example without knowing the point up front. This is a very effective way to get the reader interested in reading more.  The roadmap, or forward references, are integrated throughout the introduction - see the paragraph beginning "the result that allows," which means that the roadmap can be integrated in with content.  Also, the introduction gives some information about why theorem generation is interesting, i.e. applications.  Towards the end of the introduction, there's a paragraph on literature review, followed by the main contribution, future work, and a more standard road map. The narrative arc is from engaging anecdote to implications to a more traditional organization of an introduction at the end which is a segue to the more technical parts of the paper. One other note on style, the author likes to address the readers, see for example section 2 "Cognoscenti will recognize...," section 3.5 "You will immediately guess...," or section 3.7  "a little thought shows..."  This is a conversational style that some readers find engaging and interesting.  Others find it off-putting, particularly when the author makes assumptions about what the reader may or may not know.  Think about how you feel about this style.

Area: Distributed Systems

Manageability, Availability and Performance in Porcupine: A Highly Scalable Internet Mail Service
Yasushi Saito, Brian Bershad, and Hank Levy.
17th ACM Symposium on Operating Systems Principles, Dec 1999
http://www.ysaito.com/sosp.ps 


Notes:  The abstract is short; it starts with the key idea, describes a few details, and ends with the key contribution.  There is no extraneous background/introductory information.  In general, this paper provides little background and goes straight to the details - see if you like that.