+@book{paramodulation,
+ author = "Robert Nieuwenhuis and Alberto Rubio",
+ title = "Paramodulation-based thorem proving",
+ booktitle = "Handbook of Automated Reasoning",
+ pages = "471--443",
+ publisher = "Elsevier and MIT Press",
+ year = 2001,
+ NOTE = {ISBN-0-262-18223-8}
+}
+
@inproceedings{latexmathml,
author = {Luca Padovani},
title = {On the Roles of LATEX and MathML in Encoding and Processing Mathematical Expressions},
}
@inproceedings{thery-authoring,
- author = "Laurent Th\`ery",
+ author = "Laurent {Th\'ery}",
title = "Formal Proof Authoring: an Experiment",
booktitle = "User Interface Design for Theorem Provers",
editor = "David Aspinall and Christoph L{\"u}th",
}
@inproceedings{proof-by-pointing,
- author = "Yves Bertot",
+ author = "Yves Bertot and Gilles Kahn and Laurent Th\'ery",
title = "Proof by Pointing",
booktitle = "Symposium on Theoretical Aspects Computer Software (STACS)",
series = "Lecture Notes in Computer Science",
volume = "789",
- year = 1993
+ year = 1994
}
@inproceedings{thery-cyp,
year = 1989
}
+@book{CoqArt,
+ author = "Yves Bertot and Pierre Castéran",
+ title = "{Interactive Theorem Proving and Program Development}",
+ publisher = {Springer Verlag},
+ series = {Texts in Theoretical Computer Science},
+ year = 2004,
+ NOTE = {ISBN-3-540-20854-2}
+
+}
+
@inproceedings{proofgeneral,
author = "David Aspinall",
title = "{P}roof {G}eneral: A Generic Tool for Proof Development",
@inproceedings{Gim94,
author = "Eduardo Gim\'enez",
title = "{Codifying guarded definitions with recursive schemes}",
- booktitle = "Types'94: Types for Proofs and Programs",
+ booktitle = "Types for Proofs and Programs: International Workshop, {TYPES '94}",
series = "LNCS",
volume = 996,
year = 1994,
author = "Alexandre Miquel and Benjamin Werner",
title = "The Not So Simple Proof-Irrelevant Model of {CC}",
editor = "Herman Geuvers and Freek Wiedijk",
- booktitle = "Types for Proofs and Programs: International Workshop, TYPES 2002",
+ booktitle = "Types for Proofs and Programs: International Workshop, {TYPES 2002}",
pages = "240--258",
volume = "LNCS, 2646",
publisher = "Springer-Verlag",
and Enrico Tassi and Stefano Zacchiroli",
title = "A content based mathematical search engine: Whelp",
booktitle = "Post-proceedings of the Types 2004 International Conference",
- volume = "LNCS, (to appear)",
- pages = "xxx--xxx",
+ volume = "LNCS, 3839",
+ pages = "17--32",
publisher = "Springer-Verlag",
year = "2004"
}
@misc{CoqManual,
title = "The {C}oq Proof Assistant Reference Manual",
- author = "The Coq Development Team",
+ author = "{The Coq Development Team}",
howpublished = "\\\url{http://coq.inria.fr/doc/main.html}",
year = {2005},
key = "CoqManual"
@misc{lego,
title = "The {L}ego proof-assistant",
howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}",
- url = "\url{http://www.dcs.ed.ac.uk/home/lego/}",
key = "Lego"
}
howpublished = "W3C Recommendation 21 February 2001, \url{http://www.w3.org/TR/MathML2}",
year = {2003},
url = "\url{http://www.w3.org/TR/MathML2}",
- key = "Mathematical"
+ key = "MathML"
}
@misc{xml,
howpublished = "W3C Recommendation 10 February 1998,
\url{http://www.w3.org/TR/REC-xml}",
url = "\url{http://www.w3.org/TR/REC-xml}",
- key = "Extensible"
+ key = "XML"
}
@misc{dom,
}
@misc{omdoc,
- title = "{OMDoc}: An Open Markup Format for Mathematical Documents (Version 1.1)",
- howpublished = "\\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.1.pdf}",
+ title = "{OMDoc}: An Open Markup Format for Mathematical Documents
+(Draft, Version 1.2)",
+ howpublished = "\\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.2.pdf}",
year = {2005},
key = "OMDoc"
}
and Claudio {Sacerdoti Coen} and Irene Schena",
title = "{XML}, Stylesheets and the re-mathematization
of Formal Content",
- booktitle = "EXTREME",
+ booktitle = "Electronic Proceedings of {EXTREME Markup Languages} 2001",
year = "2001",
}
year="1997"
}
+@inproceedings{barthe95implicit,
+ author = "Gilles Barthe",
+ title = "Implicit Coercions in Type Systems",
+ booktitle = "Types for Proofs and Programs: International Workshop, {TYPES 1995}",
+ pages = "1-15",
+ year = "1995",
+ url = "citeseer.ist.psu.edu/barthe95implicit.html" }
+