+++ /dev/null
-
-@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" }
-
projects / helm.git / blobdiff