@online{wikipedia:matroid,
  label = {MWP},
  title = {Matroid --- Wikipedia{,} The Free Encyclopedia},
  urldate = {2018-04-4},
  url = {https://en.wikipedia.org/w/index.php?title=Matroid}}
@Article{imps,
  author =	"W. Farmer and J. Guttman and F. Thayer",
  title =	"{IMPS: An Interactive Mathematical Proof System}",
  journal =	"{Journal of Automated Reasoning}",
  pages =	"213--248",
  volume =	"11",
  number =	"2",
  year = 	"1993",
}
@Book{isabelle,
  author =	"L. Paulson",
  title =	"{Isabelle: A Generic Theorem Prover}",
  publisher =	"Springer",
  series =	"Lecture Notes in Computer Science",
  volume =	"828",
  year = 	"1994",
}
@INPROCEEDINGS{NorKoh:efnrsmk07,
  author = {Immanuel Normann and Michael Kohlhase},
  title = {Extended Formula Normalization for $\epsilon$-Retrieval and
           Sharing of Mathematical Knowledge},
  pages = {266--279},
  crossref = {MKM07},
  keywords = {conference},
 pubs = {mkohlhase,mws,omdoc}}
@inproceedings{KMOR:pvs:17,
  author = "M. Kohlhase and D. M{\"u}ller and S. Owre and F. Rabe",
  title = "{Making PVS Accessible to Generic Services by Interpretation in a Universal Format}",
  year = "2017",
  pages = "319--335",
  booktitle = "Interactive Theorem Proving",
  editor = "M. Ayala-Rincon and C. Munoz",
  publisher = "Springer"
}
@inproceedings{hol_isahol_matching,
  author = {T. Gauthier and C. Kaliszyk},
  title = "{Matching concepts across HOL libraries}",
  booktitle = {Intelligent Computer Mathematics},
  editor = {S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban},
  pages = {267--281},
  year = 2014,
  publisher = {Springer}
}
@online{OAFproject:on,
  label = {OAF},
  url = {https://kwarc.info/projects/oaf/},
  title = {{OAF}: An Open Archive for Formalizations},
  urldate = {2018-04-26}}
@Article{lf,
  author = 	 "R. Harper and F. Honsell and G. Plotkin",
  title = 	 "{A framework for defining logics}",
  journal =	 "{Journal of the Association for Computing Machinery}",
  year =	 1993,
  volume =	 40,
  number = 	1,
  pages =	 "143--184",
}
@inproceedings{KKMR:alignments:16,
  author = "C. Kaliszyk and M. Kohlhase and D. M{\"u}ller and F. Rabe",
  title = "{A Standard for Aligning Mathematical Concepts}",
  year = "2016",
  pages = "229--244",
  booktitle = "Work in Progress at CICM 2016",
  editor = "A. Kohlhase and M. Kohlhase and P. Libbrecht and B. Miller and F. Tompa and A. Naummowicz and W. Neuper and P. Quaresma and M. Suda",
  publisher = "CEUR-WS.org"
}
@inproceedings{ODK:mitm:16,
  author = "P. Dehaye and M. Iancu and M. Kohlhase and A. Konovalov and S. Leli{\`e}vre and D. M{\"u}ller and M. Pfeiffer and F. Rabe and N. Thi{\'e}ry and T. Wiesing",
  title = "{Interoperability in the ODK Project: The Math-in-the-Middle Approach}",
  year = "2016",
  pages = "117--131",
  booktitle = "Intelligent Computer Mathematics",
  editor = "M. Kohlhase and L. {de Moura} and M. Johansson and B. Miller and F. Tompa",
  publisher = "Springer"
}
@inproceedings{MRLR:alignments:17,
  author = "D. M{\"u}ller and C. Rothgang and Y. Liu and F. Rabe",
  title = "{Alignment-based Translations Across Formal Systems Using Interface Theories}",
  year = "2017",
  pages = "77--93",
  booktitle = "Proof eXchange for Theorem Proving",
  editor = "C. Dubois and B. {Woltzenlogel Paleo}",
  publisher = "Open Publishing Association"
}
@INPROCEEDINGS{mathhub,
  author = "M. Iancu and C. Jucovschi and M. Kohlhase and T. Wiesing",
  title = "{System Description: MathHub.info}",
  booktitle = "Intelligent Computer Mathematics",
  editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban",
  pages = "431--434",
  publisher = "Springer",
  year = {2014},
}
@inproceedings{RupKohMue:fitgv17,
  author = {Marcel Rupprecht and Michael Kohlhase and Dennis M{\"u}ller},
  title = {A Flexible, Interactive Theory-Graph Viewer},
  crossref = {MathUI17},
  url = {http://kwarc.info/kohlhase/papers/mathui17-tgview.pdf},
  pubs = {dmueller,mkohlhase,mrupprecht,odk,mathhub,odkWP6}}

@book{omdoc,
  author = "M. Kohlhase",
  title = "{OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2)}",
  series = "{Lecture Notes in Artificial Intelligence}",
  number = "4180",
  publisher = "Springer",
  year = "2006",
}
@PROCEEDINGS{MKM07,
  title = {{MKM/Calculemus}},
  booktitle = {Towards Mechanized Mathematical Assistants. {MKM/Calculemus}},
  year = {2007},
  isbn = {978-3-540-73083-5},
  editor = {Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger},
  number = {4573},
  series = {LNAI},
  keywords = {conference},
  publisher = {Springer Verlag}}
@Proceedings{MathUI17,
  editor =   {Andrea Kohlhase and Marco Pollanen},
  title =    {MathUI 2017: The 12th Workshop on Mathematical User Interfaces},
  booktitle =    {MathUI 2017: The 12th Workshop on Mathematical User Interfaces},
  SOONurl = {http://ceur-ws.org/Vol-1785/},
  pubs = {akohlhase},
  year =    {2017}}

@article{RK:mmt:10,
  author = "F. Rabe and M. Kohlhase",
  title = "{A Scalable Module System}",
  year = "2013",
  pages = "1--54",
  journal = "Information and Computation",
  volume = "230",
  number = "1"
}
@inproceedings{KR:hollight:14,
  author = "C. Kaliszyk and F. Rabe",
  title = "{Towards Knowledge Management for HOL Light}",
  year = "2014",
  pages = "357--372",
  booktitle = "Intelligent Computer Mathematics",
  editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban",
  publisher = "Springer"
}

@Article{imps,
  author =	"W. Farmer and J. Guttman and F. Thayer",
  title =	"{IMPS: An Interactive Mathematical Proof System}",
  journal =	"{Journal of Automated Reasoning}",
  pages =	"213--248",
  volume =	"11",
  number =	"2",
  year = 	"1993",
}
@article{RK:mmt:10,
  author = "F. Rabe and M. Kohlhase",
  title = "{A Scalable Module System}",
  year = "2013",
  pages = "1--54",
  journal = "Information and Computation",
  volume = "230",
  number = "1"
}
@book{omdoc,
  author = "M. Kohlhase",
  title = "{OMDoc: An Open Markup Format for Mathematical Documents (Version 1.2)}",
  series = "{Lecture Notes in Artificial Intelligence}",
  number = "4180",
  publisher = "Springer",
  year = "2006",
}
@inproceedings{KMOR:pvs:17,
  author = "M. Kohlhase and D. M{\"u}ller and S. Owre and F. Rabe",
  title = "{Making PVS Accessible to Generic Services by Interpretation in a Universal Format}",
  year = "2017",
  pages = "319--335",
  booktitle = "Interactive Theorem Proving",
  editor = "M. Ayala-Rincon and C. Munoz",
  publisher = "Springer"
}
@inproceedings{KR:hollight:14,
  author = "C. Kaliszyk and F. Rabe",
  title = "{Towards Knowledge Management for HOL Light}",
  year = "2014",
  pages = "357--372",
  booktitle = "Intelligent Computer Mathematics",
  editor = "S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban",
  publisher = "Springer"
}
@inproceedings{hol_isahol_matching,
  author = {T. Gauthier and C. Kaliszyk},
  title = "{Matching concepts across HOL libraries}",
  booktitle = {Intelligent Computer Mathematics},
  editor = {S. Watt and J. Davenport and A. Sexton and P. Sojka and J. Urban},
  pages = {267--281},
  year = 2014,
  publisher = {Springer}
}
@Article{lf,
  author = 	 "R. Harper and F. Honsell and G. Plotkin",
  title = 	 "{A framework for defining logics}",
  journal =	 "{Journal of the Association for Computing Machinery}",
  year =	 1993,
  volume =	 40,
  number = 	1,
  pages =	 "143--184",
}

@inproceedings{pvs,
    AUTHOR = {S. Owre and J. Rushby and N. Shankar},
    TITLE = "{PVS: A Prototype Verification System}",
    BOOKTITLE = "{11th International Conference on Automated Deduction (CADE)}",
    YEAR = {1992},
    EDITOR = {D. Kapur},
    PAGES = {748--752},
    PUBLISHER = {Springer},
}
@online{PVSlibraries:on,crossref={PVSlibraries:base},
  urldate = {2014-12-17},
  label = {PVS}}
@MISC{PVSlibraries:url,crossref={PVSlibraries:base},key = {PVS},
  howpublished = {\url{http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/}}}
@MISC{PVSlibraries:base,
  title = {{NASA} {PVS} Library},
  url = {http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/}}
@BOOK{Graf:ti96,
  title = {Term Indexing},
  publisher = {Springer Verlag},
  year = {1996},
  author = {Graf, Peter},
  number = {1053},
  series = {LNCS}}
@inproceedings{am:doceng10,crossref={DOCENG10},
  author    = {Serge Autexier and Normen M{\"u}ller},
  title     = {Semantics-based Change Impact Analysis for Heterogeneous Collections of Documents},
  pages     = {97--106},
  numpages  = {10},
  url       = {http://doi.acm.org/10.1145/1860559.1860580},
  doi       = {http://doi.acm.org/10.1145/1860559.1860580},
  acmid     = {1860580},
  keywords  = {change impact analysis, document collections, document management, graph rewriting, semantics},
  pubs      = {nmueller,omoc,omdoc}}
@mastersthesis{iancu:msc,
  author = "Mihnea Iancu",
  title = "{Management of Change in Declarative Languages}",
  year = "2012",
  school = "Jacobs University Bremen",
  pubs={mscthesis}
}
@proceedings{DOCENG10,
  editor    = {Michael Gormish and Rolf Ingold},
  title = {Proceedings of the 10\textsuperscript{th} {ACM} symposium on Document engineering},
  booktitle = {Proceedings of the 10\textsuperscript{th} {ACM} symposium on Document engineering},
  series    = {DocEng '10},
  year      = {2010},
  isbn      = {978-1-4503-0231-9},
  location  = {Manchester, United Kingdom},
  publisher = {ACM},
  keywords = {conference},
  address   = {New York, NY, USA}}