Name
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.
|
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-3-642-03359-9_8 | Theorem Proving in Higher Order Logics |
Keywords | Field | DocType |
general technique,canonical structures,type classes,type inference,particular instance,interactive theorem provers,possible application,suitable hint,type inference algorithm,intrusive implementation,theorem prover | Theorem provers,Programming language,Computer science,Unification,Algorithm,Theoretical computer science,Type inference,Modular design,Abstract syntax,Proof assistant | Conference |
Volume | ISSN | Citations |
5674 | 0302-9743 | 22 |
PageRank | References | Authors |
1.05 | 15 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Andrea Asperti | 1 | 849 | 75.19 |
| Wilmer Ricciotti | 2 | 179 | 13.40 |
| Claudio Sacerdoti Coen | 3 | 384 | 40.66 |
| Enrico Tassi | 4 | 327 | 21.79 |