@article(ck-sadhana-shortbib,
 author       = "A. Asperti and W. Ricciotti and C. {Sacerdoti Coen} and E. Tassi",
 year         = "2009",
 title        = "A compact kernel for the {C}alculus of {I}nductive {C}onstructions",
 journal      = "Sadhana",
 volume       = "34",
 number       = "1",
 pages        = "71--144",
 doi          = "10.1007/s12046-009-0003-3",
)
@article(matita-jar-uitp-shortbib,
 author       = "A. Asperti and C. {Sacerdoti Coen} and E. Tassi and S. Zacchiroli",
 year         = "2007",
 title        = "User Interaction with the {M}atita Proof Assistant",
 journal      = "Journal of Automated Reasoning",
 volume       = "39",
 number       = "2",
 pages        = "109--139",
 doi          = "10.1007/s10817-007-9070-5",
)
@inproceedings(unification-hints,
 author       = "Andrea Asperti and Wilmer Ricciotti and Claudio {Sacerdoti Coen} and Enrico Tassi",
 year         = "2009",
 title        = "Hints in unification",
 booktitle    = "TPHOLs 2009",
 series       = "LNCS",
 volume       = "5674/2009",
 publisher    = "Springer-Verlag",
 pages        = "84--98",
 doi          = "10.1007/978-3-642-03359-9\_8",
)
@inproceedings(BigOps,
 author       = "Yves Bertot and Georges Gonthier and Sidi Ould Biha and Ioana Pasca",
 year         = "2008",
 title        = "Canonical Big Operators",
 booktitle    = "TPHOLs",
 pages        = "86--101",
 doi          = "10.1007/978-3-540-71067-7\_11",
)
@misc(kacoq,
 author       = "Thomas Braibant and Damien Pous",
 year         = "2009",
 title        = "A Tactic for Deciding Kleene Algebras",
 howpublished = "1st Coq Workshop",
 doi          = "10.1007/978-3-642-14052-5\_13",
 url          = "http://hal.archives-ouvertes.fr/hal-00383070/fr/",
 note         = "(Available as a HAL report)",
)
@article(csc-decl,
 author       = "Claudio Sacerdoti Coen",
 year         = "2010",
 title        = "Declarative Representation of Proof Terms",
 journal      = "J. Autom. Reasoning",
 volume       = "44",
 number       = "1-2",
 pages        = "25--52",
 doi          = "10.1007/s10817-009-9136-7",
)
@phdthesis(YANNTHESIS,
 author       = "Yann Coscoy",
 year         = "2000",
 title        = "Explication textuelle de preuves pour le {C}alcul des {C}onstructions {I}nductives",
 school       = "Universit\'e de Nice-Sophia Antipolis",
)
@techreport(natural,
 author       = "Yann Coscoy and Gilles Kahn and Laurent Thery",
 year         = "1995",
 title        = "{Extracting Text from Proofs}",
 type         = "Technical Report",
 number       = "RR-2459",
 institution  = "Inria (Institut National de Recherche en Informatique et en Automatique), France",
 doi          = "10.1007/BFb0014048",
)
@inproceedings(canonical-structures,
 author       = "F. Garillot and G. Gonthier and A. Mahboubi and L. Rideau",
 year         = "2009",
 title        = "Packaging mathematical structures",
 booktitle    = "TPHOLs 2009",
 volume       = "fixme",
 pages        = "fixme",
 doi          = "10.1007/978-3-642-03359-9\_23",
)
@inproceedings(fguidi-proc,
 author       = "Ferruccio Guidi",
 year         = "2007",
 title        = "Procedural Representation of CIC Proof Terms",
 booktitle    = "PLMMS, Workshop on Programming Languages for Mechanized Mathematics",
 doi          = "10.1007/s10817-009-9137-6",
 note         = "To appear",
)
@article(coercivesubtyping,
 author       = "Zhaohui Luo",
 year         = "1999",
 title        = "Coercive Subtyping",
 journal      = "J. Logic and Computation",
 volume       = "9",
 number       = "1",
 pages        = "105--130",
 doi          = "10.1093/logcom/9.1.105",
 url          = "http://www.oup.co.uk/logcom/hdb/Volume_09/Issue_01/090105.sgm.abs.html",
)
@article(McCune,
 author       = "W. McCune",
 year         = "1992",
 title        = "Experiments with discrimination tree indexing and path indexing for term retrieval",
 journal      = "Journal of Automated Reasoning",
 volume       = "9(2)",
 pages        = "147--167",
 doi          = "10.1007/BF00245458",
)
@article(nieuwenhuis01evaluation-shortbib,
 author       = "R. Nieuwenhuis and T. Hillenbrand and A. Riazanov and A. Voronkov",
 year         = "2001",
 title        = "On the Evaluation of Indexing Techniques for Theorem Proving",
 journal      = "LNCS",
 volume       = "2083",
 pages        = "257--271",
 doi          = "10.1007/3-540-45744-5\_19",
 url          = "citeseer.ist.psu.edu/nieuwenhuis03evaluation.html",
)
@article(pollackFAC02,
 author       = "Robert Pollack",
 year         = "2002",
 title        = "Dependently Typed Records in Type Theory",
 journal      = "Formal Aspects of Computing",
 volume       = "13",
 pages        = "386--402",
 doi          = "10.1007/s001650200018",
 url          = "http://homepages.inf.ed.ac.uk/rpollack/export/recordsFAC.ps.gz",
)
@inproceedings(coercions-record-shortbib,
 author       = "C. {Sacerdoti Coen} and E. Tassi",
 year         = "2007",
 title        = "Working with Mathematical Structures in Type Theory",
 booktitle    = "TYPES",
 series       = "LNCS",
 volume       = "4941/2008",
 pages        = "157--172",
)
@inproceedings(russell-shortbib,
 author       = "M. Sozeau",
 year         = "2006",
 title        = "Subset Coercions in {C}oq",
 booktitle    = "Types for Proofs and Programs",
 series       = "LNCS",
 volume       = "4502/2007",
 publisher    = "Springer-Verlag",
 pages        = "237--252",
 doi          = "10.1007/978-3-540-74464-1\_16",
)
@inproceedings(SozeauO08-shortbib,
 author       = "M. Sozeau and N. Oury",
 year         = "2008",
 title        = "First-Class Type Classes",
 booktitle    = "TPHOLs",
 pages        = "278--293",
 doi          = "10.1007/978-3-540-71067-7\_23",
)
@article(type-classes-coq,
 author       = "Matthieu Sozeau",
 year         = "2009",
 title        = "A New Look at Generalized Rewriting in Type Theory",
 journal      = "Journal of Formalized Reasoning",
 volume       = "2",
 number       = "1",
 pages        = "41--62",
)