Several mechanisms such as Canonical Structures [14], Type Classes [13,16], or Pullbacks [10] have been recently introduced with the aim to improve the power and flexibility of the type inference algorithm for interactive theorem provers. We claim that all these mechanisms are particular instances of a simpler and more general technique, just consisting in providing suitable hints to the unification procedure underlying type inference. This allows a simple, modular and not intrusive implementation of all the above mentioned techniques, opening at the same time innovative and unexpected perspectives on its possible applications. © 2009 Springer.
CITATION STYLE
Asperti, A., Ricciotti, W., Sacerdoti Coen, C., & Tassi, E. (2009). Hints in unification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5674 LNCS, pp. 84–98). https://doi.org/10.1007/978-3-642-03359-9_8
Mendeley helps you to discover research relevant for your work.