@STRING{lncs	= "Lecture Notes in Computer Science" }
@STRING{mpc08	= "Mathematics of Program Construction, 9th International
		  Conference, MPC 2008, Marseille, France, July 15-18, 2008.
		  Proceedings" }
@STRING{springer= "Springer-Verlag" }

@InProceedings{	  abelCoquandDybjer:mpc08,
  author	= {Andreas Abel and Thierry Coquand and Peter Dybjer},
  title		= {Verifying a Semantic $\beta\eta$-Conversion Test for
		  {Martin-L\"of} Type Theory},
  booktitle	= mpc08,
  pages		= {29--56},
  year		= 2008,
  editor	= {Philippe Audebaud and Christine Paulin-Mohring},
  volume	= 5133,
  series	= lncs,
  publisher	= springer,
  url		= {http://www.springerlink.com/content/q706kp66107404k5/},
  ee		= {http://dx.doi.org/10.1007/978-3-540-70594-9_4},
  isbn		= {978-3-540-70593-2}
}