References

1. A. Asperti, W. Ricciotti, C. Sacerdoti Coen & E. Tassi (2009): A compact kernel for the Calculus of Inductive Constructions. Sadhana 34(1), pp. 71–144, doi:10.1007/s12046-009-0003-3.
2. A. Asperti, C. Sacerdoti Coen, E. Tassi & S. Zacchiroli (2007): User Interaction with the Matita Proof Assistant. Journal of Automated Reasoning 39(2), pp. 109–139, doi:10.1007/s10817-007-9070-5.
3. Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen & Enrico Tassi (2009): Hints in unification. In: TPHOLs 2009, LNCS 5674/2009. Springer-Verlag, pp. 84–98, doi:10.1007/978-3-642-03359-9_8.
4. Yves Bertot, Georges Gonthier, Sidi Ould Biha & Ioana Pasca (2008): Canonical Big Operators. In: TPHOLs, pp. 86–101, doi:10.1007/978-3-540-71067-7_11.
5. Thomas Braibant & Damien Pous (2009): A Tactic for Deciding Kleene Algebras. 1st Coq Workshop, doi:10.1007/978-3-642-14052-5_13. Available at http://hal.archives-ouvertes.fr/hal-00383070/fr/. (Available as a HAL report).
6. Claudio Sacerdoti Coen (2010): Declarative Representation of Proof Terms. J. Autom. Reasoning 44(1-2), pp. 25–52, doi:10.1007/s10817-009-9136-7.
7. Yann Coscoy (2000): Explication textuelle de preuves pour le Calcul des Constructions Inductives. Université de Nice-Sophia Antipolis.
8. Yann Coscoy, Gilles Kahn & Laurent Thery (1995): Extracting Text from Proofs. Technical Report RR-2459. Inria (Institut National de Recherche en Informatique et en Automatique), France, doi:10.1007/BFb0014048.
9. F. Garillot, G. Gonthier, A. Mahboubi & L. Rideau (2009): Packaging mathematical structures. In: TPHOLs 2009 fixme, pp. fixme, doi:10.1007/978-3-642-03359-9_23.
10. Ferruccio Guidi (2007): Procedural Representation of CIC Proof Terms. In: PLMMS, Workshop on Programming Languages for Mechanized Mathematics, doi:10.1007/s10817-009-9137-6. To appear.
11. Zhaohui Luo (1999): Coercive Subtyping. J. Logic and Computation 9(1), pp. 105–130, doi:10.1093/logcom/9.1.105. Available at http://www.oup.co.uk/logcom/hdb/Volume_09/Issue_01/090105.sgm.abs.html.
12. W. McCune (1992): Experiments with discrimination tree indexing and path indexing for term retrieval. Journal of Automated Reasoning 9(2), pp. 147–167, doi:10.1007/BF00245458.
13. R. Nieuwenhuis, T. Hillenbrand, A. Riazanov & A. Voronkov (2001): On the Evaluation of Indexing Techniques for Theorem Proving. LNCS 2083, pp. 257–271, doi:10.1007/3-540-45744-5_19. Available at citeseer.ist.psu.edu/nieuwenhuis03evaluation.html.
14. Robert Pollack (2002): Dependently Typed Records in Type Theory. Formal Aspects of Computing 13, pp. 386–402, doi:10.1007/s001650200018. Available at http://homepages.inf.ed.ac.uk/rpollack/export/recordsFAC.ps.gz.
15. C. Sacerdoti Coen & E. Tassi (2007): Working with Mathematical Structures in Type Theory. In: TYPES, LNCS 4941/2008, pp. 157–172.
16. M. Sozeau (2006): Subset Coercions in Coq. In: Types for Proofs and Programs, LNCS 4502/2007. Springer-Verlag, pp. 237–252, doi:10.1007/978-3-540-74464-1_16.
17. M. Sozeau & N. Oury (2008): First-Class Type Classes. In: TPHOLs, pp. 278–293, doi:10.1007/978-3-540-71067-7_23.
18. Matthieu Sozeau (2009): A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning 2(1), pp. 41–62.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org