-
Notifications
You must be signed in to change notification settings - Fork 11
ImplementationNotes
John Boyland edited this page Oct 10, 2015
·
1 revision
The Unification algorithm implemented in SASyLF is taken from:
Tobias Nipkow. Functional Unification of Higher-Order Patterns. Logic in Computer Science, 1993.
We found that paper to be one of the more readable introductions to higher order pattern unification. A more recent presentation, which might be worth following more directly in a future, refactored implementation, is:
Jason Reed. Higher-Order Constraint Simplification In Dependent Type Theory. LFMTP 2009.