X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita.bib;fp=helm%2Fpapers%2Fmatita%2Fmatita.bib;h=0000000000000000000000000000000000000000;hb=85747dc6d0578b484544bb8120aad7aa89813f27;hp=19d2df5dc1fd6563a8e7a4b6b342ffbbd358448a;hpb=c1986639552e01334a05db4236627a6c1ffacf21;p=helm.git diff --git a/helm/papers/matita/matita.bib b/helm/papers/matita/matita.bib deleted file mode 100644 index 19d2df5dc..000000000 --- a/helm/papers/matita/matita.bib +++ /dev/null @@ -1,1596 +0,0 @@ - -@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", - 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", - series = "LNCS", - volume = "3286", - pages = "469--487", - publisher = "Springer-Verlag", - year = 2004, -} - -@techreport{mmode, - author = "Freek Wiedijk", - title = "MMode, a Mizar Mode for the proof assistant Coq", - institution = "University of Nijmegen", - number = "NIII-R0333", - year = "2003" -} - -@article{ lamport-proof, - author = "Leslie Lamport", - title = "How to write a proof", - journal = "American Mathematical Monthly", - volume = "102", - number = "7", - pages = "600--608", - year = "1995", -} - -@inproceedings{thery-authoring, - 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", - year = 2003 -} - -@inproceedings{padovani-editex, - author = "Luca Padovani", - title = "Interactive Editing of MathML Markup Using TeX Syntax", - booktitle = "International Conference on TeX, XML, and Digital Typography", - series = "LNCS", - volume = "3130,", - pages = "125--138", - year = 2004, - publisher = "Springer-Verlag", -} - -@inproceedings{uitp-knowledge-modelling, - author = "Stuart Aitken", - title = "Problem Solving in Interactive Proof: A Knowledge-Modelling Approach", - booktitle = "European Conference on Artificial Intelligence (ECAI)", - year = 1996 -} - -@inproceedings{proof-by-pointing, - 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 = 1994 -} - -@inproceedings{thery-cyp, - author = "Laurent Th\`ery", - title = "Colouring proofs: a lightweight approach to adding formal structure to proofs", - booktitle = "User Interface Design for Theorem Provers", - editor = "David Aspinall and Christoph L{\"u}th", - year = 2003 -} - -@article{uitp-empirical, - author = "Stuart Aitken and Phil Gray and Tom Melham and Muffy Thomas", - title = "Interactive Theorem Proving: An Empirical Study of User Activity", - journal = "Journal of Symbolic Computation", - year = 1995 -} - -@inproceedings{uitp-phases, - author = "Stuart Aitken and Phil Gray and Tom Melham and Muffy Thomas", - title = "Phases, Modes and Information Flow in Theory Development", - booktitle = "User Interface Design for Theorem Provers", - editor = "Nicholas Merriam", - year = 1996 -} - -@inproceedings{searchingmath, - author = "Andrea Asperti and Stefano Zacchiroli", - title = "Searching mathematics on the Web: state of the art and future developments", - booktitle = "New Developments in Electronic Publishing of Mathematics", - editor = "Bernd Wegner", - publisher = {FIZ Karlsruhe}, - YEAR = 2005 -} - -@article{fourcolor, - author = "K. Appel and W. Haken", - title = "Every planar map is four colorable.", - journal = {Illinois Journal of Mathematics}, - year = 1977, - volume = {21}, - pages = {429--567} -} - -@misc{freekcomparison, - author = "Freek Wiedijk", - title = "The Sixteen Provers of the World", - howpublished = "University of Nijmegen,\\\url{http://www.cs.ru.nl/~freek/comparison/comparison.ps.gz}" -} - -@misc{zmath, - title = "Zentralblatt MATH", - howpublished = "\url{http://www.emis.de/ZMATH/}" -} - -@inproceedings{lcf, - author = "Michael J. C. Gordon and Robin Milner and C.P. Wadsworth", - title = "{Edinburgh LCF}: a Mechanised Logic of Computation", - series = {Lecture Notes in Computer Science}, - volume = 78, - publisher = {{Sprin\-ger-Verlag}}, - year = 1979 -} - -@phdthesis{csc-phd, - author = "Claudio {Sacerdoti Coen}", - title = "Mathematical Knowledge Management and Interactive Theorem - Proving", - school = "University of Bologna", - year = "2004", - note = "Technical Report UBLCS 2004-5" -} - -@inproceedings{Isar, - author = "Markus Wenzel", - title = "Isar - A Generic Interpretative Approach to Readable Formal Proof Documents", - booktitle = "Theorem Proving in Higher Order Logics", - pages = "167-184", - year = "1999" -} - -@inproceedings{centaur, - author = "P. Borras and D. Clement and Th. Despeyrouz and J. Incerpi and G. Kahn and B. Lang and V. Pascual", - title = "{CENTAUR}: The System", - booktitle = "Proceedings of the {ACM} {SIGSOFT}/{SIGPLAN} Software Engineering Symposium on Practical Software Development Environments ({PSDE})", - journal = "SIGPLAN Notices", - volume = "24", - number = "2", - publisher = "ACM Press", - address = "New York, NY", - pages = "14--24", - year = "1989", - url = "citeseer.nj.nec.com/borras88centaur.html" -} - -@inproceedings{Leroy-manifest-types, - AUTHOR = "Xavier Leroy", - TITLE = "Manifest types, modules, and separate compilation", - BOOKTITLE = {21st symposium Principles of Programming Languages}, - YEAR = 1994, - PUBLISHER = {ACM Press}, - PAGES = {109--122}, - URL = {http://pauillac.inria.fr/~xleroy/publi/manifest-types-popl.ps.gz} -} - -@inproceedings{overkilling, - author = "Claudio {Sacerdoti Coen}", - title = "Tactics in Modern Proof-Assistants: the Bad Habit of - Overkilling", - booktitle = "Supplementary Proceedings of the 14th International - Conference TPHOLS 2001", - pages = {352--367}, - year = 2001 -} - -@inproceedings{omegaants1, - author = "Christoph Benzm{\"u}ller and Volker Sorge", - title = {{OANTS} -- An open approach at combining Interactive and Automated - Theorem Proving}, - booktitle = {Symbolic Computation and Automated Reasoning}, - editor = {Manfred Kerber and Michael Kohlhase}, - year = 2000, - pages = {81--97}, - publisher = {A.K.Peters}, - url = {www.ags.uni-sb.de/~chris/papers/C8.pdf} -} - -@article{ocr, - author = "R. Fateman and T. Tokuyasu and B. Berman and N. Mitchell", - title = {Optical Character Recognition and Parsing of Typeset Mathematics}, - journal = {Journal of Visual Communication And Image Representation}, - year = 1996, - volume = {7}, - pages = {2--15}, - number = {1}, - month = mar, - url = {www.ags.uni-sb.de/~chris/papers/J4.pdf} -} - -@article{newauthomath, - author = "Freek Wiedijk", - title = "A new implementation of {A}utomath", - journal = {Journal of Automated Reasoning}, - year = 2002, - volume = {29}, - pages = {365--387} -} - -@article{gdome2, - author = "Paolo Casarini and Luca Padovani", - title = "The {G}nome {DOM} {E}ngine", - journal = "Markup Languages: Theory \& Practice", - year = 2002, - volume = {3}, - pages = {173--190}, - number = {2}, - publisher = "MIT Press", - month = apr -} - -@article{omegaants2, - author = "Christoph Benzm{\"u}ller and Mateja Jamnik and Manfred Kerber and - Volker Sorge", - title = {Agent based Mathematical Reasoning}, - journal = {Electronic Notes in Theoretical Computer Science, Elsevier}, - year = 1999, - volume = {23}, - pages = {21--33}, - number = {3}, - url = {www.ags.uni-sb.de/~chris/papers/J4.pdf} -} - -@inproceedings{Necula, - author = "George C. Necula and Peter Lee", - title = "Safe Kernel Extensions Without Run-Time Checking", - booktitle = "2nd Symposium on Operating Systems Design and Implementation ({OSDI} '96), October 28--31, 1996. Seattle, {WA}", - publisher = "USENIX", - address = "Berkeley, CA, USA", - editor = "{USENIX}", - pages = "229--243", - year = "1996", - url = "citeseer.nj.nec.com/necula96safe.html" -} - -@inproceedings{courant, - AUTHOR = "Judica{\"e}l Courant", - TITLE = {Explicit Universes for the {C}alculus of {C}onstructions}, - BOOKTITLE = {Theorem Proving in Higher Order Logics: - 15th International Conference, TPHOLs 2002}, - EDITOR = {Victor A. {Carre\~{n}o} and C\'{e}sar A. {Mu\~{n}oz} and Sofi\`{e}ne Tahar}, - SERIES = {Lecture Notes in Computer Science}, - VOLUME = 2410, - PAGES = {115--130}, - YEAR = 2002, - PUBLISHER = {{Sprin\-ger-Verlag}}, - MONTH = AUG, - ADDRESS = {Hampton, VA, USA} -} - -@inproceedings{NL98, - author = "George C. Necula and Peter Lee", - title="{Efficient Representation and Validation of Proofs}", - booktitle="Proceedings of the 13th Annual symposium on Logic in Computer Science,", - address="Indianapolis", - year="1998" -} - -@book{GirardJY:prot, - author = "Jean-Yves Girard and Yves Lafont and Paul Taylor", - title = "{Proofs and Types}", - publisher = {Cambridge University Press}, - series = {Cambridge Tracts in Theoretical Computer Science}, - 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", - booktitle = "Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000", - series = "LNCS", - volume = "1785", - month = jan, - year = 2000, - publisher = "Springer-Verlag", -} - -@inproceedings{Gim94, - author = "Eduardo Gim\'enez", - title = "{Codifying guarded definitions with recursive schemes}", - booktitle = "Types for Proofs and Programs: International Workshop, {TYPES '94}", - series = "LNCS", - volume = 996, - year = 1994, - publisher = "Springer-Verlag", - note = "Extended version in LIP research report 95-07, ENS Lyon", - pages = "39--59", -} - -@incollection{BarendregtH:lawcwt, - author = "H. Barendregt", - title = "{Lambda Calculi with Types}", - booktitle = "{Handbook of Logic in Computer Science}", - editor = "{Abramsky, Samson and others}", - publisher = "{Oxford University Press}", - volume = 2, - year = 1992 -} - -@inproceedings{coquand:1986, - author="Thierry Coquand", - title="{An Analysis of Girard's Paradox}", - booktitle="Symposium on Logic in Computer Science", - address="Cambridge", - publisher="MA. IEEE press", - year="1986" -} - -@phdthesis{mohring, - AUTHOR = "Christine Paulin-Mohring", - TITLE = {D\'efinitions Inductives en Th\'eorie des Types d'Ordre Sup\'rieur}, - SCHOOL = {Universit\'e Claude Bernard Lyon I}, - YEAR = 1996, - MONTH = DEC, - TYPE = {Habilitation \`a diriger les recherches}, - URL = {http://www.lri.fr/~paulin/habilitation.ps.gz} -} - -@phdthesis{garrigue, - author = "Jacques Garrigue", - title = "{Label-Selective Lambda-Calculi and Transformation Calculi}", - school = "University of Tokyo, Department of Information Science", - month = mar, - year = 1995 -} - -@phdthesis{LuoZ:extcc, - author = "Zhaohui Luo", - title = "{An Extended Calculus of Constructions}", - school = "University of Edinburgh", - year = 1990 -} - -@phdthesis{chicly, - author = "Laurent Chicli", - title = "Sur la formalisation des math\'ematiques dans le - {C}alcul des {C}onstructions {I}nductives", - school = "Universit\'e de Nice~-~Sophia Antipolis", - year = 2003 -} - -@phdthesis{geuvers:1993, - author="Herman Geuvers", - title="{Logics and Type Systems}", - school="Catholic University Nijmegen", - year="1993", - type="{Ph.D.} dissertation" -} - -@unpublished{PrimesInP, - author = "M. Agrawal and N. Kayal and N. Saxena", - title = "{PRIMES} in {P}", - note = "\url{http://www.cse.iitk.ac.in/users/manindra/primality.ps}", - month = aug, - year = 2002 -} - -@unpublished{danosKAM, - author = "Vincent Danos and Laurent Regnier", - title = "How abstract machines implement head linear reduction", - year = 2003 -} - -@inproceedings{Oostdijk, - author = "Olga Caprotti and Herman Geuvers and Martin Oostdijk", - title = "Certified and Portable Mathematical Documents from Formal Contexts", - editor = "Bruno Buchberger and Olga Caprotti", - booktitle = "On-Line Proceedings of the First International Conference on - Mathematical Knowledge Management, MKM 2001", - publisher = "The Electronic Library of Mathematics (EMIS)", - url = "\url{http://www.emis.de/ELibM.html}", - year = "2001" -} - -@inproceedings{formal-proof-sketches, - author = "Freek Wiedijk", - title = "Formal Proof Sketches", - editor = "Wan Fokkink and Jaco van de Pol", - booktitle = "7th Dutch Proof Tools Day, Program + Proceedings", - note = "CWI, Amsterdam", - year = "2003", -} - -@inproceedings{Barendregt, - author = "Henk Barendregt", - title = "Towards an Interactive Mathematical Proof Language", - editor = "Fairouz Kamareddine", - booktitle = "Thirty Five Years of Automath", - pages = "25--36", - publisher = "Kluwer", - year = "2003", -} - -@inproceedings{werner:prof-irrelevance, - 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}", - pages = "240--258", - volume = "LNCS, 2646", - publisher = "Springer-Verlag", - year = "2003", -} - -@inproceedings{csc-environment, - 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", - volume = "LNCS, 3119", - pages = "332--346", - publisher = "Springer-Verlag", - year = "2004" -} - -@inproceedings{disambiguation, - 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", - volume = "LNCS, 3119", - pages = "347--362", - publisher = "Springer-Verlag", - year = "2004" -} - -@inproceedings{pechino, - author = "Andrea Asperti and Bernd Wegner", - title = "An Approach to Machine-Understandable Representation of the Mathematical Information in Digital Documents", - editor = "Fengshai Bai and Bernd Wegner", - booktitle = "Electronic Information and Communication in Mathematics", - volume = "LNCS, 2730", - pages = "14--23", - publisher = "Springer-Verlag", - year = "2003" -} - -@inproceedings{whelp, - 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, 3839", - pages = "17--32", - publisher = "Springer-Verlag", - year = "2004" -} - -@inproceedings{exportation-module, - 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", - booktitle = "Proceedings of the Second International Conference on - Mathematical Knowledge Management, MKM 2003", - pages = "30--44", - volume = "LNCS, 2594", - publisher = "Springer-Verlag", - year = "2003", -} - -@inproceedings{ida, - 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", - pages = "XXX--XXX", - volume = "LNCS, (to appear)", - publisher = "Springer-Verlag", - year = "2005", -} - -@inproceedings{davenport, - author = "James H. Davenport", - title = "{MKM} from Book to Computer: A Case Study", - editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport", - booktitle = "Proceedings of the Second International Conference on - Mathematical Knowledge Management, MKM 2003", - pages = "17--29", - volume = "LNCS, 2594", - publisher = "Springer-Verlag", - year = "2003", -} - -@inproceedings{fguidisacerdot, - author = "Ferruccio Guidi and Claudio {Sacerdoti Coen}", - title = "Querying Distributed Digital Libraries of Mathematics", - editor = "Therese Hardin and Renaud Rioboo", - booktitle = "Calculemus 2003", - pages = "17--30", - publisher = "Aracne Editrice S.R.L.", - year = "2003", - note = "ISBN 88-7999-545-6" -} - -@inproceedings{hbugs, - 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", - pages = "43--57", - publisher = "Aracne Editrice S.R.L.", - year = "2003", - note = "ISBN 88-7999-545-6" -} - -@inproceedings{calculemus-presentation, - author = "Christoph Benzm{\"u}ller", - title = "The {CALCULEMUS} Research Training Network -- A short Overview", - editor = "Therese Hardin and Renaud Rioboo", - booktitle = "Calculemus 2003", - pages = "1--16", - publisher = "Aracne Editrice S.R.L.", - year = "2003", - note = "ISBN 88-7999-545-6" -} - -@inproceedings{linda, - 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", - booktitle = "Theoretical Computer Science: 8th Italian Conference, ICTCS 2003", - pages = "37--57", - volume = "LNCS, 2841", - publisher = "Springer-Verlag", - year = "2003", -} - -@article{asperti-categorical-understanding, - author = "Andrea Asperti", - title = "A categorical understanding of environment machines", - journal = "Journal of Functional Programming", - volume = "2", - number = "1", - pages = "23--59", - month = jan, - year = "1992" -} - -@article{namelessdummies, - author = "{N. G. de Bruijn}", - title = "Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem", - journal = "Indagationes Mathematicae", - volume = "34", - pages = "381--392", - year = "1972" -} - -@article{ctcoq1, - author = "Yves Bertot", - title = "The CtCoq System: Design and Architecture", - journal = "Formal Aspects of Computing", - volume = "11", - pages = "225--243", - 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", - journal = "Journal of Symbolic Computation", - volume = "25", - pages = "161--194", - year = "1998" -} - -@article{mbase, - author = "Michael Kohlhase and Andreas Franke", - title = "{MBase}: Representing Knowledge and Context for the Integration of Mathematical Software Systems", - journal = "Journal of Symbolic Computation", - volume = "32", - number = "4", - pages = "365--402", - year = "2001", - url = "\url{http://citeseer.nj.nec.com/kohlhase00mbase.html}" -} - -@inproceedings{mizarql, - author = "Grzegorz Bancerek and Piotr Rudnicki", - title = "Information Retrieval in {MML}", - editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport", - booktitle = "Proceedings of the Second International Conference on - Mathematical Knowledge Management, MKM 2003", - pages = "119--132", - volume = "LNCS, 2594", - publisher = "Springer-Verlag", - year = "2003", -} - -@article{codedcontexttrees, - author = "Harald Ganzinger and Robert Nieuwehuis and Pilar Nivela", - title = "Fast Term Indexing with Coded Context Trees. Journal of Automated Reasoning", - journal = "Journal of Automated Reasoning", - year = "To appear" -} - -@article{ranta, - author = "Aarne Ranta", - title = "Grammatical Framework: A Type-Theoretical Grammar Formalism", - journal = "Journal of Functional Programming", - year = "To appear", - note = "Manuscript made available in September 2002" -} - -@book{DiCosmo, - AUTHOR = "Di Cosmo, Roberto", - TITLE = {Isomorphisms of types: from $\lambda$-calculus to information retrieval and language design}, - SERIES = {Progress in Theoretical Computer Science}, - PUBLISHER = {Birkhauser}, - YEAR = {1995}, - NOTE = {ISBN-0-8176-3763-X} -} - -@book{automath, - EDITOR = "R.P. Nederpelt and J.H. Geuvers and R.C. de Vrijer", - TITLE = {Selected Papers on Automath}, - SERIES = {Studies in Logic and the Foundations of Mathematics}, - PUBLISHER = {Elsevier Science}, - VOLUME = "133", - YEAR = {1994}, - NOTE = {ISBN-0444898220} -} - -@misc{krivine, - author = "Jean-Louis Krivine", - title = "Un interpr\`ete du $\lambda$-calcul", - howpublished = "Brouillon. Available on-line at \url{http://www.logique.jussieu.fr/~krivine}", - year = 1985 -} - -@misc{na-mkm1, - title = "Progress Report: Building Interactive Digital Libraries of Formal - Algorithmic Knowledge", - howpublished = "Cornell University, \url{http://www.cs.uwyo.edu/~nuprl/documents/cornell_slides.pdf}", - month = may, - year = 2002, - key = "Progress" -} - -@misc{metadata4education, - title = "{L}earning {O}bject {M}etadata Standard", - howpublished = "Learning Technology Standards Committee of IEEE, \verb+http://www.learninglab.de/elan/kb3/lexikon/metadaten-standards/docs/+ \verb+LOM_1484_12_1_v1_Final_Draft.pdf+", - year = 2002, - key = "Learning" -} - -@misc{openmath-cd-with-plus, - title = "Arith1 {OpenMath} {C}ontent {D}ictionary", - howpublished = "The OpenMath Society, \url{http://www.openmath.org/cocoon/openmath/cd/arith1.ocd}", - year = 2002, - key = "Arith1 OpenMath Content Dictionary" -} - - -@misc{ddc, - title = "Dewey Decimal Classification", - howpublished = "\url{http://www.oclc.org/dewey}", - url = "\url{http://www.oclc.org/dewey}", - key = "Dewey" -} - -@misc{lc, - title = "Library of Congress Classification Scheme", - howpublished = "\url{http://www.loc.gov}", - url = "\url{http://www.loc.gov}", - key = "Library" -} - -@misc{msc, - title = "Mathematical {S}ubject {C}lassification, {A}merican {M}athematical {S}ociety", - howpublished = "\url{http://www.ams.org/msc}", - url = "\url{http://www.ams.org/msc}", - key = "Mathematical" -} - -@InCollection{borges, - author = "Jorge Luis Borges", - title = "The Library of {B}abel", - publisher = "Grove Press", - booktitle = "Ficciones", - year = 1942 -} - -@inproceedings{magaud, - author = "Nicolas Magaud", - title = "{C}hanging {D}ata {R}epresentation within the {C}oq {S}ystem", - booktitle = {TPHOLs'2003}, - publisher = {Springer-Verlag}, - volume = {LNCS, 2758}, - year = {2003}, -} - -@inproceedings{geuvers-jojgov, - author = "Herman Geuvers and Gueorgui I. Jojgov", - title = "Open Proofs and Open Terms: A Basis for Interactive Logic", - editor = "J. Bradfield", - booktitle = "Computer Science Logic: 16th International Workshop, CLS 2002", - pages = "537-552", - volume = "LNCS, 2471", - publisher = "Springer-Verlag", - month = jan, - year = "2002" -} - -@inproceedings{mkm-structure, - author = "Koji Nakagawa and Akihiro Nomura and Masakazu Suzuki", - title = "Extraction of Logical Structure from articles in Mathematics", - editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec", - booktitle = "Proceedings of Mathematical Knowledge Management 2004", - volume = "LNCS, 3119", - pages = "276--289", - publisher = "Springer-Verlag", - year = "2004" -} - -@inproceedings{mkm-metadata2, - author = "Andrea Asperti and Matteo Selmi", - title = "Efficient Retrieval of Mathematical Statements", - editor = "Andrea Asperti, Grzegorz Bancerek, Andrzej Trybulec", - booktitle = "Proceedings of Mathematical Knowledge Management 2004", - volume = "LNCS, 3119", - pages = "17--31", - publisher = "Springer-Verlag", - year = "2004" -} - -@inproceedings{adams, - author = "A. A. Adams", - title = "Digitisation, Representation and Formalisation: Digital - Libraries of Mathematics.", - editor = "A. Asperti, B. Buchberger, J.H. Davenport", - booktitle = "Proceedings of Mathematical Knowledge Management 2003", - volume = "LNCS, 2594", - pages = "1--16", - publisher = "Springer-Verlag", - year = "2003" -} - -@inproceedings{maya, - author = "Serge Autexier and Dieter Hutter and Heiko Mantel and Axel Schairer", - title = "Towards an Evolutionary Formal Software-Development Using {CASL}", - booktitle = "WADT99 Selected Papers Volume", - volume = "LNCS, 1827", - publisher = "Springer-Verlag", - year = "2000" -} - -@inproceedings{how-to-extract, - author = "Lu\'is Cruz Filipe and Bas Spitters", - title = "Program Extraction from large proof developments", - booktitle = "Proceedings of TPHOLS 2003", - editor = "D. Basin and B. Wolff", - volume = "LNCS, 2758", - publisher = "Springer-Verlag", - year = "2003" -} - -@inproceedings{click-and-prove, - author = "Jean-Raymond Abrial and Dominique Cansell", - title = "Click'n {P}rove: Interactive Proofs Within Set Theory", - booktitle = "Proceedings of TPHOLS 2003", - editor = "D. Basin and B. Wolff", - volume = "LNCS, 2758", - publisher = "Springer-Verlag", - year = "2003" -} - -@inproceedings{delahaye, - author = "David Delahaye and Roberto di Cosmo", - title = "Information Retrieval in a {C}oq Proof Library using - Type Isomorphisms", - booktitle = "Proceedings of TYPES 99", - volume = "LNCS", - publisher = "Springer-Verlag", - year = "1999" -} - -@TechReport{jojgov, - author = "G. I. Jojgov", - title = "Systems for open terms: An Overview", - institution = "Technische Universiteit Eindhoven", - number = "CSR 01-03", - year = "2001" -} - -@TechReport{garrigue:implicit-arguments, - author = "Jun P. Furuse and Jacques Garrigue", - title = " A label-selective lambda-calculus with optional arguments and its compilation method", - institution = "Research Institute for Mathematical Sciences, Kyoto University", - number = "RIMS Preprint 1041", - month = oct, - year = "1995" -} - -@phdthesis{miquel, - author = "Alexandre Miquel", - title = "Le {C}alcul des {C}onstructions {I}mplicite: syntaxe et s\'emantique", - school = "Universit\'e Paris 7", - year = "2001" -} - -@phdthesis{chrzaszcz, - author = "Jacek Chrz{\c{a}}szcs", - title = "Modules in Type Theory with Generative Definitions", - school = "Uniwersytet Warszawski and Universit\'e de Paris Sud", - year = "2003" -} - -@phdthesis{Pons, - author = "Olivier Pons", - title = "Conception et r\'ealisation d'outils d'aide au d\'eveloppement de grosse th\'eories dans les syst\`emes de preuves interactifs", - school = "Conservatoire National des Arts et M\'etiers", - year = "1999" -} - -@phdthesis{blanqui, - author = "Fr\'ed\'eric Blanqui", - title = "Type Theory and Rewriting", - school = "Universit\'e Paris XI", - year = "2001" -} - -@phdthesis{magnusson, - author = "Lena Magnusson", - title = "The Implementation of {ALF} -- a Proof Editor based - on Martin-L{\"o}f Monomorphic Type Theory with Explicit - Substitutions", - school = "Chalmers University of Technology / G{\"o}teborg University", - year = "1995" -} - -@phdthesis{McBride, - author = "Conor McBride", - title = "Dependently Typed Functional Programs and their Proofs", - school = "University of Edinburgh", - year = "1999" -} - -@phdthesis{schena, - author = "Irene Schena", - title = "Towards a Semantic Web for Formal Mathematics", - school = "University of Bologna", - year = "2002" -} - -@phdthesis{fguidi, - author = "Ferruccio Guidi", - title = "Searching and Retrieving in Content-Based Repositories - of Formal Mathematical Knowledge", - school = "University of Bologna", - month = mar, - year = "2003", - note = "Technical Report UBLCS 2003-06" -} - -@phdthesis{padovani, - author = "Luca Padovani", - title = "MathML Formatting", - school = "University of Bologna", - month = feb, - year = "2003", - note = "Technical Report UBLCS 2003-03" -} - -@mastersthesis{csc-master, - author = "Claudio {Sacerdoti Coen}", - title = "Progettazione e realizzazione con tecnologia {XML} di basi distribuite di conoscenza matematica formalizzata", - school = "University of Bologna", - year = 2000 -} - -@mastersthesis{zack-master, - author = "Stefano Zacchiroli", - title = "Web {s}ervices per il supporto alla dimostrazione interattiva", - school = "University of Bologna", - year = 2003 -} - -@mastersthesis{dilena, - author = "Pietro Dilena", - title = "Generazione automatica di stylesheet per notazione matematica", - school = "University of Bologna", - year = 2003 -} - -@phdthesis{munoz, - author = "C\'esar Munoz", - title = "A Calculus of Substitutions for Incomplete-Proof - Representation in Type Theory", - school = "INRIA", - month = nov, - year = "1997" -} - -@phdthesis{strecker, - author = "Martin Strecker", - title = "Construction and Deduction in Type Theories", - school = "Universit{\"a}t Ulm", - 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", - howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/project.html}", - key = "MoWGLI Proposal" -} - -@misc{debrujinfactor, - title = "The ``de Bruijn factor''", - howpublished = "\\\url{http://www.cs.ru.nl/~freek/factor/}", - year = {2000}, - author = "Freek Wiedijk", -} - -@misc{mowgli-deliverables, - title = "{MoWGLI} Project Deliverables", - howpublished = "\\\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/index.html}", - key = "MoWGLI Deliverables" -} - -@misc{ALF, - title = "The {ALF} family of proof-assistants", - howpublished = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}", - url = "\url{http://www.cs.chalmers.se/ComputingScience/Research/Logic/implementation.html}", - 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}", - key = "Coq" -} - -@misc{phox, - title = "The {PhoX} proof-assistant", - howpublished = "\\\url{http://www.lama.univ-savoie.fr/~RAFFALLI/phox.html}", - key = "PhoX" -} - -@misc{lego, - title = "The {L}ego proof-assistant", - howpublished = "\\\url{http://www.dcs.ed.ac.uk/home/lego/}", - key = "Lego" -} - -@misc{ALFA, - title = "The {A}lfa proof editor", - howpublished = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}", - url = "\url{http://www.math.chalmers.se/~hallgren/Alfa/}", - key = "Alfa" -} - -@misc{pvs, - title = "The {PVS} Specification and Verification System", - howpublished = "\\\url{http://pvs.csl.sri.com/}", - key = "PVS" -} - -@misc{isabelle, - title = "The {Isabelle} proof-assistant", - howpublished = "\\\url{http://www.cl.cam.ac.uk/Research/HVG/Isabelle/}", - 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}", - key = "NuPRL" -} - -@misc{hollight, - title = "The {HOL Light} proof-assistant", - howpublished = "\\\url{http://www.cl.cam.ac.uk/users/jrh/hol-light/}", - key = "HOL-Light" -} - -@misc{monet, - title = "The {MONET} project", - howpublished = "\\\url{http://monet.nag.co.uk/cocoon/monet/index.html}", - key = "Monet" -} - -@misc{calculemus, - title = "The {CALCULEMUS} project", - howpublished = "\url{http://www.calculemus.net/}", - url = "\url{http://www.calculemus.net/}", - key = "Calculemus" -} - -@misc{mizar, - title = "The {M}izar proof-assistant", - howpublished = "\\\url{http://mizar.uwb.edu.pl/}", - key = "Mizar" -} - -@misc{openmath, - howpublished = "The {O}pen{M}ath {E}sprit {C}onsortium", - author = "O. Caprotti and D. P. Carlisle and A. M. Cohen", - title = "{\emph{The {O}pen{M}ath {S}tandard}}" -} - -@misc{mathml, - 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 = "MathML" -} - -@misc{xml, - title = "{E}xtensible {M}arkup {L}anguage ({XML}). {V}ersion 1.0.", -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 = "XML" -} - -@misc{dom, - title = "Document {O}bject {M}odel ({DOM}) {L}evel 2 {S}pecification. {V}ersion 1.0", - howpublished = "W3C Candidate Recommendation 10 May 2000, - \url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}", - url = "\url{http://www.w3.org/TR/2000/CR-DOM-Level-2-20000510/}", - key = "Document" -} - -@misc{URIs, - title = "Universal Resource Identifiers in {WWW}", - howpublished = "RFC 1630, CERN", - month = jun, - year = "1994", - key = "URI" -} - -@misc{xpath, - title = " {XML} {P}ath {L}anguage ({XPath}). Version 1.0", - howpublished = "W3C Recommendation, 16 November 1999, - \url{http://www.w3.org/TR/xpath}", - url = "\url{http://www.w3.org/TR/xpath}", - key = "XML" -} - -@misc{xslt, - title = "{XSL} {T}ransformations ({XSLT}). {V}ersion 1.0", - howpublished = "W3C Recommendation, 16 November 1999, - \url{http://www.w3.org/TR/xslt}", - url = "\url{http://www.w3.org/TR/xslt}", - key = "XSLT" -} - -@misc{rdf, - title = "Resource {D}escription {F}ramework ({RDF}) Model and Syntax - Specification", - howpublished = "W3C Recommendation 22 February 1999, - \url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}", - url = "\url{http://www.w3.org/TR/1999/REC-rdf-syntax-19990222/}", - key = "Resource" -} - -@misc{omdoc, - 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" -} - -@misc{FORMAVIE, - title = "The {F}ormavie project", - howpublished = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}", - url = "\url{http://http://www-sop.inria.fr/oasis/Formavie/}", - key = "Formavie" -} - -@misc{EHELM, - title = "The {HELM} project", - howpublished = "\url{http://helm.cs.unibo.it}", - url = "\url{http://helm.cs.unibo.it}", - key = "HELM" -} - -@misc{helm-library, - title = "The {HELM} On-Line Library", - howpublished = "\url{http://helm.cs.unibo.it/library.html}", - url = "\url{http://helm.cs.unibo.it/library.html}", - key = "HELM Library" -} - -@misc{MATHWEB, - title = "The {M}ath{W}eb project", - howpublished = "\url{http://www.mathweb.org}", - url = "\url{http://www.mathweb.org}", - key = "MathWeb" -} - -@misc{PCOQ, - title = "The {PC}oq project", - howpublished = "\url{http://www-sop.inria.fr/lemme/pcoq}", - url = "\url{http://www-sop.inria.fr/lemme/pcoq}", - key = "PCoq" -} - -@TechReport{HELM, - author = "Andrea Asperti and Luca Padovani and Claudio {Sacerdoti Coen} - and Irene Schena", - title = "Towards a library of formal mathematics", - year = "2000", - note = "Panel session of the 13th {I}nternation {C}onference on - {T}heorem {P}roving in {H}igher {O}rder {L}ogics - ({TPHOLS}'2000), Portland, Oregon, USA", -} - -@inproceedings{Ring, - author = "Samuel Boutin", - title = "Using Reflection to Build Efficient and Certified Decision - Procedures", - editor = "Martin Abadi and Takahashi Ito editors", - booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS", - pages = "515-529", - volume = "1281", - publisher = "Springer-Verlag", - year = "1997", -} - -@inproceedings{werner-zfc, - author = "Benjamin Werner", - title = "Sets in Types, Types in Sets", - editor = "Martin Abadi and Takahashi Ito editors", - booktitle = "Theoretical Aspect of Computer Software {TACS'}97, LNCS", - pages = "530-546", - volume = "1281", - publisher = "Springer-Verlag", - year = "1997", -} - -@article{aczel, - author = "Peter Aczel", - title = "On Relating Type Theories and Set Theories", - journal = "Lecture Notes in Computer Science", - volume = "1657", - year = "1999", -} - -@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 = "Electronic Proceedings of {EXTREME Markup Languages} 2001", - year = "2001", -} - - -@phdthesis{YANNTHESIS, - author = "Yann Coscoy", - title = "Explication textuelle de preuves pour le {C}alcul des - {C}onstructions {I}nductives", - school = "Universit\'e de Nice-Sophia Antipolis", - year = "2000", -} - -@phdthesis{Lippi, - author = "Sylvain Lippi", - title = "Th\'eorie et pratique des r\'eseaux d'interaction (Interaction nets)", - school = "Universit\'e Aix-Marseille 2", - year = "2002" -} - -@phdthesis{Werner, - author = "Benjamin Werner", - title = "Une Th\'eorie des {C}onstructions {I}nductives", - school = "Universit\'e Paris VII", - month = may, - year = "1994", -} - -@InCollection{Felleisen87, - author = "M. Felleisen and D. Friedman", - editor = "M. Wirsing", - title = "Control operators, the {SECD}-machine, and the lambda calculus", - booktitle = "Formal Description of Programming Concepts III", - pages = "193--217", - publisher = "Elsevier Science Publishers B.V.", - address = "(North-Holland) Amsterdam", - year = "1987", -} - -@TechReport{yarrow, - author = "Jan Zwanenburg", - institution = "Eindhoven University of Technology", - number = "Computing Science Report CS-98-11", - title = "The Proof-assistant Yarrow", - year = "1998" -} - -@TechReport{Ager2003a, - author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard", - institution = "BRICS", - month = mar, - number = "BRICS RS-03-13", - title = "A Functional Correspondence between Evaluators and Abstract Machines", - year = "2003" -} - -@TechReport{Ager2003b, - author = "Mads Sig Ager and Dariusz Biernacki and Olivier Danvy and Jan Midtgaard", - institution = "BRICS", - month = mar, - number = "BRICS RS-03-14", - title = "From Interpreter to Compiler and Virtual Machine: A Functional Derivation", - year = "2003" -} - -@article{harperpollack, - author = "Robert Harper and Robert Pollack", - title = "Type checking with universes", - journal = "Theoretical Computer Science", - volume = "89", - pages = "107--136", - year = "1991" -} - -@article{activemath, - author = "Erica Melis and Jochen B{\"a}udenbender and George Goguadze and Paul Libbrecht and Carsten Ullrich", - title = "Knowledge Representation and Management in {ActiveMath}", - journal = "Annals of Mathematics and Artificial Intelligence", - volume = "38(1-3)", - pages = "47--64", - month = may, - year = "2003" -} - -@article{mkm-helm, - author = "Andrea Asperti and Ferruccio Guidi and Luca Padovani and - Claudio {Sacerdoti Coen} and Irene Schena", - title = "Mathematical Knowledge Management in {HELM}", - journal = "Annals of Mathematics and Artificial Intelligence", - volume = "38(1-3)", - pages = "27--46", - month = may, - year = "2003" -} - -@unpublished{formal-topology, - author = "Giovanni Sambin", - title = "Some points in formal topology", - note = "To appear in Theoretical Computer Science", - year = "2002" -} - -@TechReport{JohnHarrison:complexity-of-floating-point-proofs, - author = "John Harrison", - title = "Real Numbers in Real Applications", - note = "in Proceedings of the Workshop on Formalizing Continuous Mathematics, FCM 2002", - institution = "NASA", - number = "NASA/CP-2002-211736", - year = "2002" -} - -@inproceedings{kohlhase-anghelache, - author = "Michael Kohlhase and Romeo Anghelache", - title = "Towards Collaborative Content Management And Version Control For - Structured Mathematical Knowledge", - editor = "Andrea Asperti and Bruno Buchberger and James H. Davenport", - booktitle = "Proceedings of the Second International Conference on - Mathematical Knowledge Management, MKM 2003", - pages = "147--161", - volume = "LNCS, 2594", - publisher = "Springer-Verlag", - year = "2003", -} - -%%% Unused entries from my Master dissertation bibliography - -@misc{sgml, - title="{Standard Generalized Markup Language (SGML)}", - note="ISO 8879:1986", - key="ISO" - } - -@unpublished{helm1, - 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", - 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", - title = "{Towards a Library of Formal Mathematics}", - note = "Accepted at TPHOLS 2000", - ps = "http://www.cs.unibo.it/~asperti/HELM/tphol2k.ps.gz", -} - -@techreport{mowgli:D4a, - author = "Hanane Naciri and Luca Padovani", - title = "{MathML} Rendering/Browsing Engine", - type = {MoWGLI Report}, - number = {D4a}, - year = 2003, - howpublished = "\url{http://mowgli.cs.unibo.it/html_no_frames/deliverables/interfaces/d4a.html}" -} - -@techreport{hazewinkel, - author = "Michiel Hazewinkel", - title = "Dynamic stochastic models for indexes and thesauri, - identification clouds, and information retrieval and - storage", - type = "{MKM Net Report}", - howpublished = "\url{http://monet.nag.co.uk/mkm//index.html}" -} - -@techreport{BarrasB:coqpar, - author = "{Barras B.} and {Boutin S.} and {Cornes C.} - and {Courant J.} and {Filliatre J. C.} - and {Gim\'enez E.} and {Herbelin H.} and {Huet G.} - and {Munoz C.} and {Murthy C.} and {Parent C.} - and {Paulin-Mohring C.} and {Saibi A.} - and {Werner B.}", - title = "{The Coq Proof Assistant Reference Manual : Version - 6.1}", - institution = {Inria (Institut National de Recherche en Informatique - et en Automatique), France}, - type = {Technical Report}, - number = {RT-0203}, - year = 1997, - author_acronym = {WernerB}, - bibdate = {May 1, 1997}, - source = {http://www.cis.upenn.edu/~bcpierce/papers/bcp.bib/}, - source-date = {Mon 11 Sep 100}, - title_acronym = {coqpar} -} - -@unpublished{bw:1997, - author = "Bruno Barras and Benjamin Werner", - title = "{Coq in Coq}", - year = "1997", - note = "Submitted", - ps = "http://pauillac.inria.fr/~barras/coqincoq.ps.gz", -} - -@unpublished{berners-lee:1989, - author = "Tim Berners-Lee", - title = "{Information Management: A Proposal}", - year = "1989", - ps = "http://www.w3.org/History/1989/proposal.html", -} - -@techreport{natural, - author = "Yann Coscoy and Gilles Kahn and Laurent Thery", - title = "{Extracting Text from Proofs}", - institution = {Inria (Institut National de Recherche en Informatique - et en Automatique), France}, - type = {Technical Report}, - number = {RR-2459}, - year = 1995 -} - -@inproceedings{Bru80, - author = "de Bruijn, N. G.", - title = "{A survey of the project AUTOMATH}", - pages = "589--606", - editor = "J. P. Seldin and J. R. Hindley", - booktitle = "To H. B. Curry: Essays in Combinatory Logic, - Lambda Calculus and Formalism", - year = 1980, - publisher = "Academic Press" -} - -@techreport{tutrect, - author = "E Gim\'enez", - title = "{A Tutorial on Recursive Types in Coq}", - institution = {Inria (Institut National de Recherche en Informatique - et en Automatique), France}, - type = {Technical Report}, - number = {RT-0221}, - year = 1998 -} - -@inproceedings{QED, - author = "John Harrison", - title = "{The QED Manifesto}", - pages = "238--251", - booktitle = "Automated Deduction - CADE 12", - series = "Lecture Notes in Artificial Intelligence", - volume = 814, - year = 1994, - publisher = "Springer-Verlag" -} - -@inproceedings{harrison-mizar, - author = "John Harrison", - title = "{A Mizar Mode for HOL}", - pages = "203--220", - editor = "Joakim von Wright and Jim Grundy and John Harrison", - booktitle = "Theorem Proving in Higher Order Logics: - 9th International Conference, TPHOLs'96", - series = "Lecture Notes in Computer Science", - volume = 1125, - address = "Turku, Finland", - date = "26--30 August 1996", - year = 1996, - publisher = "Springer-Verlag" -} - -@inproceedings{proverb, - author="H. Horacek", - title="{Presenting Proofs in a Human Oriented Way}", - booktitle="16th International Conference on Automated Deduction", - year="1999" - } - -@misc{HuetG:coqpat, - author = "Gerard Huet and Gilles Kahn and Christine Paulin-Mohring", - title = "{The Coq Proof Assistant. A Tutorial}", - year = 1998 -} - -@PHDTHESIS{BJ94, - author="{Jutting van L. S. B.}", - school = {{Eindhoven University of Technology}}, - title="{Checking Landau's ``Grundlagen'' in the AUTOMATH System}", - type = {Ph D. thesis}, - note = "{Useful summary in Nederpelt, Geuvers and de Vrijier, 1994, 701-732}", - year = {1994} -} - -@misc{abriefhistoryoftheinternet, - author="{Leiner B. M.} and {Cerf V. G.} and {Clark D. D.} - and {Kahn R. E.} and {Kleinrock L.} and {Lynch D. C.} - and {Postel J.} and {Roberts L. G.} and {Wolff S.}", - title="{A Brief Hystory of the Internet}", - note="http://www.isoc.org/internet-history/brief.html" - } - -@inproceedings{MacKenzie:1995, - author="{MacKenzie D.}", - title="{The automation of proof: A historical and sociological exploration}", - booktitle="IEEE: Annals of the History of Computing", - year="1995" -} - -@PHDTHESIS{Moh89b, - author = "Christine Paulin-Mohring", - month = {January}, - school = {{Paris 7}}, - title = "{Extraction de programmes dans le Calcul des Constructions}", - type = {Th\`ese d'universit\'e}, - year = {1989}, - url = {http://www.lri.fr/~paulin/these.ps.gz}, -} - -@MASTERTHESIS{ri99, - author = "A. Ricci", - school = {{Universit\`a degli studi di Bologna}}, - title = "{Studio e progettazione di un modello RDF per biblioteche matematiche -elettroniche}", - type = {Tesi universitaria}, - year = {1999} -} - -@inproceedings{Rob65, - author="{Robinson J. A.}", - title = "{A machine-oriented logic based on the resolution principle}", - pages = "23--41", - booktitle = "Journal of the ACM", - volume = "2", - year ="1965" -} - -@inproceedings{sh:1995, - author="{Saibi A.} and {Huet G.}", - title="{Constructive Category Theory}", - booktitle="Proceedings of the joint CLICS-TYPES Workshop on Categories and Type Theory", - address="Goteborg (Sweden)", - month="January", - year="1995" - } - -@inproceedings{ranta2, - author="Thomas Hallgren and Aarne Ranta", - title="An extensible proof text editor", - BOOKTITLE = {LPAR'2000}, - SERIES = {LNCS/LNAI}, - VOLUME = 1955, - YEAR = 2000 - } - -@inproceedings{werner:1997, - author="Benjamin Werner", - title="{Constructive Category Theory}", - booktitle="Proocedings of the International Symposium on Theoretical Aspects of Computer Software", - 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" } -