Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading.

Patricia Johann, Michael Kohlhase

Browse the full CADE paper archive.