% http://cmtw.harvard.edu/Documentation/TeX/Bibtex/Example.html 

@STRING{PRL="Phys. Rev. Lett."} %(modified () to {} )
@STRING{RMP="Rev. Mod. Phys."} %(modified () to {} )

@ARTICLE{klitzing:qhe,
   AUTHOR="K. von Klitzing and G. Dorda and M. Pepper",
   TITLE="New method for high accuracy determination of fine structure
            constant based on quantised hall resistance",
   JOURNAL=PRL,
   VOLUME=45,
   PAGES=494,
   YEAR=1980
}

@ARTICLE{klitzing:nobel,
   AUTHOR="Klaus von Klitzing",
   TITLE="The Quantised Hall Effect",
   JOURNAL=RMP,
   VOLUME=58,
   PAGES=519,
   YEAR=1986
}

% ACL2 Workshop 2000 ===========================================================
% http://www.cs.utexas.edu/users/jared/acl2/workshops-bibtex/workshops.bib

@techreport{00-lusk-parallel,
  author="{Ewing Lusk} and {William McCune}",
  title="{ACL2 for Parallel Systems Software: A Progress Report}",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
}

@techreport{00-wilding-stobj,
  author="{Matthew Wilding}",
  title="{Using a Single-Threaded Object to Speed a Verified Graph Pathfinder}",
  month="November",
  year="2000",
  number="TR-00-29",
  institution="The University of Texas at Austin, Department of Computer Sciences",
  note="ACL2 Workshop 2000 Proceedings, Part A"
}

@inproceedings{04-cowles-tail,
  author="{John Cowles} and {Ruben Gamboa}",
  title="{Contributions to the Theory of Tail Recursive Functions}",
  booktitle="Fifth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2-2004)",
  year="2004",
  month="November"
}