Hints in Unification

1. Barthe, G., Ruys, M., Barendregt, H.: A two-level approach towards lean proof-checking. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 16–35. Springer, Heidelberg (1996)

   Chapter  Google Scholar 

2. Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 86–101. Springer, Heidelberg (2008)

   Chapter  Google Scholar 

3. Boutin, S.: Using reflection to build efficient and certified decision procedures. In: Ito, T., Abadi, M. (eds.) TACS 1997. LNCS, vol. 1281, pp. 515–529. Springer, Heidelberg (1997)

   Chapter  Google Scholar 

4. Bundy, A., Basin, D., Hutter, D., Ireland, A.: Rippling: meta-level guidance for mathematical reasoning. Cambridge University Press, New York (2005)

   Book  MATH  Google Scholar 

5. Delahaye, D.: A Tactic Language for the System Coq. In: Parigot, M., Voronkov, A. (eds.) LPAR 2000. LNCS, vol. 1955, pp. 85–95. Springer, Heidelberg (2000)

   Chapter  Google Scholar 

6. 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. 4732, pp. 86–101. Springer, Heidelberg (2007)

   Chapter  Google Scholar 

7. Hall, C., Hammond, K., Jones, S.P., Wadler, P.: Type classes in haskell. ACM Transactions on Programming Languages and Systems 18, 241–256 (1996)

   Article  Google Scholar 

8. Luo, Z.: Coercive subtyping. J. Logic and Computation 9(1), 105–130 (1999)

   Article  MathSciNet  MATH  Google Scholar 

9. Luo, Z.: Manifest fields and module mechanisms in intensional type theory. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941. Springer, Heidelberg (2008)

   Google Scholar 

10. Sacerdoti Coen, C., Tassi, E.: Working with mathematical structures in type theory. In: Miculan, M., Scagnetto, I., Honsell, F. (eds.) TYPES 2007. LNCS, vol. 4941, pp. 157–172. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

11. Sacerdoti Coen, C., Tassi, E.: A constructive and formal proof of Lebesgue’s dominated convergence theorem in the interactive theorem prover Matita. Journal of Formalized Reasoning 1, 51–89 (2008)

    MathSciNet  MATH  Google Scholar 

12. Saibi, A.: Typing algorithm in type theory with inheritance. In: The 24th Annual ACM SIGPLAN - SIGACT Symposium on Principle of Programming Language (POPL) (1997)

    Google Scholar 

13. Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

14. The Coq Development Team. The Coq proof assistant reference manual (2005), http://coq.inria.fr/doc/main.html

15. 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–76. ACM, New York (1989)

    Google Scholar 

16. Wenzel, M.: Type classes and overloading in higher-order logic. In: Gunter, E.L., Felty, A.P. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 307–322. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

Download references