"Proving termination using dependent types: the case of XOR-terms."

Jean-François Monin, Judicaël Courant (2006)
a service of Schloss Dagstuhl - Leibniz Center for Informatics