{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T07:05:41Z","timestamp":1742799941146},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642033582"},{"type":"electronic","value":"9783642033599"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-03359-9_8","type":"book-chapter","created":{"date-parts":[[2009,8,20]],"date-time":"2009-08-20T01:46:12Z","timestamp":1250732772000},"page":"84-98","source":"Crossref","is-referenced-by-count":33,"title":["Hints in Unification"],"prefix":"10.1007","author":[{"given":"Andrea","family":"Asperti","sequence":"first","affiliation":[]},{"given":"Wilmer","family":"Ricciotti","sequence":"additional","affiliation":[]},{"given":"Claudio","family":"Sacerdoti Coen","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Tassi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/3-540-61780-9_59","volume-title":"Types for Proofs and Programs","author":"G. Barthe","year":"1996","unstructured":"Barthe, G., Ruys, M., Barendregt, H.: A two-level approach towards lean proof-checking. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol.\u00a01158, pp. 16\u201335. Springer, Heidelberg (1996)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 86\u2013101. Springer, Heidelberg (2008)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/BFb0014565","volume-title":"Theoretical Aspects of Computer Software","author":"S. Boutin","year":"1997","unstructured":"Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol.\u00a01281, pp. 515\u2013529. Springer, Heidelberg (1997)"},{"key":"8_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511543326","volume-title":"Rippling: meta-level guidance for mathematical reasoning","author":"A. Bundy","year":"2005","unstructured":"Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: meta-level guidance for mathematical reasoning. Cambridge University Press, New York (2005)"},{"key":"8_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-44404-1_7","volume-title":"Logic for Programming and Automated Reasoning","author":"D. Delahaye","year":"2000","unstructured":"Delahaye, D.: A Tactic Language for the System Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS, vol.\u00a01955, pp. 85\u201395. Springer, Heidelberg (2000)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-74591-4_8","volume-title":"Theorem Proving in Higher Order Logics","author":"G. Gonthier","year":"2007","unstructured":"Gonthier, G., Mahboubi, A., Rideau, L., Tassi, E., Thery, L.: A Modular Formalisation of Finite Group Theory. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol.\u00a04732, pp. 86\u2013101. Springer, Heidelberg (2007)"},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1145\/227699.227700","volume":"18","author":"C. Hall","year":"1996","unstructured":"Hall, C., Hammond, K., Jones, S.P., Wadler, P.: Type classes in haskell. ACM Transactions on Programming Languages and Systems\u00a018, 241\u2013256 (1996)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"8_CR8","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1093\/logcom\/9.1.105","volume":"9","author":"Z. Luo","year":"1999","unstructured":"Luo, Z.: Coercive subtyping. J. Logic and Computation\u00a09(1), 105\u2013130 (1999)","journal-title":"J. Logic and Computation"},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-540-88011-0","volume-title":"Types for Proofs and Programs","author":"Z. Luo","year":"2008","unstructured":"Luo, Z.: Manifest fields and module mechanisms in intensional type theory. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol.\u00a04941. Springer, Heidelberg (2008)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/978-3-540-68103-8_11","volume-title":"Types for Proofs and Programs","author":"C. Coen Sacerdoti","year":"2008","unstructured":"Sacerdoti Coen, C., Tassi, E.: Working with mathematical structures in type theory. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol.\u00a04941, pp. 157\u2013172. Springer, Heidelberg (2008)"},{"key":"8_CR11","first-page":"51","volume":"1","author":"C. Sacerdoti Coen","year":"2008","unstructured":"Sacerdoti Coen, C., Tassi, E.: A constructive and formal proof of Lebesgue\u2019s dominated convergence theorem in the interactive theorem prover Matita. Journal of Formalized Reasoning\u00a01, 51\u201389 (2008)","journal-title":"Journal of Formalized Reasoning"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Saibi, A.: Typing algorithm in type theory with inheritance. In: The 24th Annual ACM SIGPLAN - SIGACT Symposium on Principle of Programming Language (POPL) (1997)","DOI":"10.1145\/263699.263742"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"key":"8_CR14","unstructured":"The Coq Development Team. The Coq proof assistant reference manual (2005), \n                    \n                      http:\/\/coq.inria.fr\/doc\/main.html"},{"key":"8_CR15","first-page":"60","volume-title":"POPL 1989: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages","author":"P. Wadler","year":"1989","unstructured":"Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: POPL 1989: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 60\u201376. ACM, New York (1989)"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/BFb0028402","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Wenzel","year":"1997","unstructured":"Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol.\u00a01275, pp. 307\u2013322. Springer, Heidelberg (1997)"}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-03359-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,9]],"date-time":"2019-03-09T14:09:38Z","timestamp":1552140578000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-03359-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642033582","9783642033599"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-03359-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}