@inproceedings{9de51ea4ebf044308d69270af37c3598,
title = "Translating a fragment of weak type theory into type theory with open terms",
abstract = "One of the main application areas of interactive proof assistants is the formalization of mathematical texts. This formalization not only allows mathematical texts to be handled electronically, but also to be checked for correctness. Due to the level of detail required in the formalization, formalized texts eliminate ambiguities that may be present in an informally presented mathematical texts.",
author = "G.I. Jojgov",
year = "2006",
doi = "10.1007/11618027\_26",
language = "English",
isbn = "3-540-31430-X",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "389--403",
editor = "M. Kohlhase",
booktitle = "Mathematical Knowledge Management (Fourth International Conference, MKM 2005, Bremen, Germany, July 15-17, 2005, Revised selected papers)",
address = "Germany",
}