diff --git a/tex/report.tex b/tex/report.tex
new file mode 100644
index 0000000000000000000000000000000000000000..13255180e9cb19e533f13b317b51f0269cbb651e
--- /dev/null
+++ b/tex/report.tex
@@ -0,0 +1,131 @@
+\documentclass[orivec]{llncs}
+
+% Florian's macros
+\usepackage{basics}
+
+\usepackage[utf8]{inputenc}
+\usepackage{url, multirow}
+%\usepackage{tipa}
+\usepackage{amsmath,amssymb,amstext}
+\usepackage{graphicx,stmaryrd,mathabx,MnSymbol,tabularx,mathtools}
+\usepackage[normalem]{ulem}
+\usepackage{array}
+\usepackage{mdframed}
+\usepackage{wrapfig}
+\usepackage{paralist}
+\usepackage{xspace}
+\usepackage{mytikz}
+%\usepackage{appendix}
+
+\usepackage[style=alphabetic,hyperref=auto,defernumbers=true,backend=bibtex,firstinits=true,maxbibnames=9,maxcitenames=3,isbn=false]{biblatex}
+
+%\addbibresource{kwarcpubs.bib}
+%\addbibresource{extpubs.bib}
+%\addbibresource{kwarccrossrefs.bib}
+%\addbibresource{extcrossrefs.bib}
+%\addbibresource{systems.bib}
+\addbibresource{biblio}
+\renewbibmacro*{event+venue+date}{}
+\renewbibmacro*{doi+eprint+url}{%
+  \iftoggle{bbx:doi}
+  {\printfield{doi}\iffieldundef{doi}{}{\clearfield{url}}}
+    {}%
+  \newunit\newblock
+  \iftoggle{bbx:eprint}
+    {\usebibmacro{eprint}}
+    {}%froms.filterNot(t => commons.exists(_.path == t.path))
+  \newunit\newblock
+  \iftoggle{bbx:url}
+    {\usebibmacro{url+urldate}}
+    {}}
+
+\setlength{\hfuzz}{3pt} \hbadness=10001
+\setcounter{tocdepth}{2} % for pdf bookmarks
+\usepackage{xcolor}
+\usepackage{listings}
+\lstset{columns=fullflexible,basicstyle=\sf}
+\usepackage[bookmarks,linkcolor=red,citecolor=blue,urlcolor=gray,colorlinks,breaklinks,bookmarksopen,bookmarksnumbered]{hyperref}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% local macros and configurations
+
+% \usepackage[llncs]{../../fr-macros/theorems}
+% \input{macros}
+
+\def\cB{\mathcal{B}}
+\def\cL{\mathcal{L}}
+\def\defemph{\textbf}
+\def\MMT{\textsf{MMT}\xspace}
+\usepackage[show]{ed}
+\newif\ifshort\shorttrue
+
+\pagestyle{plain} % remove for final version
+
+\author{Dennis Müller\inst{1} \and Michael Kohlhase\inst{1}\and Florian Rabe\inst{1,2}\orcidID{0000-0003-3040-3655}}
+\institute{Computer Science, FAU Erlangen-N\"urnberg\and LRI, Universit\'e Paris Sud}
+
+\input{macros}
+
+\setcounter{tocdepth}{2}
+
+\begin{document}
+
+%\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\
+
+
+\title{Automatically Finding Theory Morphisms for Knowledge Management}
+\maketitle
+\begin{abstract}
+  We present a method for finding morphisms between formal theories, both within as well
+  as across libraries based on different logical foundations. 
+  % These morphisms can yield both (more or less formal) \emph{alignments} between individual symbols as well as truth-preserving morphisms between whole theories. 
+  As they induce new theorems in the target theory for any of the source theory, theory morphisms are high-value elements of
+  a modular formal library. Usually, theory morphisms are manually encoded, but this
+  practice requires authors who are familiar with source and target theories at the same
+  time, which limits the scalability of the manual approach. 
+
+  To remedy this problem, we have developed a morphism finder algorithm that automates theory
+  morphism discovery. In this paper we present an implementation in the MMT system and
+  show specific use cases. We focus on an application of \emph{theory discovery}, where a user can
+  check whether a (part of a) formal theory already exists in some library, potentially
+  avoiding duplication of work or suggesting an opportunity for refactoring.
+\end{abstract}
+
+\section{Introduction}\label{sec:intro}
+\input{intro}
+
+\section{Preliminaries: MMT and Views}\label{sec:prelim}
+\input{prelim}
+
+\section{Intra-Library View Finding}\label{sec:viewfinder}
+\input{viewfinder}
+
+\section{Inter-Library View Finding}\label{sec:across}
+\input{usecase}
+
+%\section{Low-Hanging Fruit: Other Applications}\label{sec:appl}
+%\input{applications}
+
+\section{Conclusion}\label{sec:concl}
+\input{conclusion}
+
+\renewcommand*{\bibfont}{\small}
+\printbibliography
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% eval:  (set-fill-column 5000)
+%%% eval:  (visual-line-mode)
+%%% TeX-master: t
+%%% End:
+
+
+%  LocalWords:  inst maketitle formalization defs well-formedness textsf sec:impl impl
+%  LocalWords:  sec:conc conc Universit printbibliography ednote Internalizing newpage
+%  LocalWords:  ifshort sec:relwork relwork renewcommand bibfont tbw setcounter tocdepth
+%  LocalWords:  tableofcontents defemph compactenum emptyset newpart compactitem lstset
+%  LocalWords:  centering aboveskip 0pt,belowskip hline lstlisting mathescape rightarrow
+%  LocalWords:  vdash baseset sec:concl subsubsection Formalizations emph sec:usecase
+%  LocalWords:  usecase Unrealized sec:appl