diff --git a/courses/theses.md b/courses/theses.md
index c73367a18c84f2ca4555a4c34798e1c0dae747f5..c1ed4a60e448ce76edbdd653d78efb864a408708 100644
--- a/courses/theses.md
+++ b/courses/theses.md
@@ -1,14 +1,94 @@
 ---
 layout: page
-title: For Students
-menu_title: KWARC For Students
+title: KWARC Theses
+menu_title: Completed Theses
 menu_order: 101
 ---
-The KWARC Group welcomes student involvement in research. If you are interested, please
-send an e-mail to [<michael.kohlhase@fau.de>](maito:michael.kohlhase@fau.de), or come to
-our seminars and courses. 
+**List is still under construction** 
+### Ph.D. Theses
+* Mihnea Iancu: *Towards Flexiformal Mathematics*, Jacobs University, XII 2016. 
+* Feryal Fulya Horozal: *Framework for Defining Declarative Languages*, Jacobs University,
+  XI 2014. 
+* Vyacheslav Zholudev: *Enhancing XML Preservation and Workflows*, Jacobs University, VI 2012. 
+* Christoph Lange: *Enabling Collaboration on Semiformal Mathematical Knowledge by
+      Semantic Web Integration*, Jacobs University, III 2011. 
+* Christine M\"uller: *Adaptation of Mathematical Documents*,  Jacobs University, V 2010. 
+* Normen M\"uller: *Change Management on Semi-Structured Documents*,  Jacobs University, VIII 2010.
+* Immanuel Normann: *Automated Theory Interpretation*, Jacobs  University, XII 2008.
+* Florian Rabe: *Representing Logics and Logic Translations*, Jacobs University, VI 2008. 
+* Karsten Konrad: *Model Generation for Natural Lanugage Interpretation and Analysis*, Universtät des Saarlandes, IV 2000.
+* Christoph Benzm\"uller: *Equality and Extensionality in
+      Higher-Order Theorem Proving*, Universtät des Saarlandes, V 1999.
+* Susanna Kuschert: *Dynamic Meaning and Accomodation*,  Universtät des Saarlandes, II 1999, 
 
