X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita.bib;h=19d2df5dc1fd6563a8e7a4b6b342ffbbd358448a;hb=c1986639552e01334a05db4236627a6c1ffacf21;hp=d82d7d4d9e50928dba91a3aa2b4f97ff87928ea8;hpb=1aad2bcf697c0b65560fe33b4f98d9f353514be4;p=helm.git diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib index d82d7d4d9..19d2df5dc 100644 --- a/helm/papers/matita/matita.bib +++ b/helm/papers/matita/matita.bib @@ -1,4 +1,14 @@ +@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}, @@ -11,7 +21,7 @@ } @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", @@ -41,7 +51,7 @@ } @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", @@ -67,12 +77,12 @@ } @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, @@ -137,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", @@ -178,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 @@ -287,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", @@ -301,7 +321,7 @@ @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, @@ -418,7 +438,7 @@ 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", @@ -426,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", @@ -437,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", @@ -459,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", @@ -482,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", @@ -505,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", @@ -516,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", @@ -538,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", @@ -895,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 @@ -932,8 +954,8 @@ } @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", @@ -950,6 +972,7 @@ @misc{debrujinfactor, title = "The ``de Bruijn factor''", howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}", + year = {2000}, author = "Freek Wiedijk", } @@ -968,8 +991,9 @@ @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" } @@ -988,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" } @@ -1063,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, @@ -1073,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, @@ -1118,8 +1142,10 @@ 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}", + 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" } @@ -1159,7 +1185,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", @@ -1200,9 +1226,11 @@ 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", - 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", } @@ -1288,7 +1316,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)", @@ -1335,20 +1363,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", @@ -1555,3 +1586,11 @@ elettroniche}", 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" } +