Uma formalização da composicionalidade do cálculo lambda-ex em Coq - Barros, Flávio José Ferro (2010)
Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2010.