+@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{gmetadom,
- author = "Luca Padovani and Claudio Sacerdoti Coen and Stefano Zacchiroli",
+ author = "Luca Padovani and Claudio {Sacerdoti Coen} and Stefano Zacchiroli",
title = "A Generative Approach to the Implementation of Language Bindings for the Document Object Model",
booktitle = "Generative Programming and Component Engineering",
editor = "Gabor Karsai and Eelco Visser",
}
@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,
}
@phdthesis{csc-phd,
- author = "Claudio Sacerdoti Coen",
+ author = "Claudio {Sacerdoti Coen}",
title = "Mathematical Knowledge Management and Interactive Theorem
Proving",
school = "University of Bologna",
}
@inproceedings{overkilling,
- author = "Sacerdoti Coen, Claudio",
+ author = "Claudio {Sacerdoti Coen}",
title = "Tactics in Modern Proof-Assistants: the Bad Habit of
Overkilling",
booktitle = "Supplementary Proceedings of the 14th International
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",
}
@inproceedings{csc-environment,
- author = "Claudio Sacerdoti Coen",
+ author = "Claudio {Sacerdoti Coen}",
title = "Mathematical Libraries as Proof Assistant Environments",
editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
booktitle = "Proceedings of Mathematical Knowledge Management 2004",
}
@inproceedings{disambiguation,
- author = "Claudio Sacerdoti Coen and Stefano Zacchiroli",
+ author = "Claudio {Sacerdoti Coen} and Stefano Zacchiroli",
title = "Efficient Ambiguous Parsing of Mathematical Formulae",
editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec",
booktitle = "Proceedings of Mathematical Knowledge Management 2004",
}
@inproceedings{whelp,
- author = "Andrea Asperti and Ferruccio Guidi and Claudio Sacerdoti Coen and Enrico Tassi and Stefano Zacchiroli",
+ author = "Andrea Asperti and Ferruccio Guidi and Claudio {Sacerdoti Coen}
+ 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"
}
@inproceedings{exportation-module,
- author = "Sacerdoti Coen, Claudio",
+ author = "Claudio {Sacerdoti Coen}",
title = "From Proof-Assistans to Distributed Libraries of Mathematics: Tips
and Pitfalls",
editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
}
@inproceedings{ida,
- author = "Andrea Asperti and Herman Geuvers and Iris Loeb and Lionel Elie Mamane and Claudio Sacerdoti Coen",
+ author = "Andrea Asperti and Herman Geuvers and Iris Loeb
+ and Lionel Elie Mamane and Claudio {Sacerdoti Coen}",
title = "An Interactive Algebra Course with Formalised Proofs and Definitions",
editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport",
booktitle = "Post-Proceedings of the Fourth International Conference on Mathematical Knowledge Management, MKM 2005",
}
@inproceedings{fguidisacerdot,
- author = "Ferruccio Guidi and Sacerdoti Coen, Claudio",
+ author = "Ferruccio Guidi and Claudio {Sacerdoti Coen}",
title = "Querying Distributed Digital Libraries of Mathematics",
editor = "Therese Hardin and Renaud Rioboo",
booktitle = "Calculemus 2003",
}
@inproceedings{hbugs,
- author = "Sacerdoti Coen, Claudio and Stefano Zacchiroli",
+ author = "Claudio {Sacerdoti Coen} and Stefano Zacchiroli",
title = "Brokers and {W}eb-Services for Automatic Deduction: a Case Study",
editor = "Therese Hardin and Renaud Rioboo",
booktitle = "Calculemus 2003",
}
@inproceedings{linda,
- author = "Sacerdoti Coen, Claudio",
+ author = "Claudio {Sacerdoti Coen}",
title = "A Constructive Proof of the Soundness of the
Encoding of Random Access Machines in a Linda Calculus with Ordered
Semantics",
year = "2003",
}
-
@article{asperti-categorical-understanding,
author = "Andrea Asperti",
title = "A categorical understanding of environment machines",
year = "1999"
}
+@TechReport{ctcoq2,
+ author = "Laurent Th\'ery and Yves Bertot and Gilles Kahn",
+ title = "Real Theorem Provers Deserve Real User-Interfaces",
+ month = may,
+ year = "1992",
+ institution = "INRIA",
+ number = "{Inria Research Report 1684}"
+}
+
@article{ctcoq3,
author = "Yves Bertot and Laurent Th\'ery",
title = "A Generic Approach to Building User Interfaces for Theorem Provers",
}
@mastersthesis{csc-master,
- author = "Sacerdoti Coen, Claudio",
+ author = "Claudio {Sacerdoti Coen}",
title = "Progettazione e realizzazione con tecnologia {XML} di basi distribuite di conoscenza matematica formalizzata",
school = "University of Bologna",
year = 2000
}
@misc{content-centric,
- author = "Andrea Asperti and Luca padovani and Claudio Sacerdoti Coen
- and irene Schena",
+ author = "Andrea Asperti and Luca padovani
+ and Claudio {Sacerdoti Coen} and irene Schena",
title = "Content-centric Logical Envirnoments",
howpublished = "Short Presentation at the Fifteenth IEEE Symposium on Logic in Computer Science",
month = "June",
@misc{debrujinfactor,
title = "The ``de Bruijn factor''",
howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}",
+ year = {2000},
author = "Freek Wiedijk",
}
@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"
}
title = "Mathematical {M}arkup {L}anguage ({MathML}) {V}ersion 2.0",
editor="{Patrick Ion} and others",
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/omdoc.ps}",
+ howpublished = "\\\url{http://www.mathweb.org/omdoc/pubs/omdoc1.1.pdf}",
+ year = {2005},
key = "OMDoc"
}
}
@TechReport{HELM,
- author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen
+ author = "Andrea Asperti and Luca Padovani and Claudio {Sacerdoti Coen}
and Irene Schena",
title = "Towards a library of formal mathematics",
year = "2000",
({TPHOLS}'2000), Portland, Oregon, USA",
}
-@TechReport{ctcoq2,
- author = "Laurent Th\'ery and Yves Bertot and Gilles Kahn",
- title = "Real Theorem Provers Deserve Real User-Interfaces",
- month = may,
- year = "1992",
- institution = "INRIA",
- number = "{Inria Research Report 1684}"
-}
-
@inproceedings{Ring,
author = "Samuel Boutin",
title = "Using Reflection to Build Efficient and Certified Decision
}
@inproceedings{remathematization,
- author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
- title = "{XML}, Stylesheets and the re-mathematization of Formal Content",
- booktitle = "EXTREME",
+ author = "Andrea Asperti and Luca Padovani
+ and Claudio {Sacerdoti Coen} and Irene Schena",
+ title = "{XML}, Stylesheets and the re-mathematization
+ of Formal Content",
+ booktitle = "Electronic Proceedings of {EXTREME Markup Languages} 2001",
year = "2001",
}
@article{mkm-helm,
author = "Andrea Asperti and Ferruccio Guidi and Luca Padovani and
- Claudio Sacerdoti Coen and Irene Schena",
+ Claudio {Sacerdoti Coen} and Irene Schena",
title = "Mathematical Knowledge Management in {HELM}",
journal = "Annals of Mathematics and Artificial Intelligence",
volume = "38(1-3)",
}
@unpublished{helm1,
- author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
+ author = "Andrea Asperti and Luca Padovani
+ and Claudio {Sacerdoti Coen} and Irene Schena",
title = "{Content Centric Logical Environments}",
note = "Short Presentation at LICS 2000",
ps = "http://www.cs.unibo.it/~asperti/HELM/lics_short.ps.gz",
}
@unpublished{helm4,
- author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
+ author = "Andrea Asperti and Luca Padovani
+ and Claudio {Sacerdoti Coen} and Irene Schena",
title = "{Formal Mathematics in MathML}",
note = "To be presented at MathML International Conference 2000",
}
@unpublished{helm2,
- author = "Andrea Asperti and Luca Padovani and Claudio Sacerdoti Coen and Irene Schena",
+ author = "Andrea Asperti and Luca Padovani
+ and Claudio {Sacerdoti Coen} and Irene Schena",
title = "{Towards a Library of Formal Mathematics}",
note = "Accepted at TPHOLS 2000",
ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz",
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" }
+
projects / helm.git / blobdiff