-We have an initial list of topics for
-[theses, or guided research](https://gl.kwarc.info/kwarc/thesis-projects) which may suit
-you, but you can always [adopt one of our currently orphaned systems](/systems/orphans/).
+### M.Sc Theses
+* Theresa Pollinger: *[Knowledge Representation for Modeling and Simulation
+– Bridging the Gap Between Informal PDE Theory and Simulations Practice](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2017/tpollinger/thesis.pdf)*,FAU Erlangen-Nürnberg, 2017
+* Tom Wiesing: 
+[Enabling Cross-System Communication Using Virtual Theories a.nd QMT](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2017/twiesing/thesis.pdf)
+Jacobs University, 2017.
+* Ulrich Rabenstein: [Meaning Extraction and Semantic Services in STEM-Documents - 
+A case study on Quantity Expressions and Units](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2017/urabenstein/Rabenstein.pdf)
+FAU Erlangen-Nürnberg, 2017
+* Aivaras Jacubauskas: [Reflecting Declarative Rule
+Implementations](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2013/jakubauskas_aivaras/project/thesis/thesis01.pdf),
+Jacobs University, 2013.
+* Catalin David: *[Semantic Alliance Framework: Integrating Documents and Semantic Services
+](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2012/david_catalin/project/thesis/thesis.pdf)*, Jacobs University, 2012
+* Stefania Dumbrava:
+  *[A Type Theory with Reflection](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2012/dumbrava_stefania/project/MScThesis_Stefania/Thesis_Stefania.pdf)*,
+  *Jacobs University, 2012.
+* Mihnea Iancu:
+  *[Management of Change in Declarative Languages](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2012/iancu_mihnea/project/thesis/Mihnea_Iancu-Master_Thesis.pdf)*,
+  *Jacobs University, 2012.
+* Fusun Horozal:
+  *[Management of Change in the Web Ontology Language](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2011/horozal_fusun/project/final_thesis_horozal.pdf)*,
+  *Jacobs University, 2011.
+* Alin Iacob:
+  *[Towards Project-Based Workflows in Twelf](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2011/iacob_alin/project/thesis/thesis.pdf)*,
+  *Jacobs University, 2011.
+*  Mihai Grigore:
+   *[Knowledge-poor Interpretation of Mathematical Expressions in Context](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2010/grigore_mihai/thesis/thesis_template.pdf)*,
+   *Jacobs University, 2010
+* Sönke Holsten: *Smart Management of Change on OMDoc Documetns*, Jacobs University, 2010. 
+* Constantin Jucovschi: *[Editing Knowledge in Large Mathematical Corpora. A
+    case study with Semantic LATEX (sTeX)](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2010/jucovschi_constantin/masterthesis/thesis.pdf)*, Jacobs University, 2010.
+* Kristina Sojakova: *[Mechanically Verifying Logic Translations](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2010/sojakova_kristina/proposal.pdf)*, Jacobs University, 2010.
+* Milena Makaveeva *[Management of Change in Common Criteria IT Security
+      Documentation](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2009/makaveeva_milena/thesis_makaveeva.pdf)*,
+      Jacobs University, 2009.
+* Stefan Anca: *[Recovering content from Scientific Documents for Search](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2009/anca_stefan/project/thesis/Stefan_Anca_Masters_Thesis.pdf)*, Jacobs
+      University, 2009.
+* Bastian Laubner: *[Mapping Mathematics with Theory Graphs A Case Study and
+      a Prototype](https://gl.kwarc.info/supervision/MSc-archive/blob/master/2007/laubner_bastian/thesis.pdf)*, Jacobs University, 2007. 
+* Christoph Lange: *Adding Semantics to Mathematical Wikis*, Trier University, 2005. 
+* William Tayson: *Treating Quantifier Scope by Model
+    Generation*, CMU, 2004.
+* Sarah Eisenhardt: *Model Generation for Negations in Natural
+    Language*, CMU,  2004.
+* Andreas Franke: *\textsc{MBase}, A Mathematical Knowledge Base*, Universtät des Saarlandes, 2003. 
+* Stephan Walther: *Model Generation and Dynamic Semantics*, Universtät des Saarlandes, 2001. 
+* Aljoscha Burkard: *Resource-adaptive Model
+    Generation for Natural Language Understanding*, Universtät des Saarlandes, 2001.
+* Stephan Hess: *Human Computer Interaction in a Proof
+    Development Environment*, Universtät des Saarlandes, 1999. 
+* Judith Baur: *Syntax and Semantics of Mathematical Texts -- a
+    Prototype*, Universtät des Saarlandes, 1999. 
+* Lars Klein: *Intexing Techniques for Higher-Order Logic*, Universtät des Saarlandes, 1997. 
+* Andreas Meier: *Proof Transformation*, Universtät des Saarlandes, 1997 
+* Volker Sorge: *Integrating a Computer Algebra System
+    into a Logical Proof Development Environement*, Universtät des Saarlandes, 1996.
+* Gerald Klein: *Unification for a
+    lambda-Calculus with Term Declarations and Intersection Sorts*, Universtät des
+    Saarlandes, 1995.
+* Ahmet Bozkurt: *Strategies for Resolution Theorem Provers in
+    Higher-Order Logic*, Universtät des Saarlandes, 1995.
+* Susanna Kuschert: *An Extension of
+    the lambda-Calculus by Discourse Representation Structures*, Universtät des Saarlandes, 1995.
+* Ortwin Scheja: *Resolution for Higher-Order Multi-Valued Logics*, Universtät des
+  Saarlandes, 1993. 
 
+### B.Sc Theses
+
+The B.Sc theses of the last years can be found in
+[this archive](https://gl.kwarc.info/supervision/BSc-archive).