@inproceedings(largeformalwikis,
 author       = "J. Alama and K. Brink and L. Mamane and J. Urban",
 year         = "2011",
 title        = "Large Formal Wikis: Issues and Solutions",
 editor       = "J. Davenport and W. Farmer and J. Urban and F. Rabe",
 booktitle    = "Intelligent Computer Mathematics",
 publisher    = "Springer",
 pages        = "133--148",
 doi          = "10.1007/978-3-642-22673-1\_10",
)
@inproceedings(dependencyrelations,
 author       = "J. Alama and L. Mamane and J. Urban",
 year         = "2012",
 title        = "{Dependencies in Formal Mathematics: Applications and Extraction for Coq and Mizar}",
 editor       = "J. Jeuring and J. Campbell and J. Carette and G. Dos Reis and P. Sojka and M. Wenzel and V. Sorge",
 booktitle    = "Intelligent Computer Mathematics",
 publisher    = "Springer",
 pages        = "1--16",
 doi          = "10.1007/978-3-642-31374-5\_1",
)
@inproceedings(proof_general,
 author       = "D. Aspinall",
 year         = "2000",
 title        = "{Proof General: {A} Generic Tool for Proof Development}",
 editor       = "S. Graf and M. Schwartzbach",
 booktitle    = "Tools and Algorithms for Construction and Analysis of Systems",
 publisher    = "Springer",
 pages        = "38--42",
 doi          = "10.1007/3-540-46419-0\_3",
)
@inproceedings(l4verified_mkm,
 author       = "T. Bourke and M. Daum and G. Klein and R. Kolanski",
 year         = "2012",
 title        = "{Challenges and Experiences in Managing Large-Scale Proofs}",
 editor       = "J. Jeuring and J. Campbell and J. Carette and G. Dos Reis and P. Sojka and M. Wenzel and V. Sorge",
 booktitle    = "Intelligent Computer Mathematics",
 publisher    = "Springer",
 pages        = "32--48",
 doi          = "10.1007/978-3-642-31374-5\_3",
)
@techreport(coq,
 author       = "{Coq Development Team}",
 year         = "2014",
 title        = "{The Coq Proof Assistant: Reference Manual}",
 type         = "Technical Report",
 institution  = "INRIA",
)
@inproceedings(acl2sedan,
 author       = "P. Dillinger and P. Manolios and D. Vroon and J. Strother Moore",
 year         = "2007",
 title        = "{ACL2s: The ACL2 Sedan}",
 editor       = "S. Autexier and C. Benzm{\"u}ller",
 booktitle    = "Proceedings of the 7th Workshop on User Interfaces for Theorem Provers (UITP 2006)",
 pages        = "3--18",
)
@misc(eclipse,
 title        = "{Eclipse IDE}",
 howpublished = "\url {http://www.eclipse.org/}",
)
@inproceedings(oddorder,
 author       = "G. Gonthier and A. Asperti and J. Avigad and Y. Bertot and C. Cohen and F. Garillot and S. Le Roux and A. Mahboubi and R. O'Connor and S. Ould Biha and I. Pasca and L. Rideau and A. Solovyev and E. Tassi and L. Th{\'e}ry",
 year         = "2013",
 title        = "{A Machine-Checked Proof of the Odd Order Theorem}",
 editor       = "S. Blazy and C. Paulin-Mohring and D. Pichardie",
 booktitle    = "Interactive Theorem Proving",
 pages        = "163--179",
 doi          = "10.1007/978-3-642-39634-2\_14",
)
@article(lf,
 author       = "R. Harper and F. Honsell and G. Plotkin",
 year         = "1993",
 title        = "{A framework for defining logics}",
 journal      = "{Journal of the Association for Computing Machinery}",
 volume       = "40",
 number       = "1",
 pages        = "143--184",
 doi          = "10.1145/138027.138060",
)
@inproceedings(hollight,
 author       = "J. Harrison",
 year         = "1996",
 title        = "{HOL Light: A Tutorial Introduction}",
 booktitle    = "{Proceedings of the First International Conference on Formal Methods in Computer-Aided Design}",
 publisher    = "Springer",
 pages        = "265--269",
 doi          = "10.1007/BFb0031814",
)
@inproceedings(HIJKR:dimensions:11,
 author       = "F. Horozal and A. Iacob and C. Jucovschi and M. Kohlhase and F. Rabe",
 year         = "2011",
 title        = "{Combining Source, Content, Presentation, Narration, and Relational Representation}",
 editor       = "J. Davenport and W. Farmer and F. Rabe and J. Urban",
 booktitle    = "Intelligent Computer Mathematics",
 publisher    = "Springer",
 pages        = "212--227",
 doi          = "10.1007/978-3-642-22673-1\_15",
)
@inproceedings(HKR:extending:12,
 author       = "F. Horozal and M. Kohlhase and F. Rabe",
 year         = "2012",
 title        = "{Extending MKM Formats at the Statement Level}",
 editor       = "J. Campbell and J. Carette and G. {Dos Reis} and J. Jeuring and P. Sojka and V. Sorge and M. Wenzel",
 booktitle    = "Intelligent Computer Mathematics",
 publisher    = "Springer",
 pages        = "64--79",
 doi          = "10.1007/978-3-642-31374-5\_5",
)
@article(IKRU:mizar:11,
 author       = "M. Iancu and M. Kohlhase and F. Rabe and J. Urban",
 year         = "2013",
 title        = "{The Mizar Mathematical Library in OMDoc: Translation and Applications}",
 journal      = "Journal of Automated Reasoning",
 volume       = "50",
 number       = "2",
 pages        = "191--202",
 doi          = "10.1007/s10817-012-9271-4",
)
@inproceedings(IR:ui:12,
 author       = "M. Iancu and F. Rabe",
 year         = "2012",
 title        = "{(Work-in-Progress) An MMT-Based User-Interface}",
 editor       = "C. Kaliszyk and C. L{\"u}th",
 booktitle    = "Workshop on User Interfaces for Theorem Provers",
)
@misc(jedit,
 title        = "{jEdit: Programmer's Text Editor}",
 howpublished = "\url {http://www.jedit.org/}",
)
@inproceedings(proofweb,
 author       = "C. Kaliszyk",
 year         = "2007",
 title        = "{Web Interfaces for Proof Assistants}",
 booktitle    = "User Interfaces for Theorem Provers",
 pages        = "49--61",
)
@inproceedings(hollight_hints,
 author       = "C. Kaliszyk and J. Urban",
 year         = "2013",
 title        = "{Automated Reasoning Service for HOL Light}",
 editor       = "J. Carette and D. Aspinall and C. Lange and P. Sojka and W. Windsteiger",
 booktitle    = "Intelligent Computer Mathematics",
 publisher    = "Springer",
 pages        = "120--135",
 doi          = "10.1007/978-3-642-39320-4\_8",
)
@book(omdoc,
 author       = "M. Kohlhase",
 year         = "2006",
 title        = "{OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2)}",
 series       = "{Lecture Notes in Artificial Intelligence}",
 volume       = "4180",
 publisher    = "Springer",
)
@inproceedings(mathwebsearch,
 author       = "M. Kohlhase and I. {\c {S}}ucan",
 year         = "2006",
 title        = "{A Search Engine for Mathematical Formulae}",
 editor       = "T. Ida and J. Calmet and D. Wang",
 booktitle    = "{Artificial Intelligence and Symbolic Computation}",
 publisher    = "Springer",
 pages        = "241--253",
 doi          = "10.1007/11856290\_21",
)
@misc(agda,
 author       = "U. Norell",
 year         = "2005",
 title        = "{The Agda WiKi}",
 note         = "\url {http://wiki.portal.chalmers.se/agda}",
)
@book(isabelle,
 author       = "L. Paulson",
 year         = "1994",
 title        = "{Isabelle: A Generic Theorem Prover}",
 series       = "Lecture Notes in Computer Science",
 volume       = "828",
 publisher    = "Springer",
 doi          = "10.1007/BFb0030561",
)
@article(twelf,
 author       = "F. Pfenning and C. Sch{\"u}rmann",
 year         = "1999",
 title        = "System Description: {Twelf} - A Meta-Logical Framework for Deductive Systems",
 journal      = "Lecture Notes in Computer Science",
 volume       = "1632",
 pages        = "202--206",
 doi          = "10.1007/3-540-48660-7\_14",
)
@inproceedings(rabe:querying:12,
 author       = "F. Rabe",
 year         = "2012",
 title        = "{A Query Language for Formal Mathematical Libraries}",
 editor       = "J. Campbell and J. Carette and G. {Dos Reis} and J. Jeuring and P. Sojka and V. Sorge and M. Wenzel",
 booktitle    = "Intelligent Computer Mathematics",
 publisher    = "Springer",
 pages        = "142--157",
 doi          = "10.1007/978-3-642-31374-5\_10",
)
@inproceedings(rabe:mmtabs:13,
 author       = "F. Rabe",
 year         = "2013",
 title        = "{The MMT API: A Generic MKM System}",
 editor       = "J. Carette and D. Aspinall and C. Lange and P. Sojka and W. Windsteiger",
 booktitle    = "Intelligent Computer Mathematics",
 publisher    = "Springer",
 pages        = "339--343",
 doi          = "10.1007/978-3-642-39320-4\_25",
)
@unpublished(rabe:mmttypetheory:14,
 author       = "F. Rabe",
 year         = "2014",
 title        = "{A Generic Type Theory}",
 note         = "See \url {http://kwarc.info/frabe/Research/rabe_mmttypetheory_14.pdf}",
)
@article(RK:mmt:10,
 author       = "F. Rabe and M. Kohlhase",
 year         = "2013",
 title        = "{A Scalable Module System}",
 journal      = "Information and Computation",
 volume       = "230",
 number       = "1",
 pages        = "1--54",
 doi          = "10.1016/j.ic.2013.06.001",
)
@inproceedings(isabelle_jedit,
 author       = "M. Wenzel",
 year         = "2012",
 title        = "{Isabelle/jEdit - {A} Prover {IDE} within the {PIDE} Framework}",
 editor       = "J. Jeuring and J. Campbell and J. Carette and G. Dos Reis and P. Sojka and M. Wenzel and V. Sorge",
 booktitle    = "Intelligent Computer Mathematics",
 pages        = "468--471",
 doi          = "10.1007/978-3-642-31374-5\_38",
)