X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita.bib;h=8aa1c4882a5aecce42eec255e484ab6d85b44031;hb=0ef468f9000a8e9c391cc8ade2f9aea35e878305;hp=79d527b45b5136c33c12de4c3d2b812a14ee29d6;hpb=cbac948d507d74a558ba7f11ce10bc252b1ba8ba;p=helm.git diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib index 79d527b45..8aa1c4882 100644 --- a/helm/papers/matita/matita.bib +++ b/helm/papers/matita/matita.bib @@ -11,7 +11,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", @@ -137,7 +137,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 +178,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 @@ -426,7 +426,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 +437,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 +459,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 +483,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 +507,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 +518,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 +540,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", @@ -549,7 +551,6 @@ year = "2003", } - @article{asperti-categorical-understanding, author = "Andrea Asperti", title = "A categorical understanding of environment machines", @@ -579,6 +580,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", @@ -887,7 +897,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 @@ -924,8 +934,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", @@ -942,6 +952,7 @@ @misc{debrujinfactor, title = "The ``de Bruijn factor''", howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}", + year = {2000}, author = "Freek Wiedijk", } @@ -960,8 +971,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" } @@ -980,7 +992,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" } @@ -1055,8 +1066,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, @@ -1065,7 +1077,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, @@ -1111,7 +1123,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" } @@ -1151,7 +1164,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", @@ -1160,15 +1173,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 @@ -1201,8 +1205,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", } @@ -1289,7 +1295,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)", @@ -1336,20 +1342,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", @@ -1556,3 +1565,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" } +