@incollection{JaH09Ref,
	Author = {James, Daniel W.H. and Hinze, Ralf},
	Booktitle = {Post-symposium proceedings of the 10th Symposium on Trends in Functional Programming},
	Chapter = {7},
	Editor = {Horv\'{a}th, Zolt\'{a}n and Zs\'{o}k, Vikt\'{o}ria},
	Isbn = {9781841504056},
	Location = {Kom\'{a}rno, Slovakia},
	Month = {June},
	Note = {\url{http://www.intellectbooks.co.uk/books/view-Book,id=4740/}},
	Pages = {97--112},
	Publisher = {Intellect},
	Series = {TFP'09},
	Title = {A reflection-based proof tactic for lattices in {Coq}},
	Url = {http://www.comlab.ox.ac.uk/people/daniel.james/lattice.html},
	Year = {2009}
}