@STRING{lncs	= "Lecture Notes in Computer Science" }
@STRING{springer= "Springer-Verlag" }
@STRING{tlca09	= "Typed Lambda Calculi and Applications, 9th International
		  Conference, TLCA 2009, Brasilia, Brazil, July 1-3, 2009,
		  Proceedings" }

@InProceedings{	  abelCoquandPagano:tlca09,
  author	= {Andreas Abel and Thierry Coquand and Miguel Pagano},
  title		= {A Modular Type-Checking Algorithm for Type Theory with
		  Singleton Types and Proof Irrelevance},
  booktitle	= tlca09,
  pages		= {5--19},
  year		= 2009,
  editor	= {P.-L. Curien},
  volume	= 5608,
  series	= lncs,
  publisher	= springer
}