Hints in Unification

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.
Original languageEnglish
Title of host publicationTheorem Proving in Higher Order Logics
Subtitle of host publication22nd International Conference, TPHOLs 2009, Munich, Germany, August 17-20, 2009. Proceedings
PublisherSpringer Berlin Heidelberg
Pages84-98
Number of pages15
ISBN (Electronic)978-3-642-03359-9
ISBN (Print)978-3-642-03358-2
DOIs
Publication statusPublished - 2009

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume5674
ISSN (Print)0302-9743

Cite this