X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita.bib;h=12b28d754d1f6ce16cac06afc061667e0d7b21a9;hb=112afe13b5aef27425d1a0bc9c71a70b491069bf;hp=79d527b45b5136c33c12de4c3d2b812a14ee29d6;hpb=cbac948d507d74a558ba7f11ce10bc252b1ba8ba;p=helm.git diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib index 79d527b45..12b28d754 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,7 +459,8 @@ } @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)", @@ -469,7 +470,7 @@ } @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", @@ -1151,7 +1161,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 +1170,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 +1202,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 +1292,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 +1339,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",