A Transfinite Knuth-Bendix Order for Lambda-Free Higher-Order Terms.

Heiko Becker, Jasmin Christian Blanchette, Uwe Waldmann, Daniel Wand

Browse the full CADE paper archive.