X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita.bib;h=bd7b0baee43f855c0ac9788228e5a7880b922609;hb=808a892e0a16067a22eb25c3d8182fe71de3ac9a;hp=5b53ac0b9adbc95f16e08c610277006cce23b59d;hpb=af95120ce01907e21b53ebcf23e085590fa9eb04;p=helm.git diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib index 5b53ac0b9..bd7b0baee 100644 --- a/helm/papers/matita/matita.bib +++ b/helm/papers/matita/matita.bib @@ -1,6 +1,27 @@ +@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}, + booktitle = {MKM '03: Proceedings of the Second International Conference on Mathematical Knowledge Management}, + year = {2003}, + isbn = {3-540-00568-4}, + pages = {66--79}, + publisher = {Springer-Verlag}, + address = {London, UK}, +} + @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", @@ -56,12 +77,12 @@ } @inproceedings{proof-by-pointing, - author = "Yves Bertot", + author = "Yves Bertot and Gilles Kahn and Laurent Théry", 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, @@ -126,7 +147,7 @@ } @phdthesis{csc-phd, - author = "Claudio Sacerdoti Coen", + author = "Claudio {Sacerdoti Coen}", title = "Mathematical Knowledge Management and Interactive Theorem Proving", school = "University of Bologna", @@ -167,7 +188,7 @@ } @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 @@ -276,6 +297,16 @@ 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", @@ -415,7 +446,7 @@ } @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", @@ -426,7 +457,7 @@ } @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", @@ -448,17 +479,18 @@ } @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", @@ -471,7 +503,8 @@ } @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", @@ -494,7 +527,7 @@ } @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", @@ -505,7 +538,7 @@ } @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", @@ -527,7 +560,7 @@ } @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", @@ -538,7 +571,6 @@ year = "2003", } - @article{asperti-categorical-understanding, author = "Andrea Asperti", title = "A categorical understanding of environment machines", @@ -568,6 +600,15 @@ 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", @@ -876,7 +917,7 @@ } @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 @@ -912,6 +953,15 @@ year = 1998 } +@misc{content-centric, + 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", + year = "2000", + key = "content centric" +} @misc{mowgli-proposal, title = "The {MoWGLI Proposal}, {HTML} Version", @@ -922,6 +972,7 @@ @misc{debrujinfactor, title = "The ``de Bruijn factor''", howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}", + year = {2000}, author = "Freek Wiedijk", } @@ -938,6 +989,14 @@ key = "ALF" } +@misc{CoqManual, + title = "The {C}oq Proof Assistant Reference Manual", + author = "{The Coq Development Team}", + howpublished = "\\\url{http://coq.inria.fr/doc/main.html}", + year = {2005}, + key = "CoqManual" +} + @misc{Coq, title = "The {C}oq proof-assistant", howpublished = "\\\url{http://coq.inria.fr}", @@ -953,7 +1012,6 @@ @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" } @@ -976,6 +1034,17 @@ key = "Isabelle" } +@book{nuprl-book, + author = "Constable, Robert L. and Stuart F. Allen and H. M. Bromley and + W. R. Cleaveland and J. F. Cremer and R. W. Harper and Douglas J. Howe and + T. B. Knoblock and N. P. Mendler and P. Panangaden and James T. Sasaki and + Scott F. Smith", + title = "Implementing Mathematics with the {N}uprl Development System", + publisher = "Prentice-Hall", + year = 1986, + address = "NJ" +} + @misc{nuprl, title = "The {NuPRL} proof-assistant", howpublished = "\\\url{http://www.cs.cornell.edu/Info/Projects/NuPrl/nuprl.html}", @@ -1017,8 +1086,9 @@ 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, @@ -1027,7 +1097,7 @@ editor="{Tim Bray} and others", 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, @@ -1073,7 +1143,8 @@ editor="{Tim Bray} and others", @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" } @@ -1113,7 +1184,7 @@ editor="{Tim Bray} and others", } @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", @@ -1122,15 +1193,6 @@ editor="{Tim Bray} and others", ({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 @@ -1163,8 +1225,10 @@ editor="{Tim Bray} and others", } @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", + 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", year = "2001", } @@ -1251,7 +1315,7 @@ editor="{Tim Bray} and others", @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)", @@ -1298,20 +1362,23 @@ editor="{Tim Bray} and others", } @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", @@ -1518,3 +1585,11 @@ elettroniche}", year="1997" } +@inproceedings{barthe95implicit, + author = "Gilles Barthe", + title = "Implicit Coercions in Type Systems", + booktitle = "{TYPES}", + pages = "1-15", + year = "1995", + url = "citeseer.ist.psu.edu/barthe95implicit.html" } +