@(Alignments-public:on,
 title        = {Public Repository for Alignments},
 url          = {https://gl.mathhub.info/alignments/Public},
)
@inproceedings(dedukti,
 author       = {M. Boespflug and Q. Carbonneaux and O. Hermant},
 year         = {2012},
 title        = {The {$\lambda\Pi $}-calculus modulo as a universal proof language},
 editor       = {D. Pichardie and T. Weber},
 booktitle    = {Proceedings of PxTP2012: Proof Exchange for Theorem Proving},
 pages        = {28--43},
)
@inproceedings(CarFarKoh:rsckmt14,
 author       = {Jacques Carette and William Farmer and Michael Kohlhase},
 year         = {2014},
 title        = {Realms: A Structure for Consolidating Knowledge about Mathematical Theories},
 editor       = {Watt},
 pages        = {252--266},
 doi          = {10.1007/978-3-319-08434-3},
 url          = {http://kwarc.info/kohlhase/papers/cicm14-realms.pdf},
 note         = {MKM Best-Paper-Award},
)
@inproceedings(CodHorKoh:palai11,
 author       = {Mihai Codescu and Fulya Horozal and Michael Kohlhase and Till Mossakowski and Florian Rabe},
 year         = {2011},
 title        = {Project Abstract: Logic Atlas and Integrator ({LATIN})},
 editor       = {Davenport},
 pages        = {289--291},
 doi          = {10.1007/978-3-642-22673-1},
 url          = {https://kwarc.info/people/frabe/Research/CHKMR_latinabs_11.pdf},
)
@proceedings(CICM17,
 year         = {2017},
 title        = {Intelligent Computer Mathematics},
 series       = {LNAI},
 publisher    = {Springer},
 note         = {In press},
)
@proceedings(CICM11,
 editor       = {James Davenport and William Farmer and Florian Rabe and Josef Urban},
 year         = {2011},
 title        = {Intelligent Computer Mathematics},
 series       = {LNAI},
 volume       = {6824},
 publisher    = {Springer Verlag},
 doi          = {10.1007/978-3-642-22673-1},
)
@inproceedings(DehKohKon:iop16,
 author       = {Paul-Olivier Dehaye and Mihnea Iancu and Michael Kohlhase and Alexander Konovalov and Samuel Leli{\`e}vre and Dennis M{\"u}ller and Markus Pfeiffer and Florian Rabe and Nicolas M. Thi{\'e}ry and Tom Wiesing},
 year         = {2016},
 title        = {Interoperability in the {OpenDreamKit} Project: The Math-in-the-Middle Approach},
 editor       = {Michael Kohlhase and Moa Johansson and Bruce Miller and Leonardo de Moura and Frank Tompa},
 booktitle    = {{Intelligent Computer Mathematics} 2016},
 series       = {LNAI},
 volume       = {9791},
 publisher    = {Springer},
 doi          = {10.1007/978-3-642-39320-4},
 url          = {https://github.com/OpenDreamKit/OpenDreamKit/blob/master/WP6/CICM2016/published.pdf},
)
@article(FaGu93,
 author       = {William M. Farmer and Joshua D. Guttman and F. Javier Thayer},
 year         = {1993},
 title        = {{IMPS}: An {Interactive} {Mathematical} {Proof} {System}},
 journal      = {Journal of Automated Reasoning},
 volume       = {11},
 number       = {2},
 pages        = {213--248},
 doi          = {10.1007/BF00881906},
)
@inproceedings(tgck-cicm14,
 author       = {Thibault Gauthier and Cezary Kaliszyk},
 year         = {2014},
 title        = {Matching concepts across {HOL} libraries},
 editor       = {Stephen Watt and James Davenport and Alan Sexton and Petr Sojka and Josef Urban},
 booktitle    = {CICM},
 series       = {LNCS},
 volume       = {8543},
 publisher    = {Springer Verlag},
 pages        = {267--281},
 doi          = {10.1007/978-3-319-08434-3_20},
)
@techreport(IanKohRab:tmmlof11,
 author       = {Mihnea Iancu and Michael Kohlhase and Florian Rabe},
 year         = {2011},
 title        = {Translating the {Mizar Mathematical Library} into {OMDoc} format},
 type         = {{KWARC} Report},
 institution  = {Jacobs University Bremen},
 url          = {http://uniformal.github.io/doc/applications/LATIN/docs/Mizar2OMDoc-Report.pdf},
)
@unpublished(KalKohMue:alfms16,
 author       = {Cezary Kaliszyk and Michael Kohlhase and Dennis M{\"u}ller and Florian Rabe},
 year         = {2016},
 title        = {Aligning the Libraries of Formal Mathematical Systems},
 url          = {http://kwarc.info/kohlhase/submit/alignments16.pdf},
 note         = {Submitted to CPP 2016},
)
@inproceedings(KohKopMue:mmrdftg17,
 author       = {Michael Kohlhase and Thomas Koprucki and Dennis M{\"u}ller and Karsten Tabelow},
 year         = {2017},
 title        = {Mathematical models as research data via flexiformal theory graphs},
 booktitle    = {{Intelligent Computer Mathematics} (CICM) 2017},
 doi          = {10.1007/978-3-319-42432-3_53},
 url          = {http://kwarc.info/kohlhase/papers/cicm17-models.pdf},
 note         = {In press},
)
@inproceedings(KohMueOwr:mpagsiuf17,
 author       = {Michael Kohlhase and Dennis M{\"u}ller and Sam Owre and Florian Rabe},
 year         = {2017},
 title        = {Making {PVS} Accessible to Generic Services by Interpretation in a Universal Format},
 doi          = {10.1007/978-3-319-08434-3},
 url          = {http://kwarc.info/kohlhase/submit/itp17-pvs.pdf},
 note         = {Accepted at ITP 2017},
)
@book(Kohlhase:OMDoc1.2,
 author       = {Michael Kohlhase},
 year         = {2006},
 title        = {{OMDoc} -- An open markup format for mathematical documents [Version 1.2]},
 series       = {LNAI},
 volume       = {4180},
 publisher    = {Springer Verlag},
 doi          = {10.1007/11826095},
 url          = {http://omdoc.org/pubs/omdoc1.2.pdf},
)
@inproceedings(KalRab:hollight:14,
 author       = {Cezary Kaliszyk and Florian Rabe},
 year         = {2014},
 title        = {Towards Knowledge Management for {HOL Light}},
 editor       = {Watt},
 pages        = {357--372},
 doi          = {10.1007/978-3-319-08434-3_26},
 url          = {http://kwarc.info/frabe/Research/KR_hollight_14.pdf},
)
@article(KohRab:qrtpflmk15,
 author       = {Michael Kohlhase and Florian Rabe},
 year         = {2016},
 title        = {{QED} Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge},
 journal      = {Journal of Formalized Reasoning},
 volume       = {9},
 number       = {1},
 pages        = {201--234},
 doi          = {10.6092/issn.1972-5787/4570},
 url          = {http://jfr.unibo.it/article/download/4570/5733},
)
@inproceedings(KohRabSac:fvip11,
 author       = {Michael Kohlhase and Florian Rabe and Sacerdoti Coen, Claudio},
 year         = {2011},
 title        = {A Foundational View on Integration Problems},
 editor       = {Davenport},
 pages        = {107--122},
 doi          = {10.1007/978-3-642-22673-1},
 url          = {http://kwarc.info/kohlhase/papers/cicm11-integration.pdf},
)
@(LATIN:git,
 title        = {The LATIN Logic Atlas},
 url          = {https://gl.mathhub.info/MMT/LATIN},
)
@(MathHub:on,
 title        = {MathHub.info: Active Mathematics},
 url          = {http://mathhub.info},
)
@(MetaMath:on,
 title        = {Metamath Home page},
 url          = {http://us.metamath.org},
)
@inproceedings(MueGauKal:cacfms17,
 author       = {Dennis M{\"u}ller and Thibault Gauthier and Cezary Kaliszyk and Michael Kohlhase and Florian Rabe},
 year         = {2017},
 title        = {Classification of Alignments between Concepts of Formal Mathematical Systems},
 booktitle    = {{Intelligent Computer Mathematics} (CICM) 2017},
 doi          = {10.1007/978-3-540-71067-7_7},
 url          = {http://kwarc.info/kohlhase/submit/cicm17-alignments.pdf},
 note         = {In press},
)
@(MitM:on,
 title        = {MitM: The Math-in-the-Middle Ontology},
 url          = {https://mathhub.info/MitM},
)
@(MitMFoundation:on,
 title        = {MitM/Foundation},
 url          = {https://gl.mathhub.info/MitM/Foundation},
)
@(MitMInter:on,
 title        = {MitM/Interfaces},
 url          = {https://gl.mathhub.info/MitM/interfaces},
)
@(MitMsmglom:on,
 title        = {MitM/smglom},
 url          = {https://gl.mathhub.info/MitM/smglom},
)
@unpublished(KohMue:cicm15,
 author       = {Dennis M{\"u}ller and Michael Kohlhase},
 year         = {2015},
 title        = {Understanding Mathematical Theory Formation via Theory Intersections in {MMT}},
 url          = {http://cicm-conference.org/2015/fm4m/FMM_2015_paper_2.pdf},
)
@(OAF:on,
 title        = {The OAF Project \& System},
 url          = {http://oaf.mathhub.info},
)
@misc(ODKproposal:on,
 title        = {Open Digital Research Environment Toolkit for the Advancement of Mathematics},
 url          = {https://github.com/OpenDreamKit/OpenDreamKit/raw/master/Proposal/proposal-www.pdf},
)
@(OpenDreamKit:on,
 title        = {OpenDreamKit Open Digital Research Environment Toolkit for the Advancement of Mathematics},
 url          = {http://opendreamkit.org},
)
@inproceedings(OwRu92,
 author       = {S. Owre and J. M. Rushby and N. Shankar},
 year         = {1992},
 title        = {{PVS:} A Prototype Verification System},
 editor       = {D. Kapur},
 booktitle    = {Proceedings of the 11\textsuperscript{th} Conference on Automated Deduction},
 series       = {LNCS},
 volume       = {607},
 publisher    = {Springer Verlag},
 address      = {Saratoga Springs, NY, USA},
 pages        = {748--752},
 doi          = {10.1007/3-540-55602-8},
)
@inbook(Obua2006,
 author       = {Steven Obua and Sebastian Skalberg},
 year         = {2006},
 title        = {Importing HOL into Isabelle/HOL},
 pages        = {298--302},
 publisher    = {Springer Berlin Heidelberg},
 address      = {Berlin, Heidelberg},
 doi          = {10.1007/11814771_27},
)
@inproceedings(Rabe:qlfml12,
 author       = {Florian Rabe},
 year         = {2012},
 title        = {{A Query Language for Formal Mathematical Libraries}},
 editor       = {Johan Jeuring and John A. Campbell and Jacques Carette and Dos Reis, Gabriel and Petr Sojka and Makarius Wenzel and Volker Sorge},
 booktitle    = {{Intelligent Computer Mathematics}},
 series       = {LNAI},
 volume       = {7362},
 publisher    = {Springer Verlag},
 pages        = {142--157},
 doi          = {10.1007/978-3-642-31374-5_10},
)
@article(rabe:howto:14,
 author       = {Florian Rabe},
 year         = {2014},
 title        = {{How to Identify, Translate, and Combine Logics?}},
 journal      = {Journal of Logic and Computation},
 doi          = {10.1093/logcom/exu079},
)
@article(RabKoh:WSMSML13,
 author       = {Florian Rabe and Michael Kohlhase},
 year         = {2013},
 title        = {A Scalable Module System},
 journal      = {Information \& Computation},
 volume       = {0},
 number       = {230},
 pages        = {1--54},
 url          = {http://kwarc.info/frabe/Research/mmt.pdf},
)
@inproceedings(mizar,
 author       = {A. Trybulec and H. Blair},
 year         = {1985},
 title        = {{Computer Assisted Reasoning with MIZAR}},
 editor       = {A. Joshi},
 booktitle    = {Proceedings of the 9th International Joint Conference on Artificial Intelligence},
 publisher    = {Morgan Kaufmann},
 pages        = {26--28},
)
@proceedings(CICM14,
 editor       = {Stephan Watt and James Davenport and Alan Sexton and Petr Sojka and Josef Urban},
 year         = {2014},
 title        = {Intelligent Computer Mathematics},
 series       = {LNCS},
 volume       = {8543},
 publisher    = {Springer},
 doi          = {10.1007/978-3-319-08434-3},
)