@inproceedings{GBOP:01,
  author = {Gilles Barthe and Olivier Pons},
  title = {Type Isomorphisms and Proof Reuse in Dependent Type Theory},
  booktitle = {FoSSaCS},
  publisher = {Springer},
  year = {2001},
  volume = {2030},
  pages = {57--71},
  url = {http://link.springer.de/link/service/series/0558/bibs/2030/20300057.htm}
}

@article{FBJJMO:08,
  author = {Frédéric Blanqui and Jean-Pierre Jouannaud and Mitsuhiro Okada},
  title = {Inductive-data-type Systems},
  journal = {Theoretical Computer Science},
  publisher = {HAL - CCSD},
  year = {2002},
  volume = {272},
  pages = {41 -- 68},
  url = {http://hal.inria.fr/inria-00105578/en}
}

@other{METAPRL,
  author = {Robert Constable},
  title = {The Metaprl proof assistant},
  year = {1981},
  note = { http://metaprl.org/Website}
}

@article{DiC:95,
  author = {Roberto Di Cosmo},
  title = {Second Order Isomorphic Types: A Proof Theoretic Study on Second Order lambda-Calculus with Surjective Paring and Terminal Object},
  journal = {Information and Compution},
  year = {1995},
  volume = {119},
  number = {2},
  pages = {176-201}
}

@inproceedings{LCBS:03,
  author = {Luís Cruz-Filipe and Bas Spitters},
  title = {Program Extraction from Large Proof Developments},
  booktitle = {TPHOLs},
  publisher = {Springer},
  year = {2003},
  volume = {2758},
  pages = {205--220},
  url = {http://springerlink.metapress.com/openurl.asp?genre=article&issn=0302-9743&volume=2758&spage=205}
}

@inproceedings{Del:00,
  author = {D. Delahaye},
  title = {Information Retrieval in a Coq Proof Library Using Type Isomorphisms},
  booktitle = {TYPES '99: Selected papers from the International Workshop on Types for Proofs and Programs},
  journal = {Lecture Notes in Computer Science},
  publisher = {Springer-Verlag},
  year = {2000},
  volume = {1956},
  pages = {131--147},
  note = {http://link.springer.de/link/service/series/0558/bibs/1956/19560131.htmElectronic Edition},
  url = {http://link.springer.de/link/service/series/0558/bibs/1956/19560131.htm}
}

@inproceedings{FM:94,
  author = {A. Felty and D. Howe},
  title = {Generalization and Reuse of Tactic Proofs},
  booktitle = {5th International Conference on Logic Programming and Automated Reasoning},
  publisher = {Springer-Verlag },
  year = {1994},
  volume = {822},
  pages = {1--15},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.1064Electronic Edition}
}

@article{PG:00,
  author = {Philippe de Groote},
  title = {Proof-Search in Implicative Linear Logic as a Matching Problem},
  journal = {Lecture Notes in Computer Science},
  year = {2000},
  volume = {1955},
  pages = {257--??},
  url = {http://link.springer-ny.com/link/service/series/0558/bibs/1955/19550257.htm; http://link.springer-ny.com/link/service/series/0558/papers/1955/19550257.pdf}
}

@incollection{KW:98,
  author = {T. Kolbe and C. Walther},
  title = {Proof Analysis, Generalization, and Reuse},
  booktitle = {Automated Deduction: A Basis for Applications.},
  publisher = {Kluwer Academic Publishers},
  year = {1998},
  volume = {Volume II, Systems and Implementation Techniques},
  note = {http://www.inferenzsysteme.informatik.tu-darmstadt.de/~walther/Paper/Proof_Analysis_Generalization_and_Reuse.psElectronic Edition },
  url = {http://www.inferenzsysteme.informatik.tu-darmstadt.de/~walther/Paper/Proof_Analysis_Generalization_and_Reuse.ps}
}

@inproceedings{KT:95,
  author = {T. Kolbe and C. Walther},
  title = {Second-Order Matching modulo Evaluation: A Technique for Reusing Proofs},
  booktitle = {Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence},
  publisher = {Morgan Kaufmann},
  year = {1995},
  pages = {190--195},
  note = {http://www.inferenzsysteme.informatik.tu-darmstadt.de/~walther/Paper/Second-Order-Matching-mod-Eval-IJCAI-1995.pdfElectronic Edition},
  url = {http://www.inferenzsysteme.informatik.tu-darmstadt.de/~walther/Paper/Second-Order-Matching-mod-Eval-IJCAI-1995.pdf}
}

@inproceedings{MB:02,
  author = {N. Magaud and Y. Bertot},
  title = {Changing Data Structures in Type Theory: A Study of Natural Numbers},
  booktitle = {TYPES, International Workshop on Types for Proofs and Programs},
  journal = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  year = {2000},
  volume = {2277},
  pages = {181 - 196},
  note = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.8.3073Electronic Edition}
}

@article{DM:91a,
  author = {Dale Miller and Gopalan Nadathur and Frank Pfenning and Andre Scedrov},
  title = {Uniform Proofs as a Foundation for Logic Programming},
  journal = {Annals of Pure and Applied Logic},
  year = {1991},
  volume = {51},
  number = {1--2},
  pages = {125--157}
}

@inproceedings{TN:90,
  author = {Tobias Nipkow},
  title = {Proof Transformations for Equational Theories},
  booktitle = {LICS},
  publisher = {IEEE Computer Society},
  year = {1990},
  pages = {278--288}
}

@inproceedings{Pad:96,
  author = {V. Padovani},
  title = {Decidability of All Minimal Models},
  booktitle = {TYPES '95: Selected papers from the International Workshop on Types for Proofs and Programs},
  journal = {Lecture Notes in Computer Science},
  publisher = {Springer Verlag},
  year = {1996},
  volume = {1158},
  pages = {201--??},
  note = {http://dx.doi.org/10.1007/3-540-61780-9_71Electronic Edition,},
  doi = {http://dx.doi.org/10.1007/3-540-61780-9_71}
}

@phdthesis{Pym:90,
  author = {D. Pym},
  title = {Proofs, Search and Computation in General Logic},
  school = {Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh},
  year = {1990},
  number = {CST-69-90},
  note = {http://www.lfcs.inf.ed.ac.uk/reports/90/ECS-LFCS-90-125/Electronic Edition},
  url = {http://www.lfcs.inf.ed.ac.uk/reports/90/ECS-LFCS-90-125/}
}

@misc{Zer:08,
  author = {E. Zermelo},
  title = {A new proof of the possibility of a well ordering},
  year = {1908}
}

@other{Coq,,
  title = {The Coq Proof Assistant},
  year = {1992},
  note = { http://coq.inria.fr/Website},
  url = {http://coq.inria.fr/}
